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 ⊢ · ˙ = ⋅ T
frlmup.e ⊢ E = x ∈ B ⟼ ∑ T x · ˙ f A
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 ⊢ · ˙ = ⋅ T
5 frlmup.e ⊢ E = x ∈ B ⟼ ∑ T x · ˙ f A
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