Step | Hyp | Ref
| Expression |
1 | | lsmspsn.w |
. . . 4
β’ (π β π β LMod) |
2 | | lsmspsn.x |
. . . 4
β’ (π β π β π) |
3 | | lsmspsn.v |
. . . . 5
β’ π = (Baseβπ) |
4 | | lsmspsn.n |
. . . . 5
β’ π = (LSpanβπ) |
5 | 3, 4 | lspsnsubg 20456 |
. . . 4
β’ ((π β LMod β§ π β π) β (πβ{π}) β (SubGrpβπ)) |
6 | 1, 2, 5 | syl2anc 585 |
. . 3
β’ (π β (πβ{π}) β (SubGrpβπ)) |
7 | | lsmspsn.y |
. . . 4
β’ (π β π β π) |
8 | 3, 4 | lspsnsubg 20456 |
. . . 4
β’ ((π β LMod β§ π β π) β (πβ{π}) β (SubGrpβπ)) |
9 | 1, 7, 8 | syl2anc 585 |
. . 3
β’ (π β (πβ{π}) β (SubGrpβπ)) |
10 | | lsmspsn.a |
. . . 4
β’ + =
(+gβπ) |
11 | | lsmspsn.p |
. . . 4
β’ β =
(LSSumβπ) |
12 | 10, 11 | lsmelval 19436 |
. . 3
β’ (((πβ{π}) β (SubGrpβπ) β§ (πβ{π}) β (SubGrpβπ)) β (π β ((πβ{π}) β (πβ{π})) β βπ£ β (πβ{π})βπ€ β (πβ{π})π = (π£ + π€))) |
13 | 6, 9, 12 | syl2anc 585 |
. 2
β’ (π β (π β ((πβ{π}) β (πβ{π})) β βπ£ β (πβ{π})βπ€ β (πβ{π})π = (π£ + π€))) |
14 | | lsmspsn.f |
. . . . . . . . . 10
β’ πΉ = (Scalarβπ) |
15 | | lsmspsn.k |
. . . . . . . . . 10
β’ πΎ = (BaseβπΉ) |
16 | | lsmspsn.t |
. . . . . . . . . 10
β’ Β· = (
Β·π βπ) |
17 | 14, 15, 3, 16, 4 | lspsnel 20479 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π) β (π£ β (πβ{π}) β βπ β πΎ π£ = (π Β· π))) |
18 | 1, 2, 17 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π£ β (πβ{π}) β βπ β πΎ π£ = (π Β· π))) |
19 | 14, 15, 3, 16, 4 | lspsnel 20479 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π) β (π€ β (πβ{π}) β βπ β πΎ π€ = (π Β· π))) |
20 | 1, 7, 19 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π€ β (πβ{π}) β βπ β πΎ π€ = (π Β· π))) |
21 | 18, 20 | anbi12d 632 |
. . . . . . 7
β’ (π β ((π£ β (πβ{π}) β§ π€ β (πβ{π})) β (βπ β πΎ π£ = (π Β· π) β§ βπ β πΎ π€ = (π Β· π)))) |
22 | 21 | biimpa 478 |
. . . . . 6
β’ ((π β§ (π£ β (πβ{π}) β§ π€ β (πβ{π}))) β (βπ β πΎ π£ = (π Β· π) β§ βπ β πΎ π€ = (π Β· π))) |
23 | 22 | biantrurd 534 |
. . . . 5
β’ ((π β§ (π£ β (πβ{π}) β§ π€ β (πβ{π}))) β (π = (π£ + π€) β ((βπ β πΎ π£ = (π Β· π) β§ βπ β πΎ π€ = (π Β· π)) β§ π = (π£ + π€)))) |
24 | | r19.41v 3182 |
. . . . . . 7
β’
(βπ β
πΎ ((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)) β (βπ β πΎ (π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€))) |
25 | 24 | rexbii 3094 |
. . . . . 6
β’
(βπ β
πΎ βπ β πΎ ((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)) β βπ β πΎ (βπ β πΎ (π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€))) |
26 | | r19.41v 3182 |
. . . . . 6
β’
(βπ β
πΎ (βπ β πΎ (π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)) β (βπ β πΎ βπ β πΎ (π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€))) |
27 | | reeanv 3216 |
. . . . . . 7
β’
(βπ β
πΎ βπ β πΎ (π£ = (π Β· π) β§ π€ = (π Β· π)) β (βπ β πΎ π£ = (π Β· π) β§ βπ β πΎ π€ = (π Β· π))) |
28 | 27 | anbi1i 625 |
. . . . . 6
β’
((βπ β
πΎ βπ β πΎ (π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)) β ((βπ β πΎ π£ = (π Β· π) β§ βπ β πΎ π€ = (π Β· π)) β§ π = (π£ + π€))) |
29 | 25, 26, 28 | 3bitrri 298 |
. . . . 5
β’
(((βπ β
πΎ π£ = (π Β· π) β§ βπ β πΎ π€ = (π Β· π)) β§ π = (π£ + π€)) β βπ β πΎ βπ β πΎ ((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€))) |
30 | 23, 29 | bitrdi 287 |
. . . 4
β’ ((π β§ (π£ β (πβ{π}) β§ π€ β (πβ{π}))) β (π = (π£ + π€) β βπ β πΎ βπ β πΎ ((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)))) |
31 | 30 | 2rexbidva 3208 |
. . 3
β’ (π β (βπ£ β (πβ{π})βπ€ β (πβ{π})π = (π£ + π€) β βπ£ β (πβ{π})βπ€ β (πβ{π})βπ β πΎ βπ β πΎ ((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)))) |
32 | | rexrot4 3279 |
. . 3
β’
(βπ£ β
(πβ{π})βπ€ β (πβ{π})βπ β πΎ βπ β πΎ ((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)) β βπ β πΎ βπ β πΎ βπ£ β (πβ{π})βπ€ β (πβ{π})((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€))) |
33 | 31, 32 | bitrdi 287 |
. 2
β’ (π β (βπ£ β (πβ{π})βπ€ β (πβ{π})π = (π£ + π€) β βπ β πΎ βπ β πΎ βπ£ β (πβ{π})βπ€ β (πβ{π})((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)))) |
34 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π β πΎ)) β π β LMod) |
35 | | simprl 770 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π β πΎ)) β π β πΎ) |
36 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π β πΎ)) β π β π) |
37 | 3, 16, 14, 15, 4, 34, 35, 36 | lspsneli 20477 |
. . . 4
β’ ((π β§ (π β πΎ β§ π β πΎ)) β (π Β· π) β (πβ{π})) |
38 | | simprr 772 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π β πΎ)) β π β πΎ) |
39 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π β πΎ)) β π β π) |
40 | 3, 16, 14, 15, 4, 34, 38, 39 | lspsneli 20477 |
. . . 4
β’ ((π β§ (π β πΎ β§ π β πΎ)) β (π Β· π) β (πβ{π})) |
41 | | oveq1 7365 |
. . . . . 6
β’ (π£ = (π Β· π) β (π£ + π€) = ((π Β· π) + π€)) |
42 | 41 | eqeq2d 2744 |
. . . . 5
β’ (π£ = (π Β· π) β (π = (π£ + π€) β π = ((π Β· π) + π€))) |
43 | | oveq2 7366 |
. . . . . 6
β’ (π€ = (π Β· π) β ((π Β· π) + π€) = ((π Β· π) + (π Β· π))) |
44 | 43 | eqeq2d 2744 |
. . . . 5
β’ (π€ = (π Β· π) β (π = ((π Β· π) + π€) β π = ((π Β· π) + (π Β· π)))) |
45 | 42, 44 | ceqsrex2v 3609 |
. . . 4
β’ (((π Β· π) β (πβ{π}) β§ (π Β· π) β (πβ{π})) β (βπ£ β (πβ{π})βπ€ β (πβ{π})((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)) β π = ((π Β· π) + (π Β· π)))) |
46 | 37, 40, 45 | syl2anc 585 |
. . 3
β’ ((π β§ (π β πΎ β§ π β πΎ)) β (βπ£ β (πβ{π})βπ€ β (πβ{π})((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)) β π = ((π Β· π) + (π Β· π)))) |
47 | 46 | 2rexbidva 3208 |
. 2
β’ (π β (βπ β πΎ βπ β πΎ βπ£ β (πβ{π})βπ€ β (πβ{π})((π£ = (π Β· π) β§ π€ = (π Β· π)) β§ π = (π£ + π€)) β βπ β πΎ βπ β πΎ π = ((π Β· π) + (π Β· π)))) |
48 | 13, 33, 47 | 3bitrd 305 |
1
β’ (π β (π β ((πβ{π}) β (πβ{π})) β βπ β πΎ βπ β πΎ π = ((π Β· π) + (π Β· π)))) |