Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π) |
2 | | simprl 529 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π§ β π) |
3 | | simplr 528 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π β π΅) |
4 | | simprrl 539 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π β π ) |
5 | 3, 4 | sseldd 3168 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π β π΅) |
6 | | lsspropd.s1 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) β π) |
7 | 6 | ralrimivva 2569 |
. . . . . . . . . . . . . . 15
β’ (π β βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π) |
8 | 7 | ad2antrr 488 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π) |
9 | | ovrspc2v 5914 |
. . . . . . . . . . . . . 14
β’ (((π§ β π β§ π β π΅) β§ βπ₯ β π βπ¦ β π΅ (π₯( Β·π
βπΎ)π¦) β π) β (π§( Β·π
βπΎ)π) β π) |
10 | 2, 5, 8, 9 | syl21anc 1247 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β (π§( Β·π
βπΎ)π) β π) |
11 | | lsspropd.w |
. . . . . . . . . . . . . . 15
β’ (π β π΅ β π) |
12 | 11 | ad2antrr 488 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π΅ β π) |
13 | | simprrr 540 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π β π ) |
14 | 3, 13 | sseldd 3168 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π β π΅) |
15 | 12, 14 | sseldd 3168 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β π β π) |
16 | | lsspropd.p |
. . . . . . . . . . . . . 14
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) |
17 | 16 | oveqrspc2v 5915 |
. . . . . . . . . . . . 13
β’ ((π β§ ((π§( Β·π
βπΎ)π) β π β§ π β π)) β ((π§( Β·π
βπΎ)π)(+gβπΎ)π) = ((π§( Β·π
βπΎ)π)(+gβπΏ)π)) |
18 | 1, 10, 15, 17 | syl12anc 1246 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β ((π§( Β·π
βπΎ)π)(+gβπΎ)π) = ((π§( Β·π
βπΎ)π)(+gβπΏ)π)) |
19 | | lsspropd.s2 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) |
20 | 19 | oveqrspc2v 5915 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π§ β π β§ π β π΅)) β (π§( Β·π
βπΎ)π) = (π§( Β·π
βπΏ)π)) |
21 | 1, 2, 5, 20 | syl12anc 1246 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β (π§( Β·π
βπΎ)π) = (π§( Β·π
βπΏ)π)) |
22 | 21 | oveq1d 5903 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β ((π§( Β·π
βπΎ)π)(+gβπΏ)π) = ((π§( Β·π
βπΏ)π)(+gβπΏ)π)) |
23 | 18, 22 | eqtrd 2220 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β ((π§( Β·π
βπΎ)π)(+gβπΎ)π) = ((π§( Β·π
βπΏ)π)(+gβπΏ)π)) |
24 | 23 | eleq1d 2256 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ (π§ β π β§ (π β π β§ π β π ))) β (((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π β ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π )) |
25 | 24 | anassrs 400 |
. . . . . . . . 9
β’ ((((π β§ π β π΅) β§ π§ β π) β§ (π β π β§ π β π )) β (((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π β ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π )) |
26 | 25 | 2ralbidva 2509 |
. . . . . . . 8
β’ (((π β§ π β π΅) β§ π§ β π) β (βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π β βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π )) |
27 | 26 | ralbidva 2483 |
. . . . . . 7
β’ ((π β§ π β π΅) β (βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π β βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π )) |
28 | 27 | anbi2d 464 |
. . . . . 6
β’ ((π β§ π β π΅) β ((βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ) β (βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ))) |
29 | 28 | pm5.32da 452 |
. . . . 5
β’ (π β ((π β π΅ β§ (βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π )) β (π β π΅ β§ (βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π )))) |
30 | | 3anass 983 |
. . . . 5
β’ ((π β π΅ β§ βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ) β (π β π΅ β§ (βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ))) |
31 | | 3anass 983 |
. . . . 5
β’ ((π β π΅ β§ βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ) β (π β π΅ β§ (βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ))) |
32 | 29, 30, 31 | 3bitr4g 223 |
. . . 4
β’ (π β ((π β π΅ β§ βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ) β (π β π΅ β§ βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ))) |
33 | | lsspropd.b1 |
. . . . . 6
β’ (π β π΅ = (BaseβπΎ)) |
34 | 33 | sseq2d 3197 |
. . . . 5
β’ (π β (π β π΅ β π β (BaseβπΎ))) |
35 | | lsspropd.p1 |
. . . . . 6
β’ (π β π = (Baseβ(ScalarβπΎ))) |
36 | 35 | raleqdv 2689 |
. . . . 5
β’ (π β (βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π β βπ§ β (Baseβ(ScalarβπΎ))βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π )) |
37 | 34, 36 | 3anbi13d 1324 |
. . . 4
β’ (π β ((π β π΅ β§ βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ) β (π β (BaseβπΎ) β§ βπ π β π β§ βπ§ β (Baseβ(ScalarβπΎ))βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ))) |
38 | | lsspropd.b2 |
. . . . . 6
β’ (π β π΅ = (BaseβπΏ)) |
39 | 38 | sseq2d 3197 |
. . . . 5
β’ (π β (π β π΅ β π β (BaseβπΏ))) |
40 | | lsspropd.p2 |
. . . . . 6
β’ (π β π = (Baseβ(ScalarβπΏ))) |
41 | 40 | raleqdv 2689 |
. . . . 5
β’ (π β (βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π β βπ§ β (Baseβ(ScalarβπΏ))βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π )) |
42 | 39, 41 | 3anbi13d 1324 |
. . . 4
β’ (π β ((π β π΅ β§ βπ π β π β§ βπ§ β π βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ) β (π β (BaseβπΏ) β§ βπ π β π β§ βπ§ β (Baseβ(ScalarβπΏ))βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ))) |
43 | 32, 37, 42 | 3bitr3d 218 |
. . 3
β’ (π β ((π β (BaseβπΎ) β§ βπ π β π β§ βπ§ β (Baseβ(ScalarβπΎ))βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ) β (π β (BaseβπΏ) β§ βπ π β π β§ βπ§ β (Baseβ(ScalarβπΏ))βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ))) |
44 | | lsppropd.v1 |
. . . 4
β’ (π β πΎ β π) |
45 | | eqid 2187 |
. . . . 5
β’
(ScalarβπΎ) =
(ScalarβπΎ) |
46 | | eqid 2187 |
. . . . 5
β’
(Baseβ(ScalarβπΎ)) = (Baseβ(ScalarβπΎ)) |
47 | | eqid 2187 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
48 | | eqid 2187 |
. . . . 5
β’
(+gβπΎ) = (+gβπΎ) |
49 | | eqid 2187 |
. . . . 5
β’ (
Β·π βπΎ) = ( Β·π
βπΎ) |
50 | | eqid 2187 |
. . . . 5
β’
(LSubSpβπΎ) =
(LSubSpβπΎ) |
51 | 45, 46, 47, 48, 49, 50 | islssmg 13511 |
. . . 4
β’ (πΎ β π β (π β (LSubSpβπΎ) β (π β (BaseβπΎ) β§ βπ π β π β§ βπ§ β (Baseβ(ScalarβπΎ))βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ))) |
52 | 44, 51 | syl 14 |
. . 3
β’ (π β (π β (LSubSpβπΎ) β (π β (BaseβπΎ) β§ βπ π β π β§ βπ§ β (Baseβ(ScalarβπΎ))βπ β π βπ β π ((π§( Β·π
βπΎ)π)(+gβπΎ)π) β π ))) |
53 | | lsppropd.v2 |
. . . 4
β’ (π β πΏ β π) |
54 | | eqid 2187 |
. . . . 5
β’
(ScalarβπΏ) =
(ScalarβπΏ) |
55 | | eqid 2187 |
. . . . 5
β’
(Baseβ(ScalarβπΏ)) = (Baseβ(ScalarβπΏ)) |
56 | | eqid 2187 |
. . . . 5
β’
(BaseβπΏ) =
(BaseβπΏ) |
57 | | eqid 2187 |
. . . . 5
β’
(+gβπΏ) = (+gβπΏ) |
58 | | eqid 2187 |
. . . . 5
β’ (
Β·π βπΏ) = ( Β·π
βπΏ) |
59 | | eqid 2187 |
. . . . 5
β’
(LSubSpβπΏ) =
(LSubSpβπΏ) |
60 | 54, 55, 56, 57, 58, 59 | islssmg 13511 |
. . . 4
β’ (πΏ β π β (π β (LSubSpβπΏ) β (π β (BaseβπΏ) β§ βπ π β π β§ βπ§ β (Baseβ(ScalarβπΏ))βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ))) |
61 | 53, 60 | syl 14 |
. . 3
β’ (π β (π β (LSubSpβπΏ) β (π β (BaseβπΏ) β§ βπ π β π β§ βπ§ β (Baseβ(ScalarβπΏ))βπ β π βπ β π ((π§( Β·π
βπΏ)π)(+gβπΏ)π) β π ))) |
62 | 43, 52, 61 | 3bitr4d 220 |
. 2
β’ (π β (π β (LSubSpβπΎ) β π β (LSubSpβπΏ))) |
63 | 62 | eqrdv 2185 |
1
β’ (π β (LSubSpβπΎ) = (LSubSpβπΏ)) |