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 ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmup.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
frlmup.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
frlmup.v ⊢ · = ( ·𝑠 ‘ 𝑇 )
frlmup.e ⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
frlmup.t ⊢ ( 𝜑 → 𝑇 ∈ LMod )
frlmup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
frlmup.r ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) )
frlmup.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 )
frlmup.k ⊢ 𝐾 = ( LSpan ‘ 𝑇 )
Assertion frlmup3 ( 𝜑 → ran 𝐸 = ( 𝐾 ‘ ran 𝐴 ) )

Proof

Step Hyp Ref Expression
1 frlmup.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmup.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
3 frlmup.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
4 frlmup.v ⊢ · = ( ·𝑠 ‘ 𝑇 )
5 frlmup.e ⊢ 𝐸 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 Σg ( 𝑥 ∘f · 𝐴 ) ) )
6 frlmup.t ⊢ ( 𝜑 → 𝑇 ∈ LMod )
7 frlmup.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
8 frlmup.r ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑇 ) )
9 frlmup.a ⊢ ( 𝜑 → 𝐴 : 𝐼 ⟶ 𝐶 )
10 frlmup.k ⊢ 𝐾 = ( LSpan ‘ 𝑇 )
11 1 2 3 4 5 6 7 8 9 frlmup1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) )
12 eqid ⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
13 12 lmodring ⊢ ( 𝑇 ∈ LMod → ( Scalar ‘ 𝑇 ) ∈ Ring )
14 6 13 syl ⊢ ( 𝜑 → ( Scalar ‘ 𝑇 ) ∈ Ring )
15 8 14 eqeltrd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
16 eqid ⊢ ( 𝑅 unitVec 𝐼 ) = ( 𝑅 unitVec 𝐼 )
17 16 1 2 uvcff ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋 ) → ( 𝑅 unitVec 𝐼 ) : 𝐼 ⟶ 𝐵 )
18 15 7 17 syl2anc ⊢ ( 𝜑 → ( 𝑅 unitVec 𝐼 ) : 𝐼 ⟶ 𝐵 )
19 18 frnd ⊢ ( 𝜑 → ran ( 𝑅 unitVec 𝐼 ) ⊆ 𝐵 )
20 eqid ⊢ ( LSpan ‘ 𝐹 ) = ( LSpan ‘ 𝐹 )
21 2 20 10 lmhmlsp ⊢ ( ( 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) ∧ ran ( 𝑅 unitVec 𝐼 ) ⊆ 𝐵 ) → ( 𝐸 “ ( ( LSpan ‘ 𝐹 ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) ) = ( 𝐾 ‘ ( 𝐸 “ ran ( 𝑅 unitVec 𝐼 ) ) ) )
22 11 19 21 syl2anc ⊢ ( 𝜑 → ( 𝐸 “ ( ( LSpan ‘ 𝐹 ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) ) = ( 𝐾 ‘ ( 𝐸 “ ran ( 𝑅 unitVec 𝐼 ) ) ) )
23 2 3 lmhmf ⊢ ( 𝐸 ∈ ( 𝐹 LMHom 𝑇 ) → 𝐸 : 𝐵 ⟶ 𝐶 )
24 11 23 syl ⊢ ( 𝜑 → 𝐸 : 𝐵 ⟶ 𝐶 )
25 24 ffnd ⊢ ( 𝜑 → 𝐸 Fn 𝐵 )
26 fnima ⊢ ( 𝐸 Fn 𝐵 → ( 𝐸 “ 𝐵 ) = ran 𝐸 )
27 25 26 syl ⊢ ( 𝜑 → ( 𝐸 “ 𝐵 ) = ran 𝐸 )
28 eqid ⊢ ( LBasis ‘ 𝐹 ) = ( LBasis ‘ 𝐹 )
29 1 16 28 frlmlbs ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑋 ) → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ 𝐹 ) )
30 15 7 29 syl2anc ⊢ ( 𝜑 → ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ 𝐹 ) )
31 2 28 20 lbssp ⊢ ( ran ( 𝑅 unitVec 𝐼 ) ∈ ( LBasis ‘ 𝐹 ) → ( ( LSpan ‘ 𝐹 ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) = 𝐵 )
32 30 31 syl ⊢ ( 𝜑 → ( ( LSpan ‘ 𝐹 ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) = 𝐵 )
33 32 eqcomd ⊢ ( 𝜑 → 𝐵 = ( ( LSpan ‘ 𝐹 ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) )
34 33 imaeq2d ⊢ ( 𝜑 → ( 𝐸 “ 𝐵 ) = ( 𝐸 “ ( ( LSpan ‘ 𝐹 ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) ) )
35 27 34 eqtr3d ⊢ ( 𝜑 → ran 𝐸 = ( 𝐸 “ ( ( LSpan ‘ 𝐹 ) ‘ ran ( 𝑅 unitVec 𝐼 ) ) ) )
36 imaco ⊢ ( ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) “ 𝐼 ) = ( 𝐸 “ ( ( 𝑅 unitVec 𝐼 ) “ 𝐼 ) )
37 9 ffnd ⊢ ( 𝜑 → 𝐴 Fn 𝐼 )
38 18 ffnd ⊢ ( 𝜑 → ( 𝑅 unitVec 𝐼 ) Fn 𝐼 )
39 fnco ⊢ ( ( 𝐸 Fn 𝐵 ∧ ( 𝑅 unitVec 𝐼 ) Fn 𝐼 ∧ ran ( 𝑅 unitVec 𝐼 ) ⊆ 𝐵 ) → ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) Fn 𝐼 )
40 25 38 19 39 syl3anc ⊢ ( 𝜑 → ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) Fn 𝐼 )
41 fvco2 ⊢ ( ( ( 𝑅 unitVec 𝐼 ) Fn 𝐼 ∧ 𝑢 ∈ 𝐼 ) → ( ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) ‘ 𝑢 ) = ( 𝐸 ‘ ( ( 𝑅 unitVec 𝐼 ) ‘ 𝑢 ) ) )
42 38 41 sylan ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐼 ) → ( ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) ‘ 𝑢 ) = ( 𝐸 ‘ ( ( 𝑅 unitVec 𝐼 ) ‘ 𝑢 ) ) )
43 6 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐼 ) → 𝑇 ∈ LMod )
44 7 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐼 ) → 𝐼 ∈ 𝑋 )
45 8 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐼 ) → 𝑅 = ( Scalar ‘ 𝑇 ) )
46 9 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐼 ) → 𝐴 : 𝐼 ⟶ 𝐶 )
47 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐼 ) → 𝑢 ∈ 𝐼 )
48 1 2 3 4 5 43 44 45 46 47 16 frlmup2 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐼 ) → ( 𝐸 ‘ ( ( 𝑅 unitVec 𝐼 ) ‘ 𝑢 ) ) = ( 𝐴 ‘ 𝑢 ) )
49 42 48 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐼 ) → ( 𝐴 ‘ 𝑢 ) = ( ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) ‘ 𝑢 ) )
50 37 40 49 eqfnfvd ⊢ ( 𝜑 → 𝐴 = ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) )
51 50 imaeq1d ⊢ ( 𝜑 → ( 𝐴 “ 𝐼 ) = ( ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) “ 𝐼 ) )
52 fnima ⊢ ( 𝐴 Fn 𝐼 → ( 𝐴 “ 𝐼 ) = ran 𝐴 )
53 37 52 syl ⊢ ( 𝜑 → ( 𝐴 “ 𝐼 ) = ran 𝐴 )
54 51 53 eqtr3d ⊢ ( 𝜑 → ( ( 𝐸 ∘ ( 𝑅 unitVec 𝐼 ) ) “ 𝐼 ) = ran 𝐴 )
55 fnima ⊢ ( ( 𝑅 unitVec 𝐼 ) Fn 𝐼 → ( ( 𝑅 unitVec 𝐼 ) “ 𝐼 ) = ran ( 𝑅 unitVec 𝐼 ) )
56 38 55 syl ⊢ ( 𝜑 → ( ( 𝑅 unitVec 𝐼 ) “ 𝐼 ) = ran ( 𝑅 unitVec 𝐼 ) )
57 56 imaeq2d ⊢ ( 𝜑 → ( 𝐸 “ ( ( 𝑅 unitVec 𝐼 ) “ 𝐼 ) ) = ( 𝐸 “ ran ( 𝑅 unitVec 𝐼 ) ) )
58 36 54 57 3eqtr3a ⊢ ( 𝜑 → ran 𝐴 = ( 𝐸 “ ran ( 𝑅 unitVec 𝐼 ) ) )
59 58 fveq2d ⊢ ( 𝜑 → ( 𝐾 ‘ ran 𝐴 ) = ( 𝐾 ‘ ( 𝐸 “ ran ( 𝑅 unitVec 𝐼 ) ) ) )
60 22 35 59 3eqtr4d ⊢ ( 𝜑 → ran 𝐸 = ( 𝐾 ‘ ran 𝐴 ) )