Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
β’
(0gβπ) = (0gβπ) |
2 | | lmodabl 20413 |
. . . . 5
β’ (π β LMod β π β Abel) |
3 | 2 | 3ad2ant1 1134 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β π β Abel) |
4 | 3 | adantr 482 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β π β Abel) |
5 | | ssexg 5284 |
. . . . . 6
β’ ((π β π β§ π β π) β π β V) |
6 | 5 | ancoms 460 |
. . . . 5
β’ ((π β π β§ π β π) β π β V) |
7 | 6 | 3adant1 1131 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β π β V) |
8 | 7 | adantr 482 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β π β V) |
9 | | 3simpa 1149 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β (π β LMod β§ π β π)) |
10 | | gsumlsscl.s |
. . . . . 6
β’ π = (LSubSpβπ) |
11 | 10 | lsssubg 20462 |
. . . . 5
β’ ((π β LMod β§ π β π) β π β (SubGrpβπ)) |
12 | 9, 11 | syl 17 |
. . . 4
β’ ((π β LMod β§ π β π β§ π β π) β π β (SubGrpβπ)) |
13 | 12 | adantr 482 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β π β (SubGrpβπ)) |
14 | 9 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β (π β LMod β§ π β π)) |
15 | 14 | adantr 482 |
. . . . 5
β’ ((((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β§ π£ β π) β (π β LMod β§ π β π)) |
16 | | elmapi 8793 |
. . . . . . . 8
β’ (πΉ β (π΅ βm π) β πΉ:πβΆπ΅) |
17 | | ffvelcdm 7036 |
. . . . . . . . 9
β’ ((πΉ:πβΆπ΅ β§ π£ β π) β (πΉβπ£) β π΅) |
18 | 17 | ex 414 |
. . . . . . . 8
β’ (πΉ:πβΆπ΅ β (π£ β π β (πΉβπ£) β π΅)) |
19 | 16, 18 | syl 17 |
. . . . . . 7
β’ (πΉ β (π΅ βm π) β (π£ β π β (πΉβπ£) β π΅)) |
20 | 19 | ad2antrl 727 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β (π£ β π β (πΉβπ£) β π΅)) |
21 | 20 | imp 408 |
. . . . 5
β’ ((((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β§ π£ β π) β (πΉβπ£) β π΅) |
22 | | ssel 3941 |
. . . . . . . 8
β’ (π β π β (π£ β π β π£ β π)) |
23 | 22 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π£ β π β π£ β π)) |
24 | 23 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β (π£ β π β π£ β π)) |
25 | 24 | imp 408 |
. . . . 5
β’ ((((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β§ π£ β π) β π£ β π) |
26 | | gsumlsscl.r |
. . . . . 6
β’ π
= (Scalarβπ) |
27 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
28 | | gsumlsscl.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
29 | 26, 27, 28, 10 | lssvscl 20460 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ ((πΉβπ£) β π΅ β§ π£ β π)) β ((πΉβπ£)( Β·π
βπ)π£) β π) |
30 | 15, 21, 25, 29 | syl12anc 836 |
. . . 4
β’ ((((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β§ π£ β π) β ((πΉβπ£)( Β·π
βπ)π£) β π) |
31 | 30 | fmpttd 7067 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)):πβΆπ) |
32 | | simp1 1137 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β π β LMod) |
33 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ) =
(Baseβπ) |
34 | 33, 10 | lssss 20441 |
. . . . . . . . . 10
β’ (π β π β π β (Baseβπ)) |
35 | | sstr 3956 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (Baseβπ)) β π β (Baseβπ)) |
36 | 35 | expcom 415 |
. . . . . . . . . 10
β’ (π β (Baseβπ) β (π β π β π β (Baseβπ))) |
37 | 34, 36 | syl 17 |
. . . . . . . . 9
β’ (π β π β (π β π β π β (Baseβπ))) |
38 | 37 | a1i 11 |
. . . . . . . 8
β’ (π β LMod β (π β π β (π β π β π β (Baseβπ)))) |
39 | 38 | 3imp 1112 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β π β (Baseβπ)) |
40 | | elpwg 4567 |
. . . . . . . 8
β’ (π β V β (π β π«
(Baseβπ) β π β (Baseβπ))) |
41 | 7, 40 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ π β π β§ π β π) β (π β π« (Baseβπ) β π β (Baseβπ))) |
42 | 39, 41 | mpbird 257 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β π β π« (Baseβπ)) |
43 | 32, 42 | jca 513 |
. . . . 5
β’ ((π β LMod β§ π β π β§ π β π) β (π β LMod β§ π β π« (Baseβπ))) |
44 | 43 | adantr 482 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β (π β LMod β§ π β π« (Baseβπ))) |
45 | | simprl 770 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β πΉ β (π΅ βm π)) |
46 | | simprr 772 |
. . . 4
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β πΉ finSupp (0gβπ
)) |
47 | 26, 28 | scmfsupp 46544 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
)) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)) finSupp (0gβπ)) |
48 | 44, 45, 46, 47 | syl3anc 1372 |
. . 3
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)) finSupp (0gβπ)) |
49 | 1, 4, 8, 13, 31, 48 | gsumsubgcl 19705 |
. 2
β’ (((π β LMod β§ π β π β§ π β π) β§ (πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
))) β (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£))) β π) |
50 | 49 | ex 414 |
1
β’ ((π β LMod β§ π β π β§ π β π) β ((πΉ β (π΅ βm π) β§ πΉ finSupp (0gβπ
)) β (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£))) β π)) |