Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β LMod) |
2 | | lincfsuppcl.s |
. . . . . . . . 9
β’ π = (Baseβπ
) |
3 | | lincfsuppcl.r |
. . . . . . . . . 10
β’ π
= (Scalarβπ) |
4 | 3 | fveq2i 6803 |
. . . . . . . . 9
β’
(Baseβπ
) =
(Baseβ(Scalarβπ)) |
5 | 2, 4 | eqtri 2764 |
. . . . . . . 8
β’ π =
(Baseβ(Scalarβπ)) |
6 | 5 | oveq1i 7313 |
. . . . . . 7
β’ (π βm π) =
((Baseβ(Scalarβπ)) βm π) |
7 | 6 | eleq2i 2828 |
. . . . . 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 1135 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β πΉ β
((Baseβ(Scalarβπ)) βm π)) |
11 | | elpwg 4542 |
. . . . . 6
β’ (π β π β (π β π« (Baseβπ) β π β (Baseβπ))) |
12 | | lincfsuppcl.b |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
13 | 12 | a1i 11 |
. . . . . . . 8
β’ (π β π β π΅ = (Baseβπ)) |
14 | 13 | eqcomd 2742 |
. . . . . . 7
β’ (π β π β (Baseβπ) = π΅) |
15 | 14 | sseq2d 3958 |
. . . . . 6
β’ (π β π β (π β (Baseβπ) β π β π΅)) |
16 | 11, 15 | bitr2d 281 |
. . . . 5
β’ (π β π β (π β π΅ β π β π« (Baseβπ))) |
17 | 16 | biimpa 478 |
. . . 4
β’ ((π β π β§ π β π΅) β π β π« (Baseβπ)) |
18 | 17 | 3ad2ant2 1134 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β π«
(Baseβπ)) |
19 | | lincval 45807 |
. . 3
β’ ((π β LMod β§ πΉ β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (πΉ( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)))) |
20 | 1, 10, 18, 19 | syl3anc 1371 |
. 2
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (πΉ( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)))) |
21 | | eqid 2736 |
. . 3
β’
(0gβπ) = (0gβπ) |
22 | | lmodcmn 20212 |
. . . 4
β’ (π β LMod β π β CMnd) |
23 | 22 | 3ad2ant1 1133 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β CMnd) |
24 | | simpl 484 |
. . . 4
β’ ((π β π β§ π β π΅) β π β π) |
25 | 24 | 3ad2ant2 1134 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β π β π) |
26 | 1 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π£ β π) β π β LMod) |
27 | | elmapi 8664 |
. . . . . . . . 9
β’ (πΉ β (π βm π) β πΉ:πβΆπ) |
28 | | ffvelcdm 6987 |
. . . . . . . . . 10
β’ ((πΉ:πβΆπ β§ π£ β π) β (πΉβπ£) β π) |
29 | 28 | ex 414 |
. . . . . . . . 9
β’ (πΉ:πβΆπ β (π£ β π β (πΉβπ£) β π)) |
30 | 27, 29 | syl 17 |
. . . . . . . 8
β’ (πΉ β (π βm π) β (π£ β π β (πΉβπ£) β π)) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β (π£ β π β (πΉβπ£) β π)) |
32 | 31 | 3ad2ant3 1135 |
. . . . . 6
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π£ β π β (πΉβπ£) β π)) |
33 | 32 | imp 408 |
. . . . 5
β’ (((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π£ β π) β (πΉβπ£) β π) |
34 | | ssel 3919 |
. . . . . . . 8
β’ (π β π΅ β (π£ β π β π£ β π΅)) |
35 | 34 | adantl 483 |
. . . . . . 7
β’ ((π β π β§ π β π΅) β (π£ β π β π£ β π΅)) |
36 | 35 | 3ad2ant2 1134 |
. . . . . 6
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π£ β π β π£ β π΅)) |
37 | 36 | imp 408 |
. . . . 5
β’ (((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π£ β π) β π£ β π΅) |
38 | | eqid 2736 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
39 | 12, 3, 38, 2 | lmodvscl 20181 |
. . . . 5
β’ ((π β LMod β§ (πΉβπ£) β π β§ π£ β π΅) β ((πΉβπ£)( Β·π
βπ)π£) β π΅) |
40 | 26, 33, 37, 39 | syl3anc 1371 |
. . . 4
β’ (((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β§ π£ β π) β ((πΉβπ£)( Β·π
βπ)π£) β π΅) |
41 | 40 | fmpttd 7017 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)):πβΆπ΅) |
42 | | simpl 484 |
. . . . 5
β’ ((πΉ β (π βm π) β§ πΉ finSupp 0 ) β πΉ β (π βm π)) |
43 | 42 | 3ad2ant3 1135 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β πΉ β (π βm π)) |
44 | | simp3r 1202 |
. . . . 5
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β πΉ finSupp 0 ) |
45 | | lincfsuppcl.0 |
. . . . 5
β’ 0 =
(0gβπ
) |
46 | 44, 45 | breqtrdi 5122 |
. . . 4
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β πΉ finSupp
(0gβπ
)) |
47 | 3, 2 | scmfsupp 45771 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ πΉ β (π βm π) β§ πΉ finSupp (0gβπ
)) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)) finSupp (0gβπ)) |
48 | 1, 18, 43, 46, 47 | syl211anc 1376 |
. . 3
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£)) finSupp (0gβπ)) |
49 | 12, 21, 23, 25, 41, 48 | gsumcl 19557 |
. 2
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (π Ξ£g
(π£ β π β¦ ((πΉβπ£)( Β·π
βπ)π£))) β π΅) |
50 | 20, 49 | eqeltrd 2837 |
1
β’ ((π β LMod β§ (π β π β§ π β π΅) β§ (πΉ β (π βm π) β§ πΉ finSupp 0 )) β (πΉ( linC βπ)π) β π΅) |