Step | Hyp | Ref
| Expression |
1 | | lsatcvat3.s |
. 2
β’ π = (LSubSpβπ) |
2 | | lsatcvat3.p |
. 2
β’ β =
(LSSumβπ) |
3 | | lsatcvat3.a |
. 2
β’ π΄ = (LSAtomsβπ) |
4 | | eqid 2737 |
. 2
β’ (
βL βπ) = ( βL βπ) |
5 | | lsatcvat3.w |
. 2
β’ (π β π β LVec) |
6 | | lveclmod 20583 |
. . . 4
β’ (π β LVec β π β LMod) |
7 | 5, 6 | syl 17 |
. . 3
β’ (π β π β LMod) |
8 | | lsatcvat3.u |
. . 3
β’ (π β π β π) |
9 | | lsatcvat3.q |
. . . . 5
β’ (π β π β π΄) |
10 | 1, 3, 7, 9 | lsatlssel 37488 |
. . . 4
β’ (π β π β π) |
11 | | lsatcvat3.r |
. . . . 5
β’ (π β π
β π΄) |
12 | 1, 3, 7, 11 | lsatlssel 37488 |
. . . 4
β’ (π β π
β π) |
13 | 1, 2 | lsmcl 20560 |
. . . 4
β’ ((π β LMod β§ π β π β§ π
β π) β (π β π
) β π) |
14 | 7, 10, 12, 13 | syl3anc 1372 |
. . 3
β’ (π β (π β π
) β π) |
15 | 1 | lssincl 20442 |
. . 3
β’ ((π β LMod β§ π β π β§ (π β π
) β π) β (π β© (π β π
)) β π) |
16 | 7, 8, 14, 15 | syl3anc 1372 |
. 2
β’ (π β (π β© (π β π
)) β π) |
17 | | lsatcvat3.n |
. 2
β’ (π β π β π
) |
18 | | lsatcvat3.m |
. . . . 5
β’ (π β Β¬ π
β π) |
19 | 1, 2, 3, 4, 5, 8, 11 | lcv1 37532 |
. . . . 5
β’ (π β (Β¬ π
β π β π( βL βπ)(π β π
))) |
20 | 18, 19 | mpbid 231 |
. . . 4
β’ (π β π( βL βπ)(π β π
)) |
21 | | lmodabl 20385 |
. . . . . . . . . . 11
β’ (π β LMod β π β Abel) |
22 | 7, 21 | syl 17 |
. . . . . . . . . 10
β’ (π β π β Abel) |
23 | 1 | lsssssubg 20435 |
. . . . . . . . . . . 12
β’ (π β LMod β π β (SubGrpβπ)) |
24 | 7, 23 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β (SubGrpβπ)) |
25 | 24, 10 | sseldd 3950 |
. . . . . . . . . 10
β’ (π β π β (SubGrpβπ)) |
26 | 24, 12 | sseldd 3950 |
. . . . . . . . . 10
β’ (π β π
β (SubGrpβπ)) |
27 | 2 | lsmcom 19643 |
. . . . . . . . . 10
β’ ((π β Abel β§ π β (SubGrpβπ) β§ π
β (SubGrpβπ)) β (π β π
) = (π
β π)) |
28 | 22, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π β π
) = (π
β π)) |
29 | 28 | oveq2d 7378 |
. . . . . . . 8
β’ (π β (π β (π β π
)) = (π β (π
β π))) |
30 | 24, 8 | sseldd 3950 |
. . . . . . . . 9
β’ (π β π β (SubGrpβπ)) |
31 | 2 | lsmass 19458 |
. . . . . . . . 9
β’ ((π β (SubGrpβπ) β§ π
β (SubGrpβπ) β§ π β (SubGrpβπ)) β ((π β π
) β π) = (π β (π
β π))) |
32 | 30, 26, 25, 31 | syl3anc 1372 |
. . . . . . . 8
β’ (π β ((π β π
) β π) = (π β (π
β π))) |
33 | 29, 32 | eqtr4d 2780 |
. . . . . . 7
β’ (π β (π β (π β π
)) = ((π β π
) β π)) |
34 | 1, 2 | lsmcl 20560 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π β§ π
β π) β (π β π
) β π) |
35 | 7, 8, 12, 34 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π β π
) β π) |
36 | 24, 35 | sseldd 3950 |
. . . . . . . 8
β’ (π β (π β π
) β (SubGrpβπ)) |
37 | | lsatcvat3.l |
. . . . . . . 8
β’ (π β π β (π β π
)) |
38 | 2 | lsmless2 19450 |
. . . . . . . 8
β’ (((π β π
) β (SubGrpβπ) β§ (π β π
) β (SubGrpβπ) β§ π β (π β π
)) β ((π β π
) β π) β ((π β π
) β (π β π
))) |
39 | 36, 36, 37, 38 | syl3anc 1372 |
. . . . . . 7
β’ (π β ((π β π
) β π) β ((π β π
) β (π β π
))) |
40 | 33, 39 | eqsstrd 3987 |
. . . . . 6
β’ (π β (π β (π β π
)) β ((π β π
) β (π β π
))) |
41 | 2 | lsmidm 19452 |
. . . . . . 7
β’ ((π β π
) β (SubGrpβπ) β ((π β π
) β (π β π
)) = (π β π
)) |
42 | 36, 41 | syl 17 |
. . . . . 6
β’ (π β ((π β π
) β (π β π
)) = (π β π
)) |
43 | 40, 42 | sseqtrd 3989 |
. . . . 5
β’ (π β (π β (π β π
)) β (π β π
)) |
44 | 24, 14 | sseldd 3950 |
. . . . . 6
β’ (π β (π β π
) β (SubGrpβπ)) |
45 | 2 | lsmub2 19447 |
. . . . . . 7
β’ ((π β (SubGrpβπ) β§ π
β (SubGrpβπ)) β π
β (π β π
)) |
46 | 25, 26, 45 | syl2anc 585 |
. . . . . 6
β’ (π β π
β (π β π
)) |
47 | 2 | lsmless2 19450 |
. . . . . 6
β’ ((π β (SubGrpβπ) β§ (π β π
) β (SubGrpβπ) β§ π
β (π β π
)) β (π β π
) β (π β (π β π
))) |
48 | 30, 44, 46, 47 | syl3anc 1372 |
. . . . 5
β’ (π β (π β π
) β (π β (π β π
))) |
49 | 43, 48 | eqssd 3966 |
. . . 4
β’ (π β (π β (π β π
)) = (π β π
)) |
50 | 20, 49 | breqtrrd 5138 |
. . 3
β’ (π β π( βL βπ)(π β (π β π
))) |
51 | 1, 2, 4, 7, 8, 14,
50 | lcvexchlem4 37528 |
. 2
β’ (π β (π β© (π β π
))( βL βπ)(π β π
)) |
52 | 1, 2, 3, 4, 5, 16,
9, 11, 17, 51 | lsatcvat2 37542 |
1
β’ (π β (π β© (π β π
)) β π΄) |