Step | Hyp | Ref
| Expression |
1 | | islinds5.b |
. . . 4
β’ π΅ = (Baseβπ) |
2 | 1 | islinds 21231 |
. . 3
β’ (π β LMod β (π β (LIndSβπ) β (π β π΅ β§ ( I βΎ π) LIndF π))) |
3 | 2 | baibd 541 |
. 2
β’ ((π β LMod β§ π β π΅) β (π β (LIndSβπ) β ( I βΎ π) LIndF π)) |
4 | | simpl 484 |
. . 3
β’ ((π β LMod β§ π β π΅) β π β LMod) |
5 | 1 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
6 | 5 | a1i 11 |
. . . 4
β’ ((π β LMod β§ π β π΅) β π΅ β V) |
7 | | simpr 486 |
. . . 4
β’ ((π β LMod β§ π β π΅) β π β π΅) |
8 | 6, 7 | ssexd 5282 |
. . 3
β’ ((π β LMod β§ π β π΅) β π β V) |
9 | | f1oi 6823 |
. . . . 5
β’ ( I
βΎ π):πβ1-1-ontoβπ |
10 | | f1of 6785 |
. . . . 5
β’ (( I
βΎ π):πβ1-1-ontoβπ β ( I βΎ π):πβΆπ) |
11 | 9, 10 | mp1i 13 |
. . . 4
β’ ((π β LMod β§ π β π΅) β ( I βΎ π):πβΆπ) |
12 | 11, 7 | fssd 6687 |
. . 3
β’ ((π β LMod β§ π β π΅) β ( I βΎ π):πβΆπ΅) |
13 | | islinds5.r |
. . . 4
β’ πΉ = (Scalarβπ) |
14 | | islinds5.t |
. . . 4
β’ Β· = (
Β·π βπ) |
15 | | islinds5.z |
. . . 4
β’ π = (0gβπ) |
16 | | islinds5.y |
. . . 4
β’ 0 =
(0gβπΉ) |
17 | | eqid 2733 |
. . . 4
β’
(Baseβ(πΉ
freeLMod π)) =
(Baseβ(πΉ freeLMod
π)) |
18 | 1, 13, 14, 15, 16, 17 | islindf4 21260 |
. . 3
β’ ((π β LMod β§ π β V β§ ( I βΎ
π):πβΆπ΅) β (( I βΎ π) LIndF π β βπ β (Baseβ(πΉ freeLMod π))((π Ξ£g (π βf Β· ( I
βΎ π))) = π β π = (π Γ { 0 })))) |
19 | 4, 8, 12, 18 | syl3anc 1372 |
. 2
β’ ((π β LMod β§ π β π΅) β (( I βΎ π) LIndF π β βπ β (Baseβ(πΉ freeLMod π))((π Ξ£g (π βf Β· ( I
βΎ π))) = π β π = (π Γ { 0 })))) |
20 | 13 | fvexi 6857 |
. . . . . 6
β’ πΉ β V |
21 | | eqid 2733 |
. . . . . . 7
β’ (πΉ freeLMod π) = (πΉ freeLMod π) |
22 | | islinds5.k |
. . . . . . 7
β’ πΎ = (BaseβπΉ) |
23 | 21, 22, 16, 17 | frlmelbas 21178 |
. . . . . 6
β’ ((πΉ β V β§ π β V) β (π β (Baseβ(πΉ freeLMod π)) β (π β (πΎ βm π) β§ π finSupp 0 ))) |
24 | 20, 8, 23 | sylancr 588 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β (π β (Baseβ(πΉ freeLMod π)) β (π β (πΎ βm π) β§ π finSupp 0 ))) |
25 | 24 | imbi1d 342 |
. . . 4
β’ ((π β LMod β§ π β π΅) β ((π β (Baseβ(πΉ freeLMod π)) β ((π Ξ£g (π βf Β· ( I
βΎ π))) = π β π = (π Γ { 0 }))) β ((π β (πΎ βm π) β§ π finSupp 0 ) β ((π Ξ£g
(π βf
Β·
( I βΎ π))) = π β π = (π Γ { 0 }))))) |
26 | | elmapfn 8806 |
. . . . . . . . . 10
β’ (π β (πΎ βm π) β π Fn π) |
27 | 26 | ad2antrl 727 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β π Fn π) |
28 | 12 | adantr 482 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β ( I βΎ
π):πβΆπ΅) |
29 | 28 | ffnd 6670 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β ( I βΎ
π) Fn π) |
30 | 8 | adantr 482 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β π β V) |
31 | | inidm 4179 |
. . . . . . . . 9
β’ (π β© π) = π |
32 | | eqidd 2734 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β§ π£ β π) β (πβπ£) = (πβπ£)) |
33 | | fvresi 7120 |
. . . . . . . . . 10
β’ (π£ β π β (( I βΎ π)βπ£) = π£) |
34 | 33 | adantl 483 |
. . . . . . . . 9
β’ ((((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β§ π£ β π) β (( I βΎ π)βπ£) = π£) |
35 | 27, 29, 30, 30, 31, 32, 34 | offval 7627 |
. . . . . . . 8
β’ (((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β (π βf Β· ( I
βΎ π)) = (π£ β π β¦ ((πβπ£) Β· π£))) |
36 | 35 | oveq2d 7374 |
. . . . . . 7
β’ (((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β (π Ξ£g
(π βf
Β·
( I βΎ π))) = (π Ξ£g
(π£ β π β¦ ((πβπ£) Β· π£)))) |
37 | 36 | eqeq1d 2735 |
. . . . . 6
β’ (((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β ((π Ξ£g
(π βf
Β·
( I βΎ π))) = π β (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π)) |
38 | 37 | imbi1d 342 |
. . . . 5
β’ (((π β LMod β§ π β π΅) β§ (π β (πΎ βm π) β§ π finSupp 0 )) β (((π Ξ£g
(π βf
Β·
( I βΎ π))) = π β π = (π Γ { 0 })) β ((π Ξ£g
(π£ β π β¦ ((πβπ£) Β· π£))) = π β π = (π Γ { 0 })))) |
39 | 38 | pm5.74da 803 |
. . . 4
β’ ((π β LMod β§ π β π΅) β (((π β (πΎ βm π) β§ π finSupp 0 ) β ((π Ξ£g
(π βf
Β·
( I βΎ π))) = π β π = (π Γ { 0 }))) β ((π β (πΎ βm π) β§ π finSupp 0 ) β ((π Ξ£g
(π£ β π β¦ ((πβπ£) Β· π£))) = π β π = (π Γ { 0 }))))) |
40 | | impexp 452 |
. . . . . 6
β’ (((π β (πΎ βm π) β§ π finSupp 0 ) β ((π Ξ£g
(π£ β π β¦ ((πβπ£) Β· π£))) = π β π = (π Γ { 0 }))) β (π β (πΎ βm π) β (π finSupp 0 β ((π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π β π = (π Γ { 0 }))))) |
41 | | impexp 452 |
. . . . . . 7
β’ (((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 })) β (π finSupp 0 β ((π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π β π = (π Γ { 0 })))) |
42 | 41 | imbi2i 336 |
. . . . . 6
β’ ((π β (πΎ βm π) β ((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 }))) β (π β (πΎ βm π) β (π finSupp 0 β ((π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π β π = (π Γ { 0 }))))) |
43 | 40, 42 | bitr4i 278 |
. . . . 5
β’ (((π β (πΎ βm π) β§ π finSupp 0 ) β ((π Ξ£g
(π£ β π β¦ ((πβπ£) Β· π£))) = π β π = (π Γ { 0 }))) β (π β (πΎ βm π) β ((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 })))) |
44 | 43 | a1i 11 |
. . . 4
β’ ((π β LMod β§ π β π΅) β (((π β (πΎ βm π) β§ π finSupp 0 ) β ((π Ξ£g
(π£ β π β¦ ((πβπ£) Β· π£))) = π β π = (π Γ { 0 }))) β (π β (πΎ βm π) β ((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 }))))) |
45 | 25, 39, 44 | 3bitrd 305 |
. . 3
β’ ((π β LMod β§ π β π΅) β ((π β (Baseβ(πΉ freeLMod π)) β ((π Ξ£g (π βf Β· ( I
βΎ π))) = π β π = (π Γ { 0 }))) β (π β (πΎ βm π) β ((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 }))))) |
46 | 45 | ralbidv2 3167 |
. 2
β’ ((π β LMod β§ π β π΅) β (βπ β (Baseβ(πΉ freeLMod π))((π Ξ£g (π βf Β· ( I
βΎ π))) = π β π = (π Γ { 0 })) β βπ β (πΎ βm π)((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 })))) |
47 | 3, 19, 46 | 3bitrd 305 |
1
β’ ((π β LMod β§ π β π΅) β (π β (LIndSβπ) β βπ β (πΎ βm π)((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 })))) |