Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . 4
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })))) β π β (Baseβπ)) |
2 | | elpwg 4568 |
. . . . 5
β’ (π β π β (π β π« (Baseβπ) β π β (Baseβπ))) |
3 | 2 | ad2antrr 725 |
. . . 4
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })))) β (π β π« (Baseβπ) β π β (Baseβπ))) |
4 | 1, 3 | mpbird 257 |
. . 3
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })))) β π β π« (Baseβπ)) |
5 | | simplr 768 |
. . . . . . . . 9
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β π β LMod) |
6 | | ssdifss 4100 |
. . . . . . . . . . 11
β’ (π β (Baseβπ) β (π β {π }) β (Baseβπ)) |
7 | 6 | adantl 483 |
. . . . . . . . . 10
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (π β {π }) β (Baseβπ)) |
8 | | difexg 5289 |
. . . . . . . . . . . 12
β’ (π β π β (π β {π }) β V) |
9 | 8 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (π β {π }) β V) |
10 | | elpwg 4568 |
. . . . . . . . . . 11
β’ ((π β {π }) β V β ((π β {π }) β π« (Baseβπ) β (π β {π }) β (Baseβπ))) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β ((π β {π }) β π« (Baseβπ) β (π β {π }) β (Baseβπ))) |
12 | 7, 11 | mpbird 257 |
. . . . . . . . 9
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (π β {π }) β π« (Baseβπ)) |
13 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
14 | 13 | lspeqlco 46594 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β (π LinCo (π β {π })) = ((LSpanβπ)β(π β {π }))) |
15 | 14 | eleq2d 2824 |
. . . . . . . . . 10
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β ((π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β (π¦( Β·π
βπ)π ) β ((LSpanβπ)β(π β {π })))) |
16 | 15 | bicomd 222 |
. . . . . . . . 9
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β ((π¦( Β·π
βπ)π ) β ((LSpanβπ)β(π β {π })) β (π¦( Β·π
βπ)π ) β (π LinCo (π β {π })))) |
17 | 5, 12, 16 | syl2anc 585 |
. . . . . . . 8
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β ((π¦( Β·π
βπ)π ) β ((LSpanβπ)β(π β {π })) β (π¦( Β·π
βπ)π ) β (π LinCo (π β {π })))) |
18 | 17 | notbid 318 |
. . . . . . 7
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (Β¬ (π¦( Β·π
βπ)π ) β ((LSpanβπ)β(π β {π })) β Β¬ (π¦( Β·π
βπ)π ) β (π LinCo (π β {π })))) |
19 | | lindslinind.r |
. . . . . . . . . . . 12
β’ π
= (Scalarβπ) |
20 | | lindslinind.b |
. . . . . . . . . . . 12
β’ π΅ = (Baseβπ
) |
21 | 13, 19, 20 | lcoval 46567 |
. . . . . . . . . . 11
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β ((π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp (0gβπ
) β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
22 | | lindslinind.0 |
. . . . . . . . . . . . . . . 16
β’ 0 =
(0gβπ
) |
23 | 22 | eqcomi 2746 |
. . . . . . . . . . . . . . 15
β’
(0gβπ
) = 0 |
24 | 23 | breq2i 5118 |
. . . . . . . . . . . . . 14
β’ (π finSupp
(0gβπ
)
β π finSupp 0
) |
25 | 24 | anbi1i 625 |
. . . . . . . . . . . . 13
β’ ((π finSupp
(0gβπ
)
β§ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
26 | 25 | rexbii 3098 |
. . . . . . . . . . . 12
β’
(βπ β
(π΅ βm
(π β {π }))(π finSupp (0gβπ
) β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
27 | 26 | anbi2i 624 |
. . . . . . . . . . 11
β’ (((π¦(
Β·π βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp (0gβπ
) β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) |
28 | 21, 27 | bitrdi 287 |
. . . . . . . . . 10
β’ ((π β LMod β§ (π β {π }) β π« (Baseβπ)) β ((π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
29 | 5, 12, 28 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β ((π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
30 | 29 | notbid 318 |
. . . . . . . 8
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (Β¬ (π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β Β¬ ((π¦( Β·π
βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))))) |
31 | | ianor 981 |
. . . . . . . . 9
β’ (Β¬
((π¦(
Β·π βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β (Β¬ (π¦( Β·π
βπ)π ) β (Baseβπ) β¨ Β¬ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))))) |
32 | | ralnex 3076 |
. . . . . . . . . . 11
β’
(βπ β
(π΅ βm
(π β {π })) Β¬ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β Β¬ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) |
33 | | ianor 981 |
. . . . . . . . . . . 12
β’ (Β¬
(π finSupp 0 β§ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β (Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
34 | 33 | ralbii 3097 |
. . . . . . . . . . 11
β’
(βπ β
(π΅ βm
(π β {π })) Β¬ (π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
35 | 32, 34 | bitr3i 277 |
. . . . . . . . . 10
β’ (Β¬
βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π }))) β βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) |
36 | 35 | orbi2i 912 |
. . . . . . . . 9
β’ ((Β¬
(π¦(
Β·π βπ)π ) β (Baseβπ) β¨ Β¬ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β (Β¬ (π¦( Β·π
βπ)π ) β (Baseβπ) β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))) |
37 | 31, 36 | bitri 275 |
. . . . . . . 8
β’ (Β¬
((π¦(
Β·π βπ)π ) β (Baseβπ) β§ βπ β (π΅ βm (π β {π }))(π finSupp 0 β§ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })))) β (Β¬ (π¦( Β·π
βπ)π ) β (Baseβπ) β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))) |
38 | 30, 37 | bitrdi 287 |
. . . . . . 7
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (Β¬ (π¦( Β·π
βπ)π ) β (π LinCo (π β {π })) β (Β¬ (π¦( Β·π
βπ)π ) β (Baseβπ) β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))) |
39 | 18, 38 | bitrd 279 |
. . . . . 6
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (Β¬ (π¦( Β·π
βπ)π ) β ((LSpanβπ)β(π β {π })) β (Β¬ (π¦( Β·π
βπ)π ) β (Baseβπ) β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))) |
40 | 39 | 2ralbidv 3213 |
. . . . 5
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })) β βπ β π βπ¦ β (π΅ β { 0 })(Β¬ (π¦(
Β·π βπ)π ) β (Baseβπ) β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))) |
41 | | simpllr 775 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β π β LMod) |
42 | | eldifi 4091 |
. . . . . . . . . . . . 13
β’ (π¦ β (π΅ β { 0 }) β π¦ β π΅) |
43 | 42 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β π β§ π¦ β (π΅ β { 0 })) β π¦ β π΅) |
44 | 43 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β π¦ β π΅) |
45 | | ssel2 3944 |
. . . . . . . . . . . 12
β’ ((π β (Baseβπ) β§ π β π) β π β (Baseβπ)) |
46 | 45 | ad2ant2lr 747 |
. . . . . . . . . . 11
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β π β (Baseβπ)) |
47 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (
Β·π βπ) = ( Β·π
βπ) |
48 | 13, 19, 47, 20 | lmodvscl 20355 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π¦ β π΅ β§ π β (Baseβπ)) β (π¦( Β·π
βπ)π ) β (Baseβπ)) |
49 | 41, 44, 46, 48 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β (π¦(
Β·π βπ)π ) β (Baseβπ)) |
50 | 49 | notnotd 144 |
. . . . . . . . 9
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β Β¬ Β¬
(π¦(
Β·π βπ)π ) β (Baseβπ)) |
51 | | nbfal 1557 |
. . . . . . . . 9
β’ (Β¬
Β¬ (π¦(
Β·π βπ)π ) β (Baseβπ) β (Β¬ (π¦( Β·π
βπ)π ) β (Baseβπ) β β₯)) |
52 | 50, 51 | sylib 217 |
. . . . . . . 8
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β (Β¬ (π¦(
Β·π βπ)π ) β (Baseβπ) β β₯)) |
53 | 52 | orbi1d 916 |
. . . . . . 7
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ (π β π β§ π¦ β (π΅ β { 0 }))) β ((Β¬ (π¦(
Β·π βπ)π ) β (Baseβπ) β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β (β₯ β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))) |
54 | 53 | 2ralbidva 3211 |
. . . . . 6
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (βπ β π βπ¦ β (π΅ β { 0 })(Β¬ (π¦(
Β·π βπ)π ) β (Baseβπ) β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β βπ β π βπ¦ β (π΅ β { 0 })(β₯ β¨
βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))))) |
55 | | r19.32v 3189 |
. . . . . . . . 9
β’
(βπ¦ β
(π΅ β { 0 })(β₯
β¨ βπ β
(π΅ βm
(π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β (β₯ β¨ βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))) |
56 | 55 | ralbii 3097 |
. . . . . . . 8
β’
(βπ β
π βπ¦ β (π΅ β { 0 })(β₯ β¨
βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β βπ β π (β₯ β¨ βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))) |
57 | | r19.32v 3189 |
. . . . . . . 8
β’
(βπ β
π (β₯ β¨
βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β (β₯ β¨ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))) |
58 | 56, 57 | bitri 275 |
. . . . . . 7
β’
(βπ β
π βπ¦ β (π΅ β { 0 })(β₯ β¨
βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β (β₯ β¨ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))))) |
59 | | falim 1559 |
. . . . . . . . 9
β’ (β₯
β (((π β π β§ π β LMod) β§ π β (Baseβπ)) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
60 | | sneq 4601 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π₯ β {π } = {π₯}) |
61 | 60 | difeq2d 4087 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π₯ β (π β {π }) = (π β {π₯})) |
62 | 61 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π₯ β (π΅ βm (π β {π })) = (π΅ βm (π β {π₯}))) |
63 | | oveq2 7370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π₯ β (π¦( Β·π
βπ)π ) = (π¦( Β·π
βπ)π₯)) |
64 | 61 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π₯ β (π( linC βπ)(π β {π })) = (π( linC βπ)(π β {π₯}))) |
65 | 63, 64 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π₯ β ((π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })) β (π¦( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})))) |
66 | 65 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π₯ β (Β¬ (π¦( Β·π
βπ)π ) = (π( linC βπ)(π β {π })) β Β¬ (π¦( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})))) |
67 | 66 | orbi2d 915 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π₯ β ((Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β (Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))))) |
68 | 62, 67 | raleqbidv 3322 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π₯ β (βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))))) |
69 | 68 | ralbidv 3175 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π₯ β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))))) |
70 | 69 | rspcva 3582 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β π β§ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯})))) |
71 | | lindslinind.z |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (0gβπ) |
72 | 19, 20, 22, 71 | lindslinindsimp2lem5 46617 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 ))) |
73 | 72 | expr 458 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (π₯ β π β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 )))) |
74 | 73 | com14 96 |
. . . . . . . . . . . . . . . . . 18
β’
(βπ¦ β
(π΅ β { 0
})βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (π₯ β π β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (πβπ₯) = 0 )))) |
75 | 70, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π β§ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β (π₯ β π β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (πβπ₯) = 0 )))) |
76 | 75 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π β (βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β (π₯ β π β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (πβπ₯) = 0 ))))) |
77 | 76 | pm2.43a 54 |
. . . . . . . . . . . . . . 15
β’ (π₯ β π β (βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (πβπ₯) = 0 )))) |
78 | 77 | com14 96 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (π₯ β π β (πβπ₯) = 0 )))) |
79 | 78 | imp 408 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (π₯ β π β (πβπ₯) = 0 ))) |
80 | 79 | expdimp 454 |
. . . . . . . . . . . 12
β’
(((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β§ π β (π΅ βm π)) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β (π₯ β π β (πβπ₯) = 0 ))) |
81 | 80 | ralrimdv 3150 |
. . . . . . . . . . 11
β’
(((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β§ π β (π΅ βm π)) β ((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) |
82 | 81 | ralrimiva 3144 |
. . . . . . . . . 10
β’ ((((π β π β§ π β LMod) β§ π β (Baseβπ)) β§ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) |
83 | 82 | expcom 415 |
. . . . . . . . 9
β’
(βπ β
π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π }))) β (((π β π β§ π β LMod) β§ π β (Baseβπ)) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
84 | 59, 83 | jaoi 856 |
. . . . . . . 8
β’ ((β₯
β¨ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β (((π β π β§ π β LMod) β§ π β (Baseβπ)) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
85 | 84 | com12 32 |
. . . . . . 7
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β ((β₯ β¨ βπ β π βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
86 | 58, 85 | biimtrid 241 |
. . . . . 6
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (βπ β π βπ¦ β (π΅ β { 0 })(β₯ β¨
βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
87 | 54, 86 | sylbid 239 |
. . . . 5
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (βπ β π βπ¦ β (π΅ β { 0 })(Β¬ (π¦(
Β·π βπ)π ) β (Baseβπ) β¨ βπ β (π΅ βm (π β {π }))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π ) = (π( linC βπ)(π β {π })))) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
88 | 40, 87 | sylbid 239 |
. . . 4
β’ (((π β π β§ π β LMod) β§ π β (Baseβπ)) β (βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
89 | 88 | impr 456 |
. . 3
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })))) β βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )) |
90 | 4, 89 | jca 513 |
. 2
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π })))) β (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 ))) |
91 | 90 | ex 414 |
1
β’ ((π β π β§ π β LMod) β ((π β (Baseβπ) β§ βπ β π βπ¦ β (π΅ β { 0 }) Β¬ (π¦(
Β·π βπ)π ) β ((LSpanβπ)β(π β {π }))) β (π β π« (Baseβπ) β§ βπ β (π΅ βm π)((π finSupp 0 β§ (π( linC βπ)π) = π) β βπ₯ β π (πβπ₯) = 0 )))) |