# 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 freeLMod I$
frlmup.b $⊢ B = Base F$
frlmup.c $⊢ C = Base T$
frlmup.v
frlmup.e
frlmup.t $⊢ φ → T ∈ LMod$
frlmup.i $⊢ φ → I ∈ X$
frlmup.r $⊢ φ → R = Scalar ⁡ T$
frlmup.a $⊢ φ → A : I ⟶ C$
frlmup.k $⊢ K = LSpan ⁡ T$
Assertion frlmup3 $⊢ φ → ran ⁡ E = K ⁡ ran ⁡ A$

### Proof

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