# Metamath Proof Explorer

## Theorem frlmup3

Description: The range of such an evaluation map is the finite linear combinations of the target vectors and also the span of the target vectors. (Contributed by Stefan O'Rear, 6-Feb-2015)

Ref Expression
Hypotheses frlmup.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
frlmup.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
frlmup.c ${⊢}{C}={\mathrm{Base}}_{{T}}$
frlmup.v
frlmup.e
frlmup.t ${⊢}{\phi }\to {T}\in \mathrm{LMod}$
frlmup.i ${⊢}{\phi }\to {I}\in {X}$
frlmup.r ${⊢}{\phi }\to {R}=\mathrm{Scalar}\left({T}\right)$
frlmup.a ${⊢}{\phi }\to {A}:{I}⟶{C}$
frlmup.k ${⊢}{K}=\mathrm{LSpan}\left({T}\right)$
Assertion frlmup3 ${⊢}{\phi }\to \mathrm{ran}{E}={K}\left(\mathrm{ran}{A}\right)$

### Proof

Step Hyp Ref Expression
1 frlmup.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
2 frlmup.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
3 frlmup.c ${⊢}{C}={\mathrm{Base}}_{{T}}$
4 frlmup.v
5 frlmup.e
6 frlmup.t ${⊢}{\phi }\to {T}\in \mathrm{LMod}$
7 frlmup.i ${⊢}{\phi }\to {I}\in {X}$
8 frlmup.r ${⊢}{\phi }\to {R}=\mathrm{Scalar}\left({T}\right)$
9 frlmup.a ${⊢}{\phi }\to {A}:{I}⟶{C}$
10 frlmup.k ${⊢}{K}=\mathrm{LSpan}\left({T}\right)$
11 1 2 3 4 5 6 7 8 9 frlmup1 ${⊢}{\phi }\to {E}\in \left({F}\mathrm{LMHom}{T}\right)$
12 eqid ${⊢}\mathrm{Scalar}\left({T}\right)=\mathrm{Scalar}\left({T}\right)$
13 12 lmodring ${⊢}{T}\in \mathrm{LMod}\to \mathrm{Scalar}\left({T}\right)\in \mathrm{Ring}$
14 6 13 syl ${⊢}{\phi }\to \mathrm{Scalar}\left({T}\right)\in \mathrm{Ring}$
15 8 14 eqeltrd ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
16 eqid ${⊢}{R}\mathrm{unitVec}{I}={R}\mathrm{unitVec}{I}$
17 16 1 2 uvcff ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {X}\right)\to \left({R}\mathrm{unitVec}{I}\right):{I}⟶{B}$
18 15 7 17 syl2anc ${⊢}{\phi }\to \left({R}\mathrm{unitVec}{I}\right):{I}⟶{B}$
19 18 frnd ${⊢}{\phi }\to \mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\subseteq {B}$
20 eqid ${⊢}\mathrm{LSpan}\left({F}\right)=\mathrm{LSpan}\left({F}\right)$
21 2 20 10 lmhmlsp ${⊢}\left({E}\in \left({F}\mathrm{LMHom}{T}\right)\wedge \mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\subseteq {B}\right)\to {E}\left[\mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right)\right]={K}\left({E}\left[\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right]\right)$
22 11 19 21 syl2anc ${⊢}{\phi }\to {E}\left[\mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right)\right]={K}\left({E}\left[\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right]\right)$
23 2 3 lmhmf ${⊢}{E}\in \left({F}\mathrm{LMHom}{T}\right)\to {E}:{B}⟶{C}$
24 11 23 syl ${⊢}{\phi }\to {E}:{B}⟶{C}$
25 24 ffnd ${⊢}{\phi }\to {E}Fn{B}$
26 fnima ${⊢}{E}Fn{B}\to {E}\left[{B}\right]=\mathrm{ran}{E}$
27 25 26 syl ${⊢}{\phi }\to {E}\left[{B}\right]=\mathrm{ran}{E}$
28 eqid ${⊢}\mathrm{LBasis}\left({F}\right)=\mathrm{LBasis}\left({F}\right)$
29 1 16 28 frlmlbs ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {X}\right)\to \mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\in \mathrm{LBasis}\left({F}\right)$
30 15 7 29 syl2anc ${⊢}{\phi }\to \mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\in \mathrm{LBasis}\left({F}\right)$
31 2 28 20 lbssp ${⊢}\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\in \mathrm{LBasis}\left({F}\right)\to \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right)={B}$
32 30 31 syl ${⊢}{\phi }\to \mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right)={B}$
33 32 eqcomd ${⊢}{\phi }\to {B}=\mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right)$
34 33 imaeq2d ${⊢}{\phi }\to {E}\left[{B}\right]={E}\left[\mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right)\right]$
35 27 34 eqtr3d ${⊢}{\phi }\to \mathrm{ran}{E}={E}\left[\mathrm{LSpan}\left({F}\right)\left(\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right)\right]$
36 imaco ${⊢}\left({E}\circ \left({R}\mathrm{unitVec}{I}\right)\right)\left[{I}\right]={E}\left[\left({R}\mathrm{unitVec}{I}\right)\left[{I}\right]\right]$
37 9 ffnd ${⊢}{\phi }\to {A}Fn{I}$
38 18 ffnd ${⊢}{\phi }\to \left({R}\mathrm{unitVec}{I}\right)Fn{I}$
39 fnco ${⊢}\left({E}Fn{B}\wedge \left({R}\mathrm{unitVec}{I}\right)Fn{I}\wedge \mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\subseteq {B}\right)\to \left({E}\circ \left({R}\mathrm{unitVec}{I}\right)\right)Fn{I}$
40 25 38 19 39 syl3anc ${⊢}{\phi }\to \left({E}\circ \left({R}\mathrm{unitVec}{I}\right)\right)Fn{I}$
41 fvco2 ${⊢}\left(\left({R}\mathrm{unitVec}{I}\right)Fn{I}\wedge {u}\in {I}\right)\to \left({E}\circ \left({R}\mathrm{unitVec}{I}\right)\right)\left({u}\right)={E}\left(\left({R}\mathrm{unitVec}{I}\right)\left({u}\right)\right)$
42 38 41 sylan ${⊢}\left({\phi }\wedge {u}\in {I}\right)\to \left({E}\circ \left({R}\mathrm{unitVec}{I}\right)\right)\left({u}\right)={E}\left(\left({R}\mathrm{unitVec}{I}\right)\left({u}\right)\right)$
43 6 adantr ${⊢}\left({\phi }\wedge {u}\in {I}\right)\to {T}\in \mathrm{LMod}$
44 7 adantr ${⊢}\left({\phi }\wedge {u}\in {I}\right)\to {I}\in {X}$
45 8 adantr ${⊢}\left({\phi }\wedge {u}\in {I}\right)\to {R}=\mathrm{Scalar}\left({T}\right)$
46 9 adantr ${⊢}\left({\phi }\wedge {u}\in {I}\right)\to {A}:{I}⟶{C}$
47 simpr ${⊢}\left({\phi }\wedge {u}\in {I}\right)\to {u}\in {I}$
48 1 2 3 4 5 43 44 45 46 47 16 frlmup2 ${⊢}\left({\phi }\wedge {u}\in {I}\right)\to {E}\left(\left({R}\mathrm{unitVec}{I}\right)\left({u}\right)\right)={A}\left({u}\right)$
49 42 48 eqtr2d ${⊢}\left({\phi }\wedge {u}\in {I}\right)\to {A}\left({u}\right)=\left({E}\circ \left({R}\mathrm{unitVec}{I}\right)\right)\left({u}\right)$
50 37 40 49 eqfnfvd ${⊢}{\phi }\to {A}={E}\circ \left({R}\mathrm{unitVec}{I}\right)$
51 50 imaeq1d ${⊢}{\phi }\to {A}\left[{I}\right]=\left({E}\circ \left({R}\mathrm{unitVec}{I}\right)\right)\left[{I}\right]$
52 fnima ${⊢}{A}Fn{I}\to {A}\left[{I}\right]=\mathrm{ran}{A}$
53 37 52 syl ${⊢}{\phi }\to {A}\left[{I}\right]=\mathrm{ran}{A}$
54 51 53 eqtr3d ${⊢}{\phi }\to \left({E}\circ \left({R}\mathrm{unitVec}{I}\right)\right)\left[{I}\right]=\mathrm{ran}{A}$
55 fnima ${⊢}\left({R}\mathrm{unitVec}{I}\right)Fn{I}\to \left({R}\mathrm{unitVec}{I}\right)\left[{I}\right]=\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)$
56 38 55 syl ${⊢}{\phi }\to \left({R}\mathrm{unitVec}{I}\right)\left[{I}\right]=\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)$
57 56 imaeq2d ${⊢}{\phi }\to {E}\left[\left({R}\mathrm{unitVec}{I}\right)\left[{I}\right]\right]={E}\left[\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right]$
58 36 54 57 3eqtr3a ${⊢}{\phi }\to \mathrm{ran}{A}={E}\left[\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right]$
59 58 fveq2d ${⊢}{\phi }\to {K}\left(\mathrm{ran}{A}\right)={K}\left({E}\left[\mathrm{ran}\left({R}\mathrm{unitVec}{I}\right)\right]\right)$
60 22 35 59 3eqtr4d ${⊢}{\phi }\to \mathrm{ran}{E}={K}\left(\mathrm{ran}{A}\right)$