Metamath Proof Explorer

Theorem frlmup2

Description: The evaluation map has the intended behavior on the unit vectors. (Contributed by Stefan O'Rear, 7-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

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.y 
|- ( ph -> Y e. I )
frlmup.u 
|- U = ( R unitVec I )
Assertion frlmup2 
|- ( ph -> ( E ` ( U ` Y ) ) = ( A ` Y ) )

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.y 
 |-  ( ph -> Y e. I )
11 frlmup.u 
 |-  U = ( R unitVec I )
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 11 1 2 uvcff 
 |-  ( ( R e. Ring /\ I e. X ) -> U : I --> B )
17 15 7 16 syl2anc 
 |-  ( ph -> U : I --> B )
18 17 10 ffvelrnd 
 |-  ( ph -> ( U ` Y ) e. B )
19 oveq1 
 |-  ( x = ( U ` Y ) -> ( x oF .x. A ) = ( ( U ` Y ) oF .x. A ) )
20 19 oveq2d 
 |-  ( x = ( U ` Y ) -> ( T gsum ( x oF .x. A ) ) = ( T gsum ( ( U ` Y ) oF .x. A ) ) )
21 ovex 
 |-  ( T gsum ( ( U ` Y ) oF .x. A ) ) e. _V
22 20 5 21 fvmpt 
 |-  ( ( U ` Y ) e. B -> ( E ` ( U ` Y ) ) = ( T gsum ( ( U ` Y ) oF .x. A ) ) )
23 18 22 syl 
 |-  ( ph -> ( E ` ( U ` Y ) ) = ( T gsum ( ( U ` Y ) oF .x. A ) ) )
24 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
25 lmodcmn 
 |-  ( T e. LMod -> T e. CMnd )
26 cmnmnd 
 |-  ( T e. CMnd -> T e. Mnd )
27 6 25 26 3syl 
 |-  ( ph -> T e. Mnd )
28 eqid 
 |-  ( Base ` ( Scalar ` T ) ) = ( Base ` ( Scalar ` T ) )
29 eqid 
 |-  ( Base ` R ) = ( Base ` R )
30 1 29 2 frlmbasf 
 |-  ( ( I e. X /\ ( U ` Y ) e. B ) -> ( U ` Y ) : I --> ( Base ` R ) )
31 7 18 30 syl2anc 
 |-  ( ph -> ( U ` Y ) : I --> ( Base ` R ) )
32 8 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` T ) ) )
33 32 feq3d 
 |-  ( ph -> ( ( U ` Y ) : I --> ( Base ` R ) <-> ( U ` Y ) : I --> ( Base ` ( Scalar ` T ) ) ) )
34 31 33 mpbid 
 |-  ( ph -> ( U ` Y ) : I --> ( Base ` ( Scalar ` T ) ) )
35 12 28 4 3 6 34 9 7 lcomf 
 |-  ( ph -> ( ( U ` Y ) oF .x. A ) : I --> C )
36 31 ffnd 
 |-  ( ph -> ( U ` Y ) Fn I )
37 36 adantr 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( U ` Y ) Fn I )
38 9 ffnd 
 |-  ( ph -> A Fn I )
39 38 adantr 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> A Fn I )
40 7 adantr 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> I e. X )
41 eldifi 
 |-  ( x e. ( I \ { Y } ) -> x e. I )
42 41 adantl 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> x e. I )
43 fnfvof 
 |-  ( ( ( ( U ` Y ) Fn I /\ A Fn I ) /\ ( I e. X /\ x e. I ) ) -> ( ( ( U ` Y ) oF .x. A ) ` x ) = ( ( ( U ` Y ) ` x ) .x. ( A ` x ) ) )
44 37 39 40 42 43 syl22anc 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( ( U ` Y ) oF .x. A ) ` x ) = ( ( ( U ` Y ) ` x ) .x. ( A ` x ) ) )
45 15 adantr 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> R e. Ring )
46 10 adantr 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> Y e. I )
47 eldifsni 
 |-  ( x e. ( I \ { Y } ) -> x =/= Y )
48 47 necomd 
 |-  ( x e. ( I \ { Y } ) -> Y =/= x )
49 48 adantl 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> Y =/= x )
50 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
51 11 45 40 46 42 49 50 uvcvv0 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( U ` Y ) ` x ) = ( 0g ` R ) )
52 8 fveq2d 
 |-  ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` T ) ) )
53 52 adantr 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` T ) ) )
54 51 53 eqtrd 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( U ` Y ) ` x ) = ( 0g ` ( Scalar ` T ) ) )
55 54 oveq1d 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( ( U ` Y ) ` x ) .x. ( A ` x ) ) = ( ( 0g ` ( Scalar ` T ) ) .x. ( A ` x ) ) )
56 6 adantr 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> T e. LMod )
57 ffvelrn 
 |-  ( ( A : I --> C /\ x e. I ) -> ( A ` x ) e. C )
58 9 41 57 syl2an 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( A ` x ) e. C )
59 eqid 
 |-  ( 0g ` ( Scalar ` T ) ) = ( 0g ` ( Scalar ` T ) )
60 3 12 4 59 24 lmod0vs 
 |-  ( ( T e. LMod /\ ( A ` x ) e. C ) -> ( ( 0g ` ( Scalar ` T ) ) .x. ( A ` x ) ) = ( 0g ` T ) )
61 56 58 60 syl2anc 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( 0g ` ( Scalar ` T ) ) .x. ( A ` x ) ) = ( 0g ` T ) )
62 44 55 61 3eqtrd 
 |-  ( ( ph /\ x e. ( I \ { Y } ) ) -> ( ( ( U ` Y ) oF .x. A ) ` x ) = ( 0g ` T ) )
63 35 62 suppss 
 |-  ( ph -> ( ( ( U ` Y ) oF .x. A ) supp ( 0g ` T ) ) C_ { Y } )
64 3 24 27 7 10 35 63 gsumpt 
 |-  ( ph -> ( T gsum ( ( U ` Y ) oF .x. A ) ) = ( ( ( U ` Y ) oF .x. A ) ` Y ) )
65 fnfvof 
 |-  ( ( ( ( U ` Y ) Fn I /\ A Fn I ) /\ ( I e. X /\ Y e. I ) ) -> ( ( ( U ` Y ) oF .x. A ) ` Y ) = ( ( ( U ` Y ) ` Y ) .x. ( A ` Y ) ) )
66 36 38 7 10 65 syl22anc 
 |-  ( ph -> ( ( ( U ` Y ) oF .x. A ) ` Y ) = ( ( ( U ` Y ) ` Y ) .x. ( A ` Y ) ) )
67 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
68 11 15 7 10 67 uvcvv1 
 |-  ( ph -> ( ( U ` Y ) ` Y ) = ( 1r ` R ) )
69 8 fveq2d 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` T ) ) )
70 68 69 eqtrd 
 |-  ( ph -> ( ( U ` Y ) ` Y ) = ( 1r ` ( Scalar ` T ) ) )
71 70 oveq1d 
 |-  ( ph -> ( ( ( U ` Y ) ` Y ) .x. ( A ` Y ) ) = ( ( 1r ` ( Scalar ` T ) ) .x. ( A ` Y ) ) )
72 9 10 ffvelrnd 
 |-  ( ph -> ( A ` Y ) e. C )
73 eqid 
 |-  ( 1r ` ( Scalar ` T ) ) = ( 1r ` ( Scalar ` T ) )
74 3 12 4 73 lmodvs1 
 |-  ( ( T e. LMod /\ ( A ` Y ) e. C ) -> ( ( 1r ` ( Scalar ` T ) ) .x. ( A ` Y ) ) = ( A ` Y ) )
75 6 72 74 syl2anc 
 |-  ( ph -> ( ( 1r ` ( Scalar ` T ) ) .x. ( A ` Y ) ) = ( A ` Y ) )
76 66 71 75 3eqtrd 
 |-  ( ph -> ( ( ( U ` Y ) oF .x. A ) ` Y ) = ( A ` Y ) )
77 23 64 76 3eqtrd 
 |-  ( ph -> ( E ` ( U ` Y ) ) = ( A ` Y ) )