Step | Hyp | Ref
| Expression |
1 | | lsatcvat.o |
. . 3
β’ 0 =
(0gβπ) |
2 | | lsatcvat.s |
. . 3
β’ π = (LSubSpβπ) |
3 | | lsatcvat.p |
. . 3
β’ β =
(LSSumβπ) |
4 | | lsatcvat.a |
. . 3
β’ π΄ = (LSAtomsβπ) |
5 | | lsatcvat.w |
. . . 4
β’ (π β π β LVec) |
6 | 5 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β π) β π β LVec) |
7 | | lsatcvat.u |
. . . 4
β’ (π β π β π) |
8 | 7 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β π) β π β π) |
9 | | lsatcvat.q |
. . . 4
β’ (π β π β π΄) |
10 | 9 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β π) β π β π΄) |
11 | | lsatcvat.r |
. . . 4
β’ (π β π
β π΄) |
12 | 11 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β π) β π
β π΄) |
13 | | lsatcvat.n |
. . . 4
β’ (π β π β { 0 }) |
14 | 13 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β π) β π β { 0 }) |
15 | | lsatcvat.l |
. . . 4
β’ (π β π β (π β π
)) |
16 | 15 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π β π) β π β (π β π
)) |
17 | | simpr 486 |
. . 3
β’ ((π β§ Β¬ π β π) β Β¬ π β π) |
18 | 1, 2, 3, 4, 6, 8, 10, 12, 14, 16, 17 | lsatcvatlem 37540 |
. 2
β’ ((π β§ Β¬ π β π) β π β π΄) |
19 | 5 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π
β π) β π β LVec) |
20 | 7 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π
β π) β π β π) |
21 | 11 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π
β π) β π
β π΄) |
22 | 9 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π
β π) β π β π΄) |
23 | 13 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π
β π) β π β { 0 }) |
24 | | lveclmod 20583 |
. . . . . . . . 9
β’ (π β LVec β π β LMod) |
25 | 5, 24 | syl 17 |
. . . . . . . 8
β’ (π β π β LMod) |
26 | | lmodabl 20385 |
. . . . . . . 8
β’ (π β LMod β π β Abel) |
27 | 25, 26 | syl 17 |
. . . . . . 7
β’ (π β π β Abel) |
28 | 2 | lsssssubg 20435 |
. . . . . . . . 9
β’ (π β LMod β π β (SubGrpβπ)) |
29 | 25, 28 | syl 17 |
. . . . . . . 8
β’ (π β π β (SubGrpβπ)) |
30 | 2, 4, 25, 9 | lsatlssel 37488 |
. . . . . . . 8
β’ (π β π β π) |
31 | 29, 30 | sseldd 3950 |
. . . . . . 7
β’ (π β π β (SubGrpβπ)) |
32 | 2, 4, 25, 11 | lsatlssel 37488 |
. . . . . . . 8
β’ (π β π
β π) |
33 | 29, 32 | sseldd 3950 |
. . . . . . 7
β’ (π β π
β (SubGrpβπ)) |
34 | 3 | lsmcom 19643 |
. . . . . . 7
β’ ((π β Abel β§ π β (SubGrpβπ) β§ π
β (SubGrpβπ)) β (π β π
) = (π
β π)) |
35 | 27, 31, 33, 34 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β π
) = (π
β π)) |
36 | 35 | psseq2d 4058 |
. . . . 5
β’ (π β (π β (π β π
) β π β (π
β π))) |
37 | 15, 36 | mpbid 231 |
. . . 4
β’ (π β π β (π
β π)) |
38 | 37 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π
β π) β π β (π
β π)) |
39 | | simpr 486 |
. . 3
β’ ((π β§ Β¬ π
β π) β Β¬ π
β π) |
40 | 1, 2, 3, 4, 19, 20, 21, 22, 23, 38, 39 | lsatcvatlem 37540 |
. 2
β’ ((π β§ Β¬ π
β π) β π β π΄) |
41 | 29, 7 | sseldd 3950 |
. . . . . . 7
β’ (π β π β (SubGrpβπ)) |
42 | 3 | lsmlub 19453 |
. . . . . . 7
β’ ((π β (SubGrpβπ) β§ π
β (SubGrpβπ) β§ π β (SubGrpβπ)) β ((π β π β§ π
β π) β (π β π
) β π)) |
43 | 31, 33, 41, 42 | syl3anc 1372 |
. . . . . 6
β’ (π β ((π β π β§ π
β π) β (π β π
) β π)) |
44 | | ssnpss 4068 |
. . . . . 6
β’ ((π β π
) β π β Β¬ π β (π β π
)) |
45 | 43, 44 | syl6bi 253 |
. . . . 5
β’ (π β ((π β π β§ π
β π) β Β¬ π β (π β π
))) |
46 | 45 | con2d 134 |
. . . 4
β’ (π β (π β (π β π
) β Β¬ (π β π β§ π
β π))) |
47 | | ianor 981 |
. . . 4
β’ (Β¬
(π β π β§ π
β π) β (Β¬ π β π β¨ Β¬ π
β π)) |
48 | 46, 47 | syl6ib 251 |
. . 3
β’ (π β (π β (π β π
) β (Β¬ π β π β¨ Β¬ π
β π))) |
49 | 15, 48 | mpd 15 |
. 2
β’ (π β (Β¬ π β π β¨ Β¬ π
β π)) |
50 | 18, 40, 49 | mpjaodan 958 |
1
β’ (π β π β π΄) |