Step | Hyp | Ref
| Expression |
1 | | islshpat.v |
. . 3
β’ π = (Baseβπ) |
2 | | eqid 2737 |
. . 3
β’
(LSpanβπ) =
(LSpanβπ) |
3 | | islshpat.s |
. . 3
β’ π = (LSubSpβπ) |
4 | | islshpat.p |
. . 3
β’ β =
(LSSumβπ) |
5 | | islshpat.h |
. . 3
β’ π» = (LSHypβπ) |
6 | | islshpat.w |
. . 3
β’ (π β π β LMod) |
7 | 1, 2, 3, 4, 5, 6 | islshpsm 37471 |
. 2
β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (π β ((LSpanβπ)β{π£})) = π))) |
8 | | df-3an 1090 |
. . . . 5
β’ ((π β π β§ π β π β§ βπ£ β π (π β ((LSpanβπ)β{π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (π β ((LSpanβπ)β{π£})) = π)) |
9 | | r19.42v 3188 |
. . . . 5
β’
(βπ£ β
π ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β ((π β π β§ π β π) β§ βπ£ β π (π β ((LSpanβπ)β{π£})) = π)) |
10 | 8, 9 | bitr4i 278 |
. . . 4
β’ ((π β π β§ π β π β§ βπ£ β π (π β ((LSpanβπ)β{π£})) = π) β βπ£ β π ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) |
11 | | df-rex 3075 |
. . . . . . . 8
β’
(βπ£ β
π ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β βπ£(π£ β π β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
12 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β π£ = (0gβπ)) |
13 | 12 | sneqd 4603 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β {π£} = {(0gβπ)}) |
14 | 13 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β ((LSpanβπ)β{π£}) = ((LSpanβπ)β{(0gβπ)})) |
15 | 6 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β π β LMod) |
16 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(0gβπ) = (0gβπ) |
17 | 16, 2 | lspsn0 20485 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β LMod β
((LSpanβπ)β{(0gβπ)}) =
{(0gβπ)}) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β ((LSpanβπ)β{(0gβπ)}) =
{(0gβπ)}) |
19 | 14, 18 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β ((LSpanβπ)β{π£}) = {(0gβπ)}) |
20 | 19 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β (π β ((LSpanβπ)β{π£})) = (π β
{(0gβπ)})) |
21 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β π β π) |
22 | 3 | lsssubg 20434 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
23 | 15, 21, 22 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β π β (SubGrpβπ)) |
24 | 16, 4 | lsm01 19460 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (SubGrpβπ) β (π β
{(0gβπ)})
= π) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β (π β
{(0gβπ)})
= π) |
26 | 20, 25 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β (π β ((LSpanβπ)β{π£})) = π) |
27 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β π β π) |
28 | 26, 27 | eqnetrd 3012 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π£ β π) β§ (π β π β§ π β π)) β§ π£ = (0gβπ)) β (π β ((LSpanβπ)β{π£})) β π) |
29 | 28 | ex 414 |
. . . . . . . . . . . . . 14
β’ (((π β§ π£ β π) β§ (π β π β§ π β π)) β (π£ = (0gβπ) β (π β ((LSpanβπ)β{π£})) β π)) |
30 | 29 | necon2d 2967 |
. . . . . . . . . . . . 13
β’ (((π β§ π£ β π) β§ (π β π β§ π β π)) β ((π β ((LSpanβπ)β{π£})) = π β π£ β (0gβπ))) |
31 | 30 | pm4.71rd 564 |
. . . . . . . . . . . 12
β’ (((π β§ π£ β π) β§ (π β π β§ π β π)) β ((π β ((LSpanβπ)β{π£})) = π β (π£ β (0gβπ) β§ (π β ((LSpanβπ)β{π£})) = π))) |
32 | 31 | pm5.32da 580 |
. . . . . . . . . . 11
β’ ((π β§ π£ β π) β (((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β ((π β π β§ π β π) β§ (π£ β (0gβπ) β§ (π β ((LSpanβπ)β{π£})) = π)))) |
33 | 32 | pm5.32da 580 |
. . . . . . . . . 10
β’ (π β ((π£ β π β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β (π£ β π β§ ((π β π β§ π β π) β§ (π£ β (0gβπ) β§ (π β ((LSpanβπ)β{π£})) = π))))) |
34 | | eldifsn 4752 |
. . . . . . . . . . . 12
β’ (π£ β (π β {(0gβπ)}) β (π£ β π β§ π£ β (0gβπ))) |
35 | 34 | anbi1i 625 |
. . . . . . . . . . 11
β’ ((π£ β (π β {(0gβπ)}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β ((π£ β π β§ π£ β (0gβπ)) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
36 | | anass 470 |
. . . . . . . . . . . 12
β’ (((π£ β π β§ π£ β (0gβπ)) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β (π£ β π β§ (π£ β (0gβπ) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)))) |
37 | | an12 644 |
. . . . . . . . . . . . 13
β’ ((π£ β (0gβπ) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β ((π β π β§ π β π) β§ (π£ β (0gβπ) β§ (π β ((LSpanβπ)β{π£})) = π))) |
38 | 37 | anbi2i 624 |
. . . . . . . . . . . 12
β’ ((π£ β π β§ (π£ β (0gβπ) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) β (π£ β π β§ ((π β π β§ π β π) β§ (π£ β (0gβπ) β§ (π β ((LSpanβπ)β{π£})) = π)))) |
39 | 36, 38 | bitri 275 |
. . . . . . . . . . 11
β’ (((π£ β π β§ π£ β (0gβπ)) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β (π£ β π β§ ((π β π β§ π β π) β§ (π£ β (0gβπ) β§ (π β ((LSpanβπ)β{π£})) = π)))) |
40 | 35, 39 | bitr2i 276 |
. . . . . . . . . 10
β’ ((π£ β π β§ ((π β π β§ π β π) β§ (π£ β (0gβπ) β§ (π β ((LSpanβπ)β{π£})) = π))) β (π£ β (π β {(0gβπ)}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
41 | 33, 40 | bitrdi 287 |
. . . . . . . . 9
β’ (π β ((π£ β π β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β (π£ β (π β {(0gβπ)}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)))) |
42 | 41 | exbidv 1925 |
. . . . . . . 8
β’ (π β (βπ£(π£ β π β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β βπ£(π£ β (π β {(0gβπ)}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)))) |
43 | 11, 42 | bitrid 283 |
. . . . . . 7
β’ (π β (βπ£ β π ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β βπ£(π£ β (π β {(0gβπ)}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)))) |
44 | | fvex 6860 |
. . . . . . . . . 10
β’
((LSpanβπ)β{π£}) β V |
45 | 44 | rexcom4b 3477 |
. . . . . . . . 9
β’
(βπβπ£ β (π β {(0gβπ)})(((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β§ π = ((LSpanβπ)β{π£})) β βπ£ β (π β {(0gβπ)})((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) |
46 | | df-rex 3075 |
. . . . . . . . 9
β’
(βπ£ β
(π β
{(0gβπ)})((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β βπ£(π£ β (π β {(0gβπ)}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
47 | 45, 46 | bitr2i 276 |
. . . . . . . 8
β’
(βπ£(π£ β (π β {(0gβπ)}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β βπβπ£ β (π β {(0gβπ)})(((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β§ π = ((LSpanβπ)β{π£}))) |
48 | | ancom 462 |
. . . . . . . . . 10
β’ ((((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β§ π = ((LSpanβπ)β{π£})) β (π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
49 | 48 | rexbii 3098 |
. . . . . . . . 9
β’
(βπ£ β
(π β
{(0gβπ)})(((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β§ π = ((LSpanβπ)β{π£})) β βπ£ β (π β {(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
50 | 49 | exbii 1851 |
. . . . . . . 8
β’
(βπβπ£ β (π β {(0gβπ)})(((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β§ π = ((LSpanβπ)β{π£})) β βπβπ£ β (π β {(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
51 | 47, 50 | bitri 275 |
. . . . . . 7
β’
(βπ£(π£ β (π β {(0gβπ)}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)) β βπβπ£ β (π β {(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
52 | 43, 51 | bitrdi 287 |
. . . . . 6
β’ (π β (βπ£ β π ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β βπβπ£ β (π β {(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π)))) |
53 | | r19.41v 3186 |
. . . . . . . 8
β’
(βπ£ β
(π β
{(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π)) β (βπ£ β (π β {(0gβπ)})π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π))) |
54 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = ((LSpanβπ)β{π£}) β (π β π) = (π β ((LSpanβπ)β{π£}))) |
55 | 54 | eqeq1d 2739 |
. . . . . . . . . . 11
β’ (π = ((LSpanβπ)β{π£}) β ((π β π) = π β (π β ((LSpanβπ)β{π£})) = π)) |
56 | 55 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = ((LSpanβπ)β{π£}) β (((π β π β§ π β π) β§ (π β π) = π) β ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
57 | 56 | pm5.32i 576 |
. . . . . . . . 9
β’ ((π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π)) β (π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
58 | 57 | rexbii 3098 |
. . . . . . . 8
β’
(βπ£ β
(π β
{(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π)) β βπ£ β (π β {(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
59 | 53, 58 | bitr3i 277 |
. . . . . . 7
β’
((βπ£ β
(π β
{(0gβπ)})π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π)) β βπ£ β (π β {(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
60 | 59 | exbii 1851 |
. . . . . 6
β’
(βπ(βπ£ β (π β {(0gβπ)})π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π)) β βπβπ£ β (π β {(0gβπ)})(π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π))) |
61 | 52, 60 | bitr4di 289 |
. . . . 5
β’ (π β (βπ£ β π ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β βπ(βπ£ β (π β {(0gβπ)})π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π)))) |
62 | | islshpat.a |
. . . . . . . . 9
β’ π΄ = (LSAtomsβπ) |
63 | 1, 2, 16, 62 | islsat 37482 |
. . . . . . . 8
β’ (π β LMod β (π β π΄ β βπ£ β (π β {(0gβπ)})π = ((LSpanβπ)β{π£}))) |
64 | 6, 63 | syl 17 |
. . . . . . 7
β’ (π β (π β π΄ β βπ£ β (π β {(0gβπ)})π = ((LSpanβπ)β{π£}))) |
65 | 64 | anbi1d 631 |
. . . . . 6
β’ (π β ((π β π΄ β§ ((π β π β§ π β π) β§ (π β π) = π)) β (βπ£ β (π β {(0gβπ)})π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π)))) |
66 | 65 | exbidv 1925 |
. . . . 5
β’ (π β (βπ(π β π΄ β§ ((π β π β§ π β π) β§ (π β π) = π)) β βπ(βπ£ β (π β {(0gβπ)})π = ((LSpanβπ)β{π£}) β§ ((π β π β§ π β π) β§ (π β π) = π)))) |
67 | 61, 66 | bitr4d 282 |
. . . 4
β’ (π β (βπ£ β π ((π β π β§ π β π) β§ (π β ((LSpanβπ)β{π£})) = π) β βπ(π β π΄ β§ ((π β π β§ π β π) β§ (π β π) = π)))) |
68 | 10, 67 | bitrid 283 |
. . 3
β’ (π β ((π β π β§ π β π β§ βπ£ β π (π β ((LSpanβπ)β{π£})) = π) β βπ(π β π΄ β§ ((π β π β§ π β π) β§ (π β π) = π)))) |
69 | | df-3an 1090 |
. . . 4
β’ ((π β π β§ π β π β§ βπ β π΄ (π β π) = π) β ((π β π β§ π β π) β§ βπ β π΄ (π β π) = π)) |
70 | | r19.42v 3188 |
. . . . 5
β’
(βπ β
π΄ ((π β π β§ π β π) β§ (π β π) = π) β ((π β π β§ π β π) β§ βπ β π΄ (π β π) = π)) |
71 | | df-rex 3075 |
. . . . 5
β’
(βπ β
π΄ ((π β π β§ π β π) β§ (π β π) = π) β βπ(π β π΄ β§ ((π β π β§ π β π) β§ (π β π) = π))) |
72 | 70, 71 | bitr3i 277 |
. . . 4
β’ (((π β π β§ π β π) β§ βπ β π΄ (π β π) = π) β βπ(π β π΄ β§ ((π β π β§ π β π) β§ (π β π) = π))) |
73 | 69, 72 | bitr2i 276 |
. . 3
β’
(βπ(π β π΄ β§ ((π β π β§ π β π) β§ (π β π) = π)) β (π β π β§ π β π β§ βπ β π΄ (π β π) = π)) |
74 | 68, 73 | bitrdi 287 |
. 2
β’ (π β ((π β π β§ π β π β§ βπ£ β π (π β ((LSpanβπ)β{π£})) = π) β (π β π β§ π β π β§ βπ β π΄ (π β π) = π))) |
75 | 7, 74 | bitrd 279 |
1
β’ (π β (π β π» β (π β π β§ π β π β§ βπ β π΄ (π β π) = π))) |