Step | Hyp | Ref
| Expression |
1 | | lsateln0.u |
. . . 4
β’ (π β π β π΄) |
2 | | lsateln0.w |
. . . . 5
β’ (π β π β LMod) |
3 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
4 | | eqid 2737 |
. . . . . 6
β’
(LSpanβπ) =
(LSpanβπ) |
5 | | lsateln0.z |
. . . . . 6
β’ 0 =
(0gβπ) |
6 | | lsateln0.a |
. . . . . 6
β’ π΄ = (LSAtomsβπ) |
7 | 3, 4, 5, 6 | islsat 37482 |
. . . . 5
β’ (π β LMod β (π β π΄ β βπ£ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π£}))) |
8 | 2, 7 | syl 17 |
. . . 4
β’ (π β (π β π΄ β βπ£ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π£}))) |
9 | 1, 8 | mpbid 231 |
. . 3
β’ (π β βπ£ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π£})) |
10 | | eldifi 4091 |
. . . . . 6
β’ (π£ β ((Baseβπ) β { 0 }) β π£ β (Baseβπ)) |
11 | 3, 4 | lspsnid 20470 |
. . . . . 6
β’ ((π β LMod β§ π£ β (Baseβπ)) β π£ β ((LSpanβπ)β{π£})) |
12 | 2, 10, 11 | syl2an 597 |
. . . . 5
β’ ((π β§ π£ β ((Baseβπ) β { 0 })) β π£ β ((LSpanβπ)β{π£})) |
13 | | eleq2 2827 |
. . . . 5
β’ (π = ((LSpanβπ)β{π£}) β (π£ β π β π£ β ((LSpanβπ)β{π£}))) |
14 | 12, 13 | syl5ibrcom 247 |
. . . 4
β’ ((π β§ π£ β ((Baseβπ) β { 0 })) β (π = ((LSpanβπ)β{π£}) β π£ β π)) |
15 | 14 | reximdva 3166 |
. . 3
β’ (π β (βπ£ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π£}) β βπ£ β ((Baseβπ) β { 0 })π£ β π)) |
16 | 9, 15 | mpd 15 |
. 2
β’ (π β βπ£ β ((Baseβπ) β { 0 })π£ β π) |
17 | | eldifsn 4752 |
. . . . . . 7
β’ (π£ β ((Baseβπ) β { 0 }) β (π£ β (Baseβπ) β§ π£ β 0 )) |
18 | 17 | anbi1i 625 |
. . . . . 6
β’ ((π£ β ((Baseβπ) β { 0 }) β§ π£ β π) β ((π£ β (Baseβπ) β§ π£ β 0 ) β§ π£ β π)) |
19 | | anass 470 |
. . . . . 6
β’ (((π£ β (Baseβπ) β§ π£ β 0 ) β§ π£ β π) β (π£ β (Baseβπ) β§ (π£ β 0 β§ π£ β π))) |
20 | 18, 19 | bitri 275 |
. . . . 5
β’ ((π£ β ((Baseβπ) β { 0 }) β§ π£ β π) β (π£ β (Baseβπ) β§ (π£ β 0 β§ π£ β π))) |
21 | 20 | simprbi 498 |
. . . 4
β’ ((π£ β ((Baseβπ) β { 0 }) β§ π£ β π) β (π£ β 0 β§ π£ β π)) |
22 | 21 | ancomd 463 |
. . 3
β’ ((π£ β ((Baseβπ) β { 0 }) β§ π£ β π) β (π£ β π β§ π£ β 0 )) |
23 | 22 | reximi2 3083 |
. 2
β’
(βπ£ β
((Baseβπ) β {
0 })π£ β π β βπ£ β π π£ β 0 ) |
24 | 16, 23 | syl 17 |
1
β’ (π β βπ£ β π π£ β 0 ) |