Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β π β LMod) |
2 | | linccl.r |
. . . . . . . 8
β’ π
=
(Baseβ(Scalarβπ)) |
3 | 2 | oveq1i 7371 |
. . . . . . 7
β’ (π
βm π) =
((Baseβ(Scalarβπ)) βm π) |
4 | 3 | eleq2i 2826 |
. . . . . 6
β’ (π β (π
βm π) β π β ((Baseβ(Scalarβπ)) βm π)) |
5 | 4 | biimpi 215 |
. . . . 5
β’ (π β (π
βm π) β π β ((Baseβ(Scalarβπ)) βm π)) |
6 | 5 | 3ad2ant3 1136 |
. . . 4
β’ ((π β Fin β§ π β π΅ β§ π β (π
βm π)) β π β ((Baseβ(Scalarβπ)) βm π)) |
7 | 6 | adantl 483 |
. . 3
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β π β ((Baseβ(Scalarβπ)) βm π)) |
8 | | linccl.b |
. . . . . . 7
β’ π΅ = (Baseβπ) |
9 | 8 | sseq2i 3977 |
. . . . . 6
β’ (π β π΅ β π β (Baseβπ)) |
10 | | fvex 6859 |
. . . . . . . . 9
β’
(Baseβπ)
β V |
11 | 10 | ssex 5282 |
. . . . . . . 8
β’ (π β (Baseβπ) β π β V) |
12 | | elpwg 4567 |
. . . . . . . 8
β’ (π β V β (π β π«
(Baseβπ) β π β (Baseβπ))) |
13 | 11, 12 | syl 17 |
. . . . . . 7
β’ (π β (Baseβπ) β (π β π« (Baseβπ) β π β (Baseβπ))) |
14 | 13 | ibir 268 |
. . . . . 6
β’ (π β (Baseβπ) β π β π« (Baseβπ)) |
15 | 9, 14 | sylbi 216 |
. . . . 5
β’ (π β π΅ β π β π« (Baseβπ)) |
16 | 15 | 3ad2ant2 1135 |
. . . 4
β’ ((π β Fin β§ π β π΅ β§ π β (π
βm π)) β π β π« (Baseβπ)) |
17 | 16 | adantl 483 |
. . 3
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β π β π« (Baseβπ)) |
18 | | lincval 46580 |
. . 3
β’ ((π β LMod β§ π β
((Baseβ(Scalarβπ)) βm π) β§ π β π« (Baseβπ)) β (π( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πβπ£)( Β·π
βπ)π£)))) |
19 | 1, 7, 17, 18 | syl3anc 1372 |
. 2
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β (π( linC βπ)π) = (π Ξ£g (π£ β π β¦ ((πβπ£)( Β·π
βπ)π£)))) |
20 | | eqid 2733 |
. . 3
β’
(0gβπ) = (0gβπ) |
21 | | lmodcmn 20414 |
. . . 4
β’ (π β LMod β π β CMnd) |
22 | 21 | adantr 482 |
. . 3
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β π β CMnd) |
23 | | simpr1 1195 |
. . 3
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β π β Fin) |
24 | 1 | adantr 482 |
. . . . 5
β’ (((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β§ π£ β π) β π β LMod) |
25 | 2 | fvexi 6860 |
. . . . . . . . . . 11
β’ π
β V |
26 | | elmapg 8784 |
. . . . . . . . . . 11
β’ ((π
β V β§ π β Fin) β (π β (π
βm π) β π:πβΆπ
)) |
27 | 25, 26 | mpan 689 |
. . . . . . . . . 10
β’ (π β Fin β (π β (π
βm π) β π:πβΆπ
)) |
28 | | ffvelcdm 7036 |
. . . . . . . . . . 11
β’ ((π:πβΆπ
β§ π£ β π) β (πβπ£) β π
) |
29 | 28 | ex 414 |
. . . . . . . . . 10
β’ (π:πβΆπ
β (π£ β π β (πβπ£) β π
)) |
30 | 27, 29 | syl6bi 253 |
. . . . . . . . 9
β’ (π β Fin β (π β (π
βm π) β (π£ β π β (πβπ£) β π
))) |
31 | 30 | imp 408 |
. . . . . . . 8
β’ ((π β Fin β§ π β (π
βm π)) β (π£ β π β (πβπ£) β π
)) |
32 | 31 | 3adant2 1132 |
. . . . . . 7
β’ ((π β Fin β§ π β π΅ β§ π β (π
βm π)) β (π£ β π β (πβπ£) β π
)) |
33 | 32 | adantl 483 |
. . . . . 6
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β (π£ β π β (πβπ£) β π
)) |
34 | 33 | imp 408 |
. . . . 5
β’ (((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β§ π£ β π) β (πβπ£) β π
) |
35 | | ssel 3941 |
. . . . . . . 8
β’ (π β π΅ β (π£ β π β π£ β π΅)) |
36 | 35 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β Fin β§ π β π΅ β§ π β (π
βm π)) β (π£ β π β π£ β π΅)) |
37 | 36 | adantl 483 |
. . . . . 6
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β (π£ β π β π£ β π΅)) |
38 | 37 | imp 408 |
. . . . 5
β’ (((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β§ π£ β π) β π£ β π΅) |
39 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
40 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ) = ( Β·π
βπ) |
41 | 8, 39, 40, 2 | lmodvscl 20383 |
. . . . 5
β’ ((π β LMod β§ (πβπ£) β π
β§ π£ β π΅) β ((πβπ£)( Β·π
βπ)π£) β π΅) |
42 | 24, 34, 38, 41 | syl3anc 1372 |
. . . 4
β’ (((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β§ π£ β π) β ((πβπ£)( Β·π
βπ)π£) β π΅) |
43 | 42 | fmpttd 7067 |
. . 3
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β (π£ β π β¦ ((πβπ£)( Β·π
βπ)π£)):πβΆπ΅) |
44 | 16 | anim2i 618 |
. . . 4
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β (π β LMod β§ π β π« (Baseβπ))) |
45 | | simpr3 1197 |
. . . 4
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β π β (π
βm π)) |
46 | | elmapi 8793 |
. . . . . . 7
β’ (π β (π
βm π) β π:πβΆπ
) |
47 | 46 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π β Fin β§ π β π΅ β§ π β (π
βm π)) β π:πβΆπ
) |
48 | 47 | adantl 483 |
. . . . 5
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β π:πβΆπ
) |
49 | | fvexd 6861 |
. . . . 5
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β
(0gβ(Scalarβπ)) β V) |
50 | 48, 23, 49 | fdmfifsupp 9323 |
. . . 4
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β π finSupp
(0gβ(Scalarβπ))) |
51 | 39, 2 | scmfsupp 46544 |
. . . 4
β’ (((π β LMod β§ π β π«
(Baseβπ)) β§ π β (π
βm π) β§ π finSupp
(0gβ(Scalarβπ))) β (π£ β π β¦ ((πβπ£)( Β·π
βπ)π£)) finSupp (0gβπ)) |
52 | 44, 45, 50, 51 | syl3anc 1372 |
. . 3
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β (π£ β π β¦ ((πβπ£)( Β·π
βπ)π£)) finSupp (0gβπ)) |
53 | 8, 20, 22, 23, 43, 52 | gsumcl 19700 |
. 2
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β (π Ξ£g (π£ β π β¦ ((πβπ£)( Β·π
βπ)π£))) β π΅) |
54 | 19, 53 | eqeltrd 2834 |
1
β’ ((π β LMod β§ (π β Fin β§ π β π΅ β§ π β (π
βm π))) β (π( linC βπ)π) β π΅) |