Step | Hyp | Ref
| Expression |
1 | | lsatcvat.s |
. . 3
β’ π = (LSubSpβπ) |
2 | | lsatcvat.o |
. . 3
β’ 0 =
(0gβπ) |
3 | | lsatcvat.a |
. . 3
β’ π΄ = (LSAtomsβπ) |
4 | | lsatcvat.w |
. . . 4
β’ (π β π β LVec) |
5 | | lveclmod 20417 |
. . . 4
β’ (π β LVec β π β LMod) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π β π β LMod) |
7 | | lsatcvat.u |
. . 3
β’ (π β π β π) |
8 | | lsatcvat.n |
. . 3
β’ (π β π β { 0 }) |
9 | 1, 2, 3, 6, 7, 8 | lssatomic 37225 |
. 2
β’ (π β βπ₯ β π΄ π₯ β π) |
10 | | eqid 2736 |
. . . . 5
β’ (
βL βπ) = ( βL βπ) |
11 | 4 | 3ad2ant1 1133 |
. . . . 5
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β LVec) |
12 | 6 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β LMod) |
13 | | simp2 1137 |
. . . . . 6
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π₯ β π΄) |
14 | 1, 3, 12, 13 | lsatlssel 37211 |
. . . . 5
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π₯ β π) |
15 | | lsatcvat.q |
. . . . . . . 8
β’ (π β π β π΄) |
16 | 1, 3, 6, 15 | lsatlssel 37211 |
. . . . . . 7
β’ (π β π β π) |
17 | 16 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β π) |
18 | | lsatcvat.p |
. . . . . . 7
β’ β =
(LSSumβπ) |
19 | 1, 18 | lsmcl 20394 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π₯ β π) β (π β π₯) β π) |
20 | 12, 17, 14, 19 | syl3anc 1371 |
. . . . 5
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β (π β π₯) β π) |
21 | 7 | 3ad2ant1 1133 |
. . . . 5
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β π) |
22 | | lsatcvat.m |
. . . . . . . . . 10
β’ (π β Β¬ π β π) |
23 | 22 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β Β¬ π β π) |
24 | | sseq1 3951 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ β π β π β π)) |
25 | 24 | biimpcd 249 |
. . . . . . . . . . 11
β’ (π₯ β π β (π₯ = π β π β π)) |
26 | 25 | necon3bd 2955 |
. . . . . . . . . 10
β’ (π₯ β π β (Β¬ π β π β π₯ β π)) |
27 | 26 | 3ad2ant3 1135 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β (Β¬ π β π β π₯ β π)) |
28 | 23, 27 | mpd 15 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π₯ β π) |
29 | 15 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β π΄) |
30 | 2, 3, 11, 13, 29 | lsatnem0 37259 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β (π₯ β π β (π₯ β© π) = { 0 })) |
31 | 28, 30 | mpbid 231 |
. . . . . . 7
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β (π₯ β© π) = { 0 }) |
32 | 1, 18, 2, 3, 10, 11, 14, 29 | lcvp 37254 |
. . . . . . 7
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β ((π₯ β© π) = { 0 } β π₯( βL
βπ)(π₯ β π))) |
33 | 31, 32 | mpbid 231 |
. . . . . 6
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π₯( βL βπ)(π₯ β π)) |
34 | | lmodabl 20219 |
. . . . . . . 8
β’ (π β LMod β π β Abel) |
35 | 12, 34 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β Abel) |
36 | 1 | lsssssubg 20269 |
. . . . . . . . 9
β’ (π β LMod β π β (SubGrpβπ)) |
37 | 12, 36 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β (SubGrpβπ)) |
38 | 37, 14 | sseldd 3927 |
. . . . . . 7
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π₯ β (SubGrpβπ)) |
39 | 37, 17 | sseldd 3927 |
. . . . . . 7
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β (SubGrpβπ)) |
40 | 18 | lsmcom 19508 |
. . . . . . 7
β’ ((π β Abel β§ π₯ β (SubGrpβπ) β§ π β (SubGrpβπ)) β (π₯ β π) = (π β π₯)) |
41 | 35, 38, 39, 40 | syl3anc 1371 |
. . . . . 6
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β (π₯ β π) = (π β π₯)) |
42 | 33, 41 | breqtrd 5107 |
. . . . 5
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π₯( βL βπ)(π β π₯)) |
43 | | simp3 1138 |
. . . . 5
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π₯ β π) |
44 | | lsatcvat.l |
. . . . . . 7
β’ (π β π β (π β π
)) |
45 | 44 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β (π β π
)) |
46 | 18 | lsmub1 19311 |
. . . . . . . 8
β’ ((π β (SubGrpβπ) β§ π₯ β (SubGrpβπ)) β π β (π β π₯)) |
47 | 39, 38, 46 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β (π β π₯)) |
48 | | lsatcvat.r |
. . . . . . . . 9
β’ (π β π
β π΄) |
49 | 48 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π
β π΄) |
50 | 44 | pssssd 4038 |
. . . . . . . . . 10
β’ (π β π β (π β π
)) |
51 | 50 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β (π β π
)) |
52 | 43, 51 | sstrd 3936 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π₯ β (π β π
)) |
53 | 18, 3, 11, 13, 49, 29, 52, 28 | lsatexch1 37260 |
. . . . . . 7
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π
β (π β π₯)) |
54 | 1, 3, 6, 48 | lsatlssel 37211 |
. . . . . . . . . 10
β’ (π β π
β π) |
55 | 54 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π
β π) |
56 | 37, 55 | sseldd 3927 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π
β (SubGrpβπ)) |
57 | 37, 20 | sseldd 3927 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β (π β π₯) β (SubGrpβπ)) |
58 | 18 | lsmlub 19319 |
. . . . . . . 8
β’ ((π β (SubGrpβπ) β§ π
β (SubGrpβπ) β§ (π β π₯) β (SubGrpβπ)) β ((π β (π β π₯) β§ π
β (π β π₯)) β (π β π
) β (π β π₯))) |
59 | 39, 56, 57, 58 | syl3anc 1371 |
. . . . . . 7
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β ((π β (π β π₯) β§ π
β (π β π₯)) β (π β π
) β (π β π₯))) |
60 | 47, 53, 59 | mpbi2and 710 |
. . . . . 6
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β (π β π
) β (π β π₯)) |
61 | 45, 60 | psssstrd 4050 |
. . . . 5
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β (π β π₯)) |
62 | 1, 10, 11, 14, 20, 21, 42, 43, 61 | lcvnbtwn3 37242 |
. . . 4
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π = π₯) |
63 | 62, 13 | eqeltrd 2837 |
. . 3
β’ ((π β§ π₯ β π΄ β§ π₯ β π) β π β π΄) |
64 | 63 | rexlimdv3a 3153 |
. 2
β’ (π β (βπ₯ β π΄ π₯ β π β π β π΄)) |
65 | 9, 64 | mpd 15 |
1
β’ (π β π β π΄) |