Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β LMod) |
2 | | lincfsuppcl.s |
. . . . . . . . 9
β’ π = (Baseβπ
) |
3 | | lincfsuppcl.r |
. . . . . . . . . 10
β’ π
= (Scalarβπ) |
4 | 3 | fveq2i 6895 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβ(Scalarβπ)) |
5 | 2, 4 | eqtri 2761 |
. . . . . . . 8
β’ π =
(Baseβ(Scalarβπ)) |
6 | 5 | oveq1i 7419 |
. . . . . . 7
β’ (π βm π) =
((Baseβ(Scalarβπ)) βm π) |
7 | 6 | eleq2i 2826 |
. . . . . 6
β’ (πΉ β (π βm π) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
8 | 7 | biimpi 215 |
. . . . 5
β’ (πΉ β (π βm π) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
9 | 8 | adantr 482 |
. . . 4
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β πΉ β ((Baseβ(Scalarβπ)) βm π)) |
10 | 9 | 3ad2ant3 1136 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β πΉ β
((Baseβ(Scalarβπ)) βm π)) |
11 | | elpwg 4606 |
. . . . . 6
β’ (π β π β (π β π« (Baseβπ) β π β (Baseβπ))) |
12 | | lincfsuppcl.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ (π β π β π΅ = (Baseβπ)) |
14 | 13 | eqcomd 2739 |
. . . . . . 7
β’ (π β π β (Baseβπ) = π΅) |
15 | 14 | sseq2d 4015 |
. . . . . 6
β’ (π β π β (π β (Baseβπ) β π β π΅)) |
16 | 11, 15 | bitr2d 280 |
. . . . 5
β’ (π β π β (π β π΅ β π β π« (Baseβπ))) |
17 | 16 | biimpa 478 |
. . . 4
β’ ((π β π β§ π β π΅) β π β π« (Baseβπ)) |
18 | 17 | 3ad2ant2 1135 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β π«
(Baseβπ)) |
19 | | lincval 47090 |
. . 3
β’ ((π β LMod β§ πΉ β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (πΉ( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)))) |
20 | 1, 10, 18, 19 | syl3anc 1372 |
. 2
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (πΉ( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)))) |
21 | | eqid 2733 |
. . 3
β’
(0gβπ) = (0gβπ) |
22 | | lmodcmn 20520 |
. . . 4
β’ (π β LMod β π β CMnd) |
23 | 22 | 3ad2ant1 1134 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β CMnd) |
24 | | simpl 484 |
. . . 4
β’ ((π β π β§ π β π΅) β π β π) |
25 | 24 | 3ad2ant2 1135 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β π) |
26 | 1 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π£ β π) β π β LMod) |
27 | | elmapi 8843 |
. . . . . . . . 9
β’ (πΉ β (π βm π) β πΉ:πβΆπ) |
28 | | ffvelcdm 7084 |
. . . . . . . . . 10
β’ ((πΉ:πβΆπ β§ π£ β π) β (πΉβπ£) β π) |
29 | 28 | ex 414 |
. . . . . . . . 9
β’ (πΉ:πβΆπ β (π£ β π β (πΉβπ£) β π)) |
30 | 27, 29 | syl 17 |
. . . . . . . 8
β’ (πΉ β (π βm π) β (π£ β π β (πΉβπ£) β π)) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β (π£ β π β (πΉβπ£) β π)) |
32 | 31 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π£ β π β (πΉβπ£) β π)) |
33 | 32 | imp 408 |
. . . . 5
β’ (((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π£ β π) β (πΉβπ£) β π) |
34 | | ssel 3976 |
. . . . . . . 8
β’ (π β π΅ β (π£ β π β π£ β π΅)) |
35 | 34 | adantl 483 |
. . . . . . 7
β’ ((π β π β§ π β π΅) β (π£ β π β π£ β π΅)) |
36 | 35 | 3ad2ant2 1135 |
. . . . . 6
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π£ β π β π£ β π΅)) |
37 | 36 | imp 408 |
. . . . 5
β’ (((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π£ β π) β π£ β π΅) |
38 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
39 | 12, 3, 38, 2 | lmodvscl 20489 |
. . . . 5
β’ ((π β LMod β§ (πΉβπ£) β π β§ π£ β π΅) β ((πΉβπ£)( Β·π
βπ)π£) β π΅) |
40 | 26, 33, 37, 39 | syl3anc 1372 |
. . . 4
β’ (((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π£ β π) β ((πΉβπ£)( Β·π
βπ)π£) β π΅) |
41 | 40 | fmpttd 7115 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)):πβΆπ΅) |
42 | | simpl 484 |
. . . . 5
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β πΉ β (π βm π)) |
43 | 42 | 3ad2ant3 1136 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β πΉ β (π βm π)) |
44 | | simp3r 1203 |
. . . . 5
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β πΉ finSupp 0 ) |
45 | | lincfsuppcl.0 |
. . . . 5
β’ 0 =
(0gβπ
) |
46 | 44, 45 | breqtrdi 5190 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β πΉ finSupp
(0gβπ
)) |
47 | 3, 2 | scmfsupp 47054 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΉ β (π βm π) β§ πΉ finSupp (0gβπ
)) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)) finSupp (0gβπ)) |
48 | 1, 18, 43, 46, 47 | syl211anc 1377 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)) finSupp (0gβπ)) |
49 | 12, 21, 23, 25, 41, 48 | gsumcl 19783 |
. 2
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π Ξ£g
(π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£))) β π΅) |
50 | 20, 49 | eqeltrd 2834 |
1
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (πΉ( linC βπ)π) β π΅) |