Step | Hyp | Ref
| Expression |
1 | | lsatcmp.u |
. . 3
β’ (π β π β π΄) |
2 | | lsatcmp.w |
. . . . 5
β’ (π β π β LVec) |
3 | | lveclmod 20567 |
. . . . 5
β’ (π β LVec β π β LMod) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (π β π β LMod) |
5 | | eqid 2736 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
6 | | eqid 2736 |
. . . . 5
β’
(LSpanβπ) =
(LSpanβπ) |
7 | | eqid 2736 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
8 | | lsatcmp.a |
. . . . 5
β’ π΄ = (LSAtomsβπ) |
9 | 5, 6, 7, 8 | islsat 37453 |
. . . 4
β’ (π β LMod β (π β π΄ β βπ£ β ((Baseβπ) β {(0gβπ)})π = ((LSpanβπ)β{π£}))) |
10 | 4, 9 | syl 17 |
. . 3
β’ (π β (π β π΄ β βπ£ β ((Baseβπ) β {(0gβπ)})π = ((LSpanβπ)β{π£}))) |
11 | 1, 10 | mpbid 231 |
. 2
β’ (π β βπ£ β ((Baseβπ) β {(0gβπ)})π = ((LSpanβπ)β{π£})) |
12 | | eldifsn 4747 |
. . . . 5
β’ (π£ β ((Baseβπ) β
{(0gβπ)})
β (π£ β
(Baseβπ) β§ π£ β (0gβπ))) |
13 | | lsatcmp.t |
. . . . . . . . . . 11
β’ (π β π β π΄) |
14 | 7, 8, 4, 13 | lsatn0 37461 |
. . . . . . . . . 10
β’ (π β π β {(0gβπ)}) |
15 | 14 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β π β {(0gβπ)}) |
16 | 2 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β π β LVec) |
17 | | eqid 2736 |
. . . . . . . . . . . . . 14
β’
(LSubSpβπ) =
(LSubSpβπ) |
18 | 17, 8, 4, 13 | lsatlssel 37459 |
. . . . . . . . . . . . 13
β’ (π β π β (LSubSpβπ)) |
19 | 18 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β π β (LSubSpβπ)) |
20 | | simplrl 775 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β π£ β (Baseβπ)) |
21 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β π β ((LSpanβπ)β{π£})) |
22 | 5, 7, 17, 6 | lspsnat 20606 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ π β (LSubSpβπ) β§ π£ β (Baseβπ)) β§ π β ((LSpanβπ)β{π£})) β (π = ((LSpanβπ)β{π£}) β¨ π = {(0gβπ)})) |
23 | 16, 19, 20, 21, 22 | syl31anc 1373 |
. . . . . . . . . . 11
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β (π = ((LSpanβπ)β{π£}) β¨ π = {(0gβπ)})) |
24 | 23 | ord 862 |
. . . . . . . . . 10
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β (Β¬ π = ((LSpanβπ)β{π£}) β π = {(0gβπ)})) |
25 | 24 | necon1ad 2960 |
. . . . . . . . 9
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β (π β {(0gβπ)} β π = ((LSpanβπ)β{π£}))) |
26 | 15, 25 | mpd 15 |
. . . . . . . 8
β’ (((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β§ π β ((LSpanβπ)β{π£})) β π = ((LSpanβπ)β{π£})) |
27 | 26 | ex 413 |
. . . . . . 7
β’ ((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β (π β ((LSpanβπ)β{π£}) β π = ((LSpanβπ)β{π£}))) |
28 | | eqimss 4000 |
. . . . . . 7
β’ (π = ((LSpanβπ)β{π£}) β π β ((LSpanβπ)β{π£})) |
29 | 27, 28 | impbid1 224 |
. . . . . 6
β’ ((π β§ (π£ β (Baseβπ) β§ π£ β (0gβπ))) β (π β ((LSpanβπ)β{π£}) β π = ((LSpanβπ)β{π£}))) |
30 | 29 | ex 413 |
. . . . 5
β’ (π β ((π£ β (Baseβπ) β§ π£ β (0gβπ)) β (π β ((LSpanβπ)β{π£}) β π = ((LSpanβπ)β{π£})))) |
31 | 12, 30 | biimtrid 241 |
. . . 4
β’ (π β (π£ β ((Baseβπ) β {(0gβπ)}) β (π β ((LSpanβπ)β{π£}) β π = ((LSpanβπ)β{π£})))) |
32 | | sseq2 3970 |
. . . . . 6
β’ (π = ((LSpanβπ)β{π£}) β (π β π β π β ((LSpanβπ)β{π£}))) |
33 | | eqeq2 2748 |
. . . . . 6
β’ (π = ((LSpanβπ)β{π£}) β (π = π β π = ((LSpanβπ)β{π£}))) |
34 | 32, 33 | bibi12d 345 |
. . . . 5
β’ (π = ((LSpanβπ)β{π£}) β ((π β π β π = π) β (π β ((LSpanβπ)β{π£}) β π = ((LSpanβπ)β{π£})))) |
35 | 34 | biimprcd 249 |
. . . 4
β’ ((π β ((LSpanβπ)β{π£}) β π = ((LSpanβπ)β{π£})) β (π = ((LSpanβπ)β{π£}) β (π β π β π = π))) |
36 | 31, 35 | syl6 35 |
. . 3
β’ (π β (π£ β ((Baseβπ) β {(0gβπ)}) β (π = ((LSpanβπ)β{π£}) β (π β π β π = π)))) |
37 | 36 | rexlimdv 3150 |
. 2
β’ (π β (βπ£ β ((Baseβπ) β {(0gβπ)})π = ((LSpanβπ)β{π£}) β (π β π β π = π))) |
38 | 11, 37 | mpd 15 |
1
β’ (π β (π β π β π = π)) |