Step | Hyp | Ref
| Expression |
1 | | elpwi 4572 |
. . . 4
β’ (π β π«
(Baseβπ) β π β (Baseβπ)) |
2 | 1 | ad2antrl 727 |
. . 3
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β π β (Baseβπ)) |
3 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π β§ π β LMod) β π β LMod) |
4 | 3 | anim2i 618 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β (π β π« (Baseβπ) β§ π β LMod)) |
5 | 4 | ancomd 463 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β (π β LMod β§ π β π« (Baseβπ))) |
6 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (π β LMod β§ π β π« (Baseβπ))) |
7 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β (π΅ β { 0 }) β π¦ β π΅) |
8 | 7 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π β§ π¦ β (π΅ β { 0 })) β π¦ β π΅) |
9 | 8 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β π¦ β π΅) |
10 | 9 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β π¦ β π΅) |
11 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β π β π) |
12 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β π β π) |
13 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β π β (π΅ βm (π β {π }))) |
14 | 10, 12, 13 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (π¦ β π΅ β§ π β π β§ π β (π΅ βm (π β {π })))) |
15 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β π finSupp 0 ) |
16 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(Baseβπ) =
(Baseβπ) |
17 | | lindslinind.r |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π
= (Scalarβπ) |
18 | | lindslinind.b |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π΅ = (Baseβπ
) |
19 | | lindslinind.0 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 =
(0gβπ
) |
20 | | lindslinind.z |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π = (0gβπ) |
21 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(invgβπ
) = (invgβπ
) |
22 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) |
23 | 16, 17, 18, 19, 20, 21, 22 | lincext2 46610 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π¦ β π΅ β§ π β π β§ π β (π΅ βm (π β {π }))) β§ π finSupp 0 ) β (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) finSupp 0 ) |
24 | 6, 14, 15, 23 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) finSupp 0 ) |
25 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β (π β π«
(Baseβπ) β§ π β LMod)) |
26 | 25 | ancomd 463 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β (π β LMod β§ π β π«
(Baseβπ))) |
27 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (π β LMod β§ π β π« (Baseβπ))) |
28 | 16, 17, 18, 19, 20, 21, 22 | lincext1 46609 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π¦ β π΅ β§ π β π β§ π β (π΅ βm (π β {π })))) β (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β (π΅ βm π)) |
29 | 27, 14, 28 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β (π΅ βm π)) |
30 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β (π finSupp 0 β (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) finSupp 0 )) |
31 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β (π( linC βπ)π) = ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π)) |
32 | 31 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β ((π( linC βπ)π) = π β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π)) |
33 | 30, 32 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π))) |
34 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β (πβπ₯) = ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯)) |
35 | 34 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β ((πβπ₯) = 0 β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 )) |
36 | 35 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β (βπ₯ β π (πβπ₯) = 0 β βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 )) |
37 | 33, 36 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β (((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β (((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π) β βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 ))) |
38 | 37 | rspcv 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) β (π΅ βm π) β (βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β (((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π) β βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 ))) |
39 | 29, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β (((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) finSupp 0 β§ ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π) β βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 ))) |
40 | 39 | exp4a 433 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) finSupp 0 β (((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π β βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 )))) |
41 | 24, 40 | mpid 44 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β (((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π β βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 ))) |
42 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
43 | 16, 17, 18, 19, 20, 21, 22 | lincext3 46611 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§
(π¦ β π΅ β§ π β π β§ π β (π΅ βm (π β {π }))) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π) |
44 | 6, 14, 42, 43 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π) |
45 | | fveqeq2 6856 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π₯ = π β (((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ ) = 0 )) |
46 | 45 | rspcv 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β (βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ ) = 0 )) |
47 | 12, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ ) = 0 )) |
48 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§))) = (π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))) |
49 | | iftrue 4497 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ = π β if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)) = ((invgβπ
)βπ¦)) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ π§ = π ) β if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)) = ((invgβπ
)βπ¦)) |
51 | | fvexd 6862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β
((invgβπ
)βπ¦) β V) |
52 | 48, 50, 11, 51 | fvmptd 6960 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ ) = ((invgβπ
)βπ¦)) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ ) = ((invgβπ
)βπ¦)) |
54 | 53 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ ) = 0 β
((invgβπ
)βπ¦) = 0 )) |
55 | 17 | lmodfgrp 20347 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β LMod β π
β Grp) |
56 | 18, 19, 21 | grpinvnzcl 18826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π
β Grp β§ π¦ β (π΅ β { 0 })) β
((invgβπ
)βπ¦) β (π΅ β { 0 })) |
57 | | eldif 3925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((invgβπ
)βπ¦) β (π΅ β { 0 }) β
(((invgβπ
)βπ¦) β π΅ β§ Β¬ ((invgβπ
)βπ¦) β { 0 })) |
58 | | fvex 6860 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((invgβπ
)βπ¦) β V |
59 | 58 | elsn 4606 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((invgβπ
)βπ¦) β { 0 } β
((invgβπ
)βπ¦) = 0 ) |
60 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (Β¬
((invgβπ
)βπ¦) = 0 β
(((invgβπ
)βπ¦) = 0 β (π β π β (π β π β (π β π« (Baseβπ) β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))))) |
61 | 60 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (Β¬
((invgβπ
)βπ¦) = 0 β (π β π« (Baseβπ) β (π β π β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))))) |
62 | 59, 61 | sylnbi 330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (Β¬
((invgβπ
)βπ¦) β { 0 } β (π β π«
(Baseβπ) β
(π β π β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))))) |
63 | 57, 62 | simplbiim 506 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((invgβπ
)βπ¦) β (π΅ β { 0 }) β (π β π«
(Baseβπ) β
(π β π β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))))) |
64 | 56, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π
β Grp β§ π¦ β (π΅ β { 0 })) β (π β π«
(Baseβπ) β
(π β π β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))))) |
65 | 64 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π
β Grp β (π¦ β (π΅ β { 0 }) β (π β π«
(Baseβπ) β
(π β π β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))))) |
66 | 55, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β LMod β (π¦ β (π΅ β { 0 }) β (π β π«
(Baseβπ) β
(π β π β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))))) |
67 | 66 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β LMod β (π β π β (π β π« (Baseβπ) β (π¦ β (π΅ β { 0 }) β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))))) |
68 | 67 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β π β§ π β LMod) β (π β π« (Baseβπ) β (π¦ β (π΅ β { 0 }) β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))))) |
69 | 68 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β (π¦ β (π΅ β { 0 }) β (π β π β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))) |
70 | 69 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β (π¦ β (π΅ β { 0 }) β ((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β
(((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))) |
71 | 70 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π β§ π¦ β (π΅ β { 0 })) β ((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β
(((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))) |
72 | 71 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β
(((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
73 | 72 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (((invgβπ
)βπ¦) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
74 | 54, 73 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ ) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
75 | 47, 74 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β (βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
76 | 44, 75 | embantd 59 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β ((((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))( linC βπ)π) = π β βπ₯ β π ((π§ β π β¦ if(π§ = π , ((invgβπ
)βπ¦), (πβπ§)))βπ₯) = 0 ) β Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
77 | 41, 76 | syldc 48 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ β
(π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β ((((π β π«
(Baseβπ) β§ (π β π β§ π β LMod)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ (π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
78 | 77 | exp5j 447 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ) β (π β π«
(Baseβπ) β
((π β π β§ π β LMod) β ((π β π β§ π¦ β (π΅ β { 0 })) β ((π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))))) |
79 | 78 | impcom 409 |
. . . . . . . . . . . . . . . 16
β’ ((π β π«
(Baseβπ) β§
βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) β ((π β π β§ π β LMod) β ((π β π β§ π¦ β (π΅ β { 0 })) β ((π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
80 | 79 | impcom 409 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β ((π β π β§ π¦ β (π΅ β { 0 })) β ((π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) |
81 | 80 | imp 408 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β ((π β (π΅ βm (π β {π })) β§ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
82 | 81 | expdimp 454 |
. . . . . . . . . . . . 13
β’
(((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ π β (π΅ βm (π β {π }))) β ((π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
83 | 82 | expd 417 |
. . . . . . . . . . . 12
β’
(((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ π β (π΅ βm (π β {π }))) β (π finSupp 0 β ((π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) |
84 | 83 | impcom 409 |
. . . . . . . . . . 11
β’ ((π finSupp 0 β§ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ π β (π΅ βm (π β {π })))) β ((π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
85 | 84 | pm2.01d 189 |
. . . . . . . . . 10
β’ ((π finSupp 0 β§ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ π β (π΅ βm (π β {π })))) β Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) |
86 | 85 | olcd 873 |
. . . . . . . . 9
β’ ((π finSupp 0 β§ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ π β (π΅ βm (π β {π })))) β (Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
87 | | animorl 977 |
. . . . . . . . 9
β’ ((Β¬
π finSupp 0 β§
((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ π β (π΅ βm (π β {π })))) β (Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
88 | 86, 87 | pm2.61ian 811 |
. . . . . . . 8
β’
(((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β§ π β (π΅ βm (π β {π }))) β (Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
89 | 88 | ralrimiva 3144 |
. . . . . . 7
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
90 | | ralnex 3076 |
. . . . . . . 8
β’
(βπ β
(π΅ βm
(π β {π })) Β¬ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β Β¬ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
91 | | ianor 981 |
. . . . . . . . 9
β’ (Β¬
(π finSupp 0 β§ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β (Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
92 | 91 | ralbii 3097 |
. . . . . . . 8
β’
(βπ β
(π΅ βm
(π β {π })) Β¬ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
93 | 90, 92 | bitr3i 277 |
. . . . . . 7
β’ (Β¬
βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
94 | 89, 93 | sylibr 233 |
. . . . . 6
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β Β¬
βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
95 | 94 | intnand 490 |
. . . . 5
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β Β¬ ((π¦(
Β·π βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) |
96 | 3 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β π β LMod) |
97 | | difexg 5289 |
. . . . . . . . . 10
β’ (π β π β (π β {π }) β V) |
98 | 97 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β (π β {π }) β V) |
99 | 1 | ssdifssd 4107 |
. . . . . . . . . 10
β’ (π β π«
(Baseβπ) β
(π β {π }) β (Baseβπ)) |
100 | 99 | ad2antrl 727 |
. . . . . . . . 9
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β (π β {π }) β (Baseβπ)) |
101 | 98, 100 | elpwd 4571 |
. . . . . . . 8
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β (π β {π }) β π« (Baseβπ)) |
102 | 101 | adantr 482 |
. . . . . . 7
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β (π β {π }) β π« (Baseβπ)) |
103 | 16 | lspeqlco 46594 |
. . . . . . . . 9
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β (π LinCo (π β {π })) = ((LSpanβπ)β(π β {π }))) |
104 | 103 | eleq2d 2824 |
. . . . . . . 8
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β ((π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β (π¦( Β·π
βπ)π ) β ((LSpanβπ)β(π β {π })))) |
105 | 104 | bicomd 222 |
. . . . . . 7
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β ((π¦( Β·π
βπ)π ) β ((LSpanβπ)β(π β {π })) β (π¦( Β·π
βπ)π ) β (π LinCo (π β {π })))) |
106 | 96, 102, 105 | syl2anc 585 |
. . . . . 6
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β ((π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })) β (π¦( Β·π
βπ)π ) β (π LinCo (π β {π })))) |
107 | 3 | adantr 482 |
. . . . . . . . 9
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β π β LMod) |
108 | | difexg 5289 |
. . . . . . . . . . 11
β’ (π β π«
(Baseβπ) β
(π β {π }) β V) |
109 | 108, 99 | elpwd 4571 |
. . . . . . . . . 10
β’ (π β π«
(Baseβπ) β
(π β {π }) β π«
(Baseβπ)) |
110 | 109 | ad2antrl 727 |
. . . . . . . . 9
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β (π β {π }) β π« (Baseβπ)) |
111 | 107, 110 | jca 513 |
. . . . . . . 8
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β (π β LMod β§ (π β {π }) β π« (Baseβπ))) |
112 | 111 | adantr 482 |
. . . . . . 7
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β (π β LMod β§ (π β {π }) β π« (Baseβπ))) |
113 | 16, 17, 18 | lcoval 46567 |
. . . . . . . 8
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β ((π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp (0gβπ
) β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
114 | 19 | eqcomi 2746 |
. . . . . . . . . . . 12
β’
(0gβπ
) = 0 |
115 | 114 | breq2i 5118 |
. . . . . . . . . . 11
β’ (π finSupp
(0gβπ
)
β π finSupp 0
) |
116 | 115 | anbi1i 625 |
. . . . . . . . . 10
β’ ((π finSupp
(0gβπ
)
β§ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
117 | 116 | rexbii 3098 |
. . . . . . . . 9
β’
(βπ β
(π΅ βm
(π β {π }))(π finSupp (0gβπ
) β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
118 | 117 | anbi2i 624 |
. . . . . . . 8
β’ (((π¦(
Β·π βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp (0gβπ
) β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) |
119 | 113, 118 | bitrdi 287 |
. . . . . . 7
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β ((π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
120 | 112, 119 | syl 17 |
. . . . . 6
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β ((π¦(
Β·π βπ)π ) β (π LinCo (π β {π })) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
121 | 106, 120 | bitrd 279 |
. . . . 5
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β ((π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
122 | 95, 121 | mtbird 325 |
. . . 4
β’ ((((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π }))) |
123 | 122 | ralrimivva 3198 |
. . 3
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π }))) |
124 | 2, 123 | jca 513 |
. 2
β’ (((π β π β§ π β LMod) β§ (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) β (π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })))) |
125 | 124 | ex 414 |
1
β’ ((π β π β§ π β LMod) β ((π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) β (π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π }))))) |