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 
|- .x. = ( .s ` T )
frlmup.e 
|- E = ( x e. B |-> ( T gsum ( x oF .x. A ) ) )
frlmup.t 
|- ( ph -> T e. LMod )
frlmup.i 
|- ( ph -> I e. X )
frlmup.r 
|- ( ph -> R = ( Scalar ` T ) )
frlmup.a 
|- ( ph -> A : I --> C )
frlmup.k 
|- K = ( LSpan ` T )
Assertion frlmup3 
|- ( ph -> 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 
 |-  .x. = ( .s ` T )
5 frlmup.e 
 |-  E = ( x e. B |-> ( T gsum ( x oF .x. A ) ) )
6 frlmup.t 
 |-  ( ph -> T e. LMod )
7 frlmup.i 
 |-  ( ph -> I e. X )
8 frlmup.r 
 |-  ( ph -> R = ( Scalar ` T ) )
9 frlmup.a 
 |-  ( ph -> A : I --> C )
10 frlmup.k 
 |-  K = ( LSpan ` T )
11 1 2 3 4 5 6 7 8 9 frlmup1 
 |-  ( ph -> E e. ( F LMHom T ) )
12 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
13 12 lmodring 
 |-  ( T e. LMod -> ( Scalar ` T ) e. Ring )
14 6 13 syl 
 |-  ( ph -> ( Scalar ` T ) e. Ring )
15 8 14 eqeltrd 
 |-  ( ph -> R e. Ring )
16 eqid 
 |-  ( R unitVec I ) = ( R unitVec I )
17 16 1 2 uvcff 
 |-  ( ( R e. Ring /\ I e. X ) -> ( R unitVec I ) : I --> B )
18 15 7 17 syl2anc 
 |-  ( ph -> ( R unitVec I ) : I --> B )
19 18 frnd 
 |-  ( ph -> ran ( R unitVec I ) C_ B )
20 eqid 
 |-  ( LSpan ` F ) = ( LSpan ` F )
21 2 20 10 lmhmlsp 
 |-  ( ( E e. ( F LMHom T ) /\ ran ( R unitVec I ) C_ B ) -> ( E " ( ( LSpan ` F ) ` ran ( R unitVec I ) ) ) = ( K ` ( E " ran ( R unitVec I ) ) ) )
22 11 19 21 syl2anc 
 |-  ( ph -> ( E " ( ( LSpan ` F ) ` ran ( R unitVec I ) ) ) = ( K ` ( E " ran ( R unitVec I ) ) ) )
23 2 3 lmhmf 
 |-  ( E e. ( F LMHom T ) -> E : B --> C )
24 11 23 syl 
 |-  ( ph -> E : B --> C )
25 24 ffnd 
 |-  ( ph -> E Fn B )
26 fnima 
 |-  ( E Fn B -> ( E " B ) = ran E )
27 25 26 syl 
 |-  ( ph -> ( E " B ) = ran E )
28 eqid 
 |-  ( LBasis ` F ) = ( LBasis ` F )
29 1 16 28 frlmlbs 
 |-  ( ( R e. Ring /\ I e. X ) -> ran ( R unitVec I ) e. ( LBasis ` F ) )
30 15 7 29 syl2anc 
 |-  ( ph -> ran ( R unitVec I ) e. ( LBasis ` F ) )
31 2 28 20 lbssp 
 |-  ( ran ( R unitVec I ) e. ( LBasis ` F ) -> ( ( LSpan ` F ) ` ran ( R unitVec I ) ) = B )
32 30 31 syl 
 |-  ( ph -> ( ( LSpan ` F ) ` ran ( R unitVec I ) ) = B )
33 32 eqcomd 
 |-  ( ph -> B = ( ( LSpan ` F ) ` ran ( R unitVec I ) ) )
34 33 imaeq2d 
 |-  ( ph -> ( E " B ) = ( E " ( ( LSpan ` F ) ` ran ( R unitVec I ) ) ) )
35 27 34 eqtr3d 
 |-  ( ph -> ran E = ( E " ( ( LSpan ` F ) ` ran ( R unitVec I ) ) ) )
36 imaco 
 |-  ( ( E o. ( R unitVec I ) ) " I ) = ( E " ( ( R unitVec I ) " I ) )
37 9 ffnd 
 |-  ( ph -> A Fn I )
38 18 ffnd 
 |-  ( ph -> ( R unitVec I ) Fn I )
39 fnco 
 |-  ( ( E Fn B /\ ( R unitVec I ) Fn I /\ ran ( R unitVec I ) C_ B ) -> ( E o. ( R unitVec I ) ) Fn I )
40 25 38 19 39 syl3anc 
 |-  ( ph -> ( E o. ( R unitVec I ) ) Fn I )
41 fvco2 
 |-  ( ( ( R unitVec I ) Fn I /\ u e. I ) -> ( ( E o. ( R unitVec I ) ) ` u ) = ( E ` ( ( R unitVec I ) ` u ) ) )
42 38 41 sylan 
 |-  ( ( ph /\ u e. I ) -> ( ( E o. ( R unitVec I ) ) ` u ) = ( E ` ( ( R unitVec I ) ` u ) ) )
43 6 adantr 
 |-  ( ( ph /\ u e. I ) -> T e. LMod )
44 7 adantr 
 |-  ( ( ph /\ u e. I ) -> I e. X )
45 8 adantr 
 |-  ( ( ph /\ u e. I ) -> R = ( Scalar ` T ) )
46 9 adantr 
 |-  ( ( ph /\ u e. I ) -> A : I --> C )
47 simpr 
 |-  ( ( ph /\ u e. I ) -> u e. I )
48 1 2 3 4 5 43 44 45 46 47 16 frlmup2 
 |-  ( ( ph /\ u e. I ) -> ( E ` ( ( R unitVec I ) ` u ) ) = ( A ` u ) )
49 42 48 eqtr2d 
 |-  ( ( ph /\ u e. I ) -> ( A ` u ) = ( ( E o. ( R unitVec I ) ) ` u ) )
50 37 40 49 eqfnfvd 
 |-  ( ph -> A = ( E o. ( R unitVec I ) ) )
51 50 imaeq1d 
 |-  ( ph -> ( A " I ) = ( ( E o. ( R unitVec I ) ) " I ) )
52 fnima 
 |-  ( A Fn I -> ( A " I ) = ran A )
53 37 52 syl 
 |-  ( ph -> ( A " I ) = ran A )
54 51 53 eqtr3d 
 |-  ( ph -> ( ( E o. ( 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 
 |-  ( ph -> ( ( R unitVec I ) " I ) = ran ( R unitVec I ) )
57 56 imaeq2d 
 |-  ( ph -> ( E " ( ( R unitVec I ) " I ) ) = ( E " ran ( R unitVec I ) ) )
58 36 54 57 3eqtr3a 
 |-  ( ph -> ran A = ( E " ran ( R unitVec I ) ) )
59 58 fveq2d 
 |-  ( ph -> ( K ` ran A ) = ( K ` ( E " ran ( R unitVec I ) ) ) )
60 22 35 59 3eqtr4d 
 |-  ( ph -> ran E = ( K ` ran A ) )