Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . 3
β’ ((πβπ₯) = 0 β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 )) |
2 | 1 | 2a1d 26 |
. 2
β’ ((πβπ₯) = 0 β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 )))) |
3 | | elmapi 8794 |
. . . . . . . . . 10
β’ (π β (π΅ βm π) β π:πβΆπ΅) |
4 | | ffvelcdm 7037 |
. . . . . . . . . . . . . 14
β’ ((π:πβΆπ΅ β§ π₯ β π) β (πβπ₯) β π΅) |
5 | 4 | expcom 415 |
. . . . . . . . . . . . 13
β’ (π₯ β π β (π:πβΆπ΅ β (πβπ₯) β π΅)) |
6 | 5 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β (Baseβπ) β§ π₯ β π) β (π:πβΆπ΅ β (πβπ₯) β π΅)) |
7 | 6 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π:πβΆπ΅ β (πβπ₯) β π΅)) |
8 | 7 | com12 32 |
. . . . . . . . . 10
β’ (π:πβΆπ΅ β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (πβπ₯) β π΅)) |
9 | 3, 8 | syl 17 |
. . . . . . . . 9
β’ (π β (π΅ βm π) β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (πβπ₯) β π΅)) |
10 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (πβπ₯) β π΅)) |
11 | 10 | impcom 409 |
. . . . . . 7
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (πβπ₯) β π΅) |
12 | 11 | biantrurd 534 |
. . . . . 6
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β ((πβπ₯) β 0 β ((πβπ₯) β π΅ β§ (πβπ₯) β 0 ))) |
13 | | df-ne 2945 |
. . . . . . 7
β’ ((πβπ₯) β 0 β Β¬ (πβπ₯) = 0 ) |
14 | 13 | bicomi 223 |
. . . . . 6
β’ (Β¬
(πβπ₯) = 0 β (πβπ₯) β 0 ) |
15 | | eldifsn 4752 |
. . . . . 6
β’ ((πβπ₯) β (π΅ β { 0 }) β ((πβπ₯) β π΅ β§ (πβπ₯) β 0 )) |
16 | 12, 14, 15 | 3bitr4g 314 |
. . . . 5
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (Β¬ (πβπ₯) = 0 β (πβπ₯) β (π΅ β { 0 }))) |
17 | | lindslinind.r |
. . . . . . . . . . 11
β’ π
= (Scalarβπ) |
18 | 17 | lmodfgrp 20347 |
. . . . . . . . . 10
β’ (π β LMod β π
β Grp) |
19 | 18 | adantl 483 |
. . . . . . . . 9
β’ ((π β π β§ π β LMod) β π
β Grp) |
20 | 19 | adantr 482 |
. . . . . . . 8
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β π
β Grp) |
21 | 20 | adantr 482 |
. . . . . . 7
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β π
β Grp) |
22 | | lindslinind.b |
. . . . . . . 8
β’ π΅ = (Baseβπ
) |
23 | | lindslinind.0 |
. . . . . . . 8
β’ 0 =
(0gβπ
) |
24 | | eqid 2737 |
. . . . . . . 8
β’
(invgβπ
) = (invgβπ
) |
25 | 22, 23, 24 | grpinvnzcl 18826 |
. . . . . . 7
β’ ((π
β Grp β§ (πβπ₯) β (π΅ β { 0 })) β
((invgβπ
)β(πβπ₯)) β (π΅ β { 0 })) |
26 | 21, 25 | sylan 581 |
. . . . . 6
β’
(((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β§ (πβπ₯) β (π΅ β { 0 })) β
((invgβπ
)β(πβπ₯)) β (π΅ β { 0 })) |
27 | 26 | ex 414 |
. . . . 5
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β ((πβπ₯) β (π΅ β { 0 }) β
((invgβπ
)β(πβπ₯)) β (π΅ β { 0 }))) |
28 | 16, 27 | sylbid 239 |
. . . 4
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (Β¬ (πβπ₯) = 0 β
((invgβπ
)β(πβπ₯)) β (π΅ β { 0 }))) |
29 | | oveq1 7369 |
. . . . . . . . . . 11
β’ (π¦ = ((invgβπ
)β(πβπ₯)) β (π¦( Β·π
βπ)π₯) = (((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯)) |
30 | 29 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π¦ = ((invgβπ
)β(πβπ₯)) β ((π¦( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})) β (((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})))) |
31 | 30 | notbid 318 |
. . . . . . . . 9
β’ (π¦ = ((invgβπ
)β(πβπ₯)) β (Β¬ (π¦( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})) β Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})))) |
32 | 31 | orbi2d 915 |
. . . . . . . 8
β’ (π¦ = ((invgβπ
)β(πβπ₯)) β ((Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯}))))) |
33 | 32 | ralbidv 3175 |
. . . . . . 7
β’ (π¦ = ((invgβπ
)β(πβπ₯)) β (βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯}))))) |
34 | 33 | rspcva 3582 |
. . . . . 6
β’
((((invgβπ
)β(πβπ₯)) β (π΅ β { 0 }) β§ βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯})))) β βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})))) |
35 | | simpl 484 |
. . . . . . . . 9
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β π β§ π β LMod)) |
36 | 35 | adantr 482 |
. . . . . . . 8
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π β π β§ π β LMod)) |
37 | | simplrl 776 |
. . . . . . . 8
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β π β (Baseβπ)) |
38 | | simplrr 777 |
. . . . . . . 8
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β π₯ β π) |
39 | | simpl 484 |
. . . . . . . . 9
β’ ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β π β (π΅ βm π)) |
40 | 39 | adantl 483 |
. . . . . . . 8
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β π β (π΅ βm π)) |
41 | | lindslinind.z |
. . . . . . . . 9
β’ π = (0gβπ) |
42 | | eqid 2737 |
. . . . . . . . 9
β’
((invgβπ
)β(πβπ₯)) = ((invgβπ
)β(πβπ₯)) |
43 | | eqid 2737 |
. . . . . . . . 9
β’ (π βΎ (π β {π₯})) = (π βΎ (π β {π₯})) |
44 | 17, 22, 23, 41, 42, 43 | lindslinindimp2lem2 46614 |
. . . . . . . 8
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π β§ π β (π΅ βm π))) β (π βΎ (π β {π₯})) β (π΅ βm (π β {π₯}))) |
45 | 36, 37, 38, 40, 44 | syl13anc 1373 |
. . . . . . 7
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π βΎ (π β {π₯})) β (π΅ βm (π β {π₯}))) |
46 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (π β {π₯})) β π = (π βΎ (π β {π₯}))) |
47 | 23 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (π β {π₯})) β 0 =
(0gβπ
)) |
48 | 46, 47 | breq12d 5123 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ (π β {π₯})) β (π finSupp 0 β (π βΎ (π β {π₯})) finSupp (0gβπ
))) |
49 | 48 | notbid 318 |
. . . . . . . . . . . 12
β’ (π = (π βΎ (π β {π₯})) β (Β¬ π finSupp 0 β Β¬ (π βΎ (π β {π₯})) finSupp (0gβπ
))) |
50 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π = (π βΎ (π β {π₯})) β (π( linC βπ)(π β {π₯})) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯}))) |
51 | 50 | eqeq2d 2748 |
. . . . . . . . . . . . 13
β’ (π = (π βΎ (π β {π₯})) β ((((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})) β (((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯})))) |
52 | 51 | notbid 318 |
. . . . . . . . . . . 12
β’ (π = (π βΎ (π β {π₯})) β (Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})) β Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯})))) |
53 | 49, 52 | orbi12d 918 |
. . . . . . . . . . 11
β’ (π = (π βΎ (π β {π₯})) β ((Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (Β¬ (π βΎ (π β {π₯})) finSupp (0gβπ
) β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯}))))) |
54 | 53 | rspcva 3582 |
. . . . . . . . . 10
β’ (((π βΎ (π β {π₯})) β (π΅ βm (π β {π₯})) β§ βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})))) β (Β¬ (π βΎ (π β {π₯})) finSupp (0gβπ
) β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯})))) |
55 | 23 | breq2i 5118 |
. . . . . . . . . . . . . . . . . 18
β’ (π finSupp 0 β π finSupp (0gβπ
)) |
56 | 55 | biimpi 215 |
. . . . . . . . . . . . . . . . 17
β’ (π finSupp 0 β π finSupp (0gβπ
)) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π finSupp 0 β§ (π( linC βπ)π) = π) β π finSupp (0gβπ
)) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β π finSupp (0gβπ
)) |
59 | 58 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β π finSupp (0gβπ
)) |
60 | | fvexd 6862 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (0gβπ
) β V) |
61 | 59, 60 | fsuppres 9337 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π βΎ (π β {π₯})) finSupp (0gβπ
)) |
62 | 61 | pm2.24d 151 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (Β¬ (π βΎ (π β {π₯})) finSupp (0gβπ
) β (πβπ₯) = 0 )) |
63 | 62 | com12 32 |
. . . . . . . . . . 11
β’ (Β¬
(π βΎ (π β {π₯})) finSupp (0gβπ
) β ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (πβπ₯) = 0 )) |
64 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β π β LMod) |
65 | 64 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β π β LMod) |
66 | 17 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβπ
) =
(Baseβ(Scalarβπ)) |
67 | 22, 66 | eqtr2i 2766 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβ(Scalarβπ)) = π΅ |
68 | 67 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
β’
((Baseβ(Scalarβπ)) βm (π β {π₯})) = (π΅ βm (π β {π₯})) |
69 | 45, 68 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π βΎ (π β {π₯})) β ((Baseβ(Scalarβπ)) βm (π β {π₯}))) |
70 | | ssdifss 4100 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (Baseβπ) β (π β {π₯}) β (Baseβπ)) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (Baseβπ) β§ π₯ β π) β (π β {π₯}) β (Baseβπ)) |
72 | 71 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β {π₯}) β (Baseβπ)) |
73 | | difexg 5289 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (π β {π₯}) β V) |
74 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π β§ π β LMod) β (π β {π₯}) β V) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β {π₯}) β V) |
76 | | elpwg 4568 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β {π₯}) β V β ((π β {π₯}) β π« (Baseβπ) β (π β {π₯}) β (Baseβπ))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π β {π₯}) β π« (Baseβπ) β (π β {π₯}) β (Baseβπ))) |
78 | 72, 77 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β (π β {π₯}) β π« (Baseβπ)) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π β {π₯}) β π« (Baseβπ)) |
80 | | lincval 46564 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ (π βΎ (π β {π₯})) β ((Baseβ(Scalarβπ)) βm (π β {π₯})) β§ (π β {π₯}) β π« (Baseβπ)) β ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯})) = (π Ξ£g (π§ β (π β {π₯}) β¦ (((π βΎ (π β {π₯}))βπ§)( Β·π
βπ)π§)))) |
81 | 65, 69, 79, 80 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯})) = (π Ξ£g (π§ β (π β {π₯}) β¦ (((π βΎ (π β {π₯}))βπ§)( Β·π
βπ)π§)))) |
82 | | fvres 6866 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β (π β {π₯}) β ((π βΎ (π β {π₯}))βπ§) = (πβπ§)) |
83 | 82 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β§ π§ β (π β {π₯})) β ((π βΎ (π β {π₯}))βπ§) = (πβπ§)) |
84 | 83 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
β’
(((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β§ π§ β (π β {π₯})) β (((π βΎ (π β {π₯}))βπ§)( Β·π
βπ)π§) = ((πβπ§)( Β·π
βπ)π§)) |
85 | 84 | mpteq2dva 5210 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π§ β (π β {π₯}) β¦ (((π βΎ (π β {π₯}))βπ§)( Β·π
βπ)π§)) = (π§ β (π β {π₯}) β¦ ((πβπ§)( Β·π
βπ)π§))) |
86 | 85 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π Ξ£g (π§ β (π β {π₯}) β¦ (((π βΎ (π β {π₯}))βπ§)( Β·π
βπ)π§))) = (π Ξ£g (π§ β (π β {π₯}) β¦ ((πβπ§)( Β·π
βπ)π§)))) |
87 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π β (Baseβπ) β§ π₯ β π)) |
88 | | 3anass 1096 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π) β (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) |
89 | 88 | bicomi 223 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π)) |
90 | 89 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π)) |
91 | 90 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π)) |
92 | 17, 22, 23, 41, 42, 43 | lindslinindimp2lem4 46616 |
. . . . . . . . . . . . . . 15
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π) β§ (π β (π΅ βm π) β§ π finSupp 0 β§ (π( linC βπ)π) = π)) β (π Ξ£g (π§ β (π β {π₯}) β¦ ((πβπ§)( Β·π
βπ)π§))) = (((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯)) |
93 | 36, 87, 91, 92 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (π Ξ£g (π§ β (π β {π₯}) β¦ ((πβπ§)( Β·π
βπ)π§))) = (((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯)) |
94 | 81, 86, 93 | 3eqtrrd 2782 |
. . . . . . . . . . . . 13
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯}))) |
95 | 94 | pm2.24d 151 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯})) β (πβπ₯) = 0 )) |
96 | 95 | com12 32 |
. . . . . . . . . . 11
β’ (Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯})) β ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (πβπ₯) = 0 )) |
97 | 63, 96 | jaoi 856 |
. . . . . . . . . 10
β’ ((Β¬
(π βΎ (π β {π₯})) finSupp (0gβπ
) β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = ((π βΎ (π β {π₯}))( linC βπ)(π β {π₯}))) β ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (πβπ₯) = 0 )) |
98 | 54, 97 | syl 17 |
. . . . . . . . 9
β’ (((π βΎ (π β {π₯})) β (π΅ βm (π β {π₯})) β§ βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯})))) β ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (πβπ₯) = 0 )) |
99 | 98 | ex 414 |
. . . . . . . 8
β’ ((π βΎ (π β {π₯})) β (π΅ βm (π β {π₯})) β (βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯}))) β ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (πβπ₯) = 0 ))) |
100 | 99 | com23 86 |
. . . . . . 7
β’ ((π βΎ (π β {π₯})) β (π΅ βm (π β {π₯})) β ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 ))) |
101 | 45, 100 | mpcom 38 |
. . . . . 6
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬
(((invgβπ
)β(πβπ₯))( Β·π
βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 )) |
102 | 34, 101 | syl5 34 |
. . . . 5
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β ((((invgβπ
)β(πβπ₯)) β (π΅ β { 0 }) β§ βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯})))) β (πβπ₯) = 0 )) |
103 | 102 | expd 417 |
. . . 4
β’ ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (((invgβπ
)β(πβπ₯)) β (π΅ β { 0 }) β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 ))) |
104 | 28, 103 | syldc 48 |
. . 3
β’ (Β¬
(πβπ₯) = 0 β ((((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β§ (π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π))) β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 ))) |
105 | 104 | expd 417 |
. 2
β’ (Β¬
(πβπ₯) = 0 β (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 )))) |
106 | 2, 105 | pm2.61i 182 |
1
β’ (((π β π β§ π β LMod) β§ (π β (Baseβπ) β§ π₯ β π)) β ((π β (π΅ βm π) β§ (π finSupp 0 β§ (π( linC βπ)π) = π)) β (βπ¦ β (π΅ β { 0 })βπ β (π΅ βm (π β {π₯}))(Β¬ π finSupp 0 β¨ Β¬ (π¦(
Β·π βπ)π₯) = (π( linC βπ)(π β {π₯}))) β (πβπ₯) = 0 ))) |