This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwsplusgval

Description: Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsplusgval.y 
|- Y = ( R ^s I )
pwsplusgval.b 
|- B = ( Base ` Y )
pwsplusgval.r 
|- ( ph -> R e. V )
pwsplusgval.i 
|- ( ph -> I e. W )
pwsplusgval.f 
|- ( ph -> F e. B )
pwsplusgval.g 
|- ( ph -> G e. B )
pwsplusgval.a 
|- .+ = ( +g ` R )
pwsplusgval.p 
|- .+b = ( +g ` Y )
Assertion pwsplusgval 
|- ( ph -> ( F .+b G ) = ( F oF .+ G ) )

Proof

Step Hyp Ref Expression
1 pwsplusgval.y 
 |-  Y = ( R ^s I )
2 pwsplusgval.b 
 |-  B = ( Base ` Y )
3 pwsplusgval.r 
 |-  ( ph -> R e. V )
4 pwsplusgval.i 
 |-  ( ph -> I e. W )
5 pwsplusgval.f 
 |-  ( ph -> F e. B )
6 pwsplusgval.g 
 |-  ( ph -> G e. B )
7 pwsplusgval.a 
 |-  .+ = ( +g ` R )
8 pwsplusgval.p 
 |-  .+b = ( +g ` Y )
9 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
10 eqid 
 |-  ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
11 fvexd 
 |-  ( ph -> ( Scalar ` R ) e. _V )
12 fnconstg 
 |-  ( R e. V -> ( I X. { R } ) Fn I )
13 3 12 syl 
 |-  ( ph -> ( I X. { R } ) Fn I )
14 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
15 1 14 pwsval 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
16 3 4 15 syl2anc 
 |-  ( ph -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
17 16 fveq2d 
 |-  ( ph -> ( Base ` Y ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
18 2 17 eqtrid 
 |-  ( ph -> B = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
19 5 18 eleqtrd 
 |-  ( ph -> F e. ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
20 6 18 eleqtrd 
 |-  ( ph -> G e. ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
21 eqid 
 |-  ( +g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( +g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
22 9 10 11 4 13 19 20 21 prdsplusgval 
 |-  ( ph -> ( F ( +g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) G ) = ( x e. I |-> ( ( F ` x ) ( +g ` ( ( I X. { R } ) ` x ) ) ( G ` x ) ) ) )
23 fvconst2g 
 |-  ( ( R e. V /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
24 3 23 sylan 
 |-  ( ( ph /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
25 24 fveq2d 
 |-  ( ( ph /\ x e. I ) -> ( +g ` ( ( I X. { R } ) ` x ) ) = ( +g ` R ) )
26 25 7 eqtr4di 
 |-  ( ( ph /\ x e. I ) -> ( +g ` ( ( I X. { R } ) ` x ) ) = .+ )
27 26 oveqd 
 |-  ( ( ph /\ x e. I ) -> ( ( F ` x ) ( +g ` ( ( I X. { R } ) ` x ) ) ( G ` x ) ) = ( ( F ` x ) .+ ( G ` x ) ) )
28 27 mpteq2dva 
 |-  ( ph -> ( x e. I |-> ( ( F ` x ) ( +g ` ( ( I X. { R } ) ` x ) ) ( G ` x ) ) ) = ( x e. I |-> ( ( F ` x ) .+ ( G ` x ) ) ) )
29 22 28 eqtrd 
 |-  ( ph -> ( F ( +g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) G ) = ( x e. I |-> ( ( F ` x ) .+ ( G ` x ) ) ) )
30 16 fveq2d 
 |-  ( ph -> ( +g ` Y ) = ( +g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
31 8 30 eqtrid 
 |-  ( ph -> .+b = ( +g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
32 31 oveqd 
 |-  ( ph -> ( F .+b G ) = ( F ( +g ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) G ) )
33 fvexd 
 |-  ( ( ph /\ x e. I ) -> ( F ` x ) e. _V )
34 fvexd 
 |-  ( ( ph /\ x e. I ) -> ( G ` x ) e. _V )
35 eqid 
 |-  ( Base ` R ) = ( Base ` R )
36 1 35 2 3 4 5 pwselbas 
 |-  ( ph -> F : I --> ( Base ` R ) )
37 36 feqmptd 
 |-  ( ph -> F = ( x e. I |-> ( F ` x ) ) )
38 1 35 2 3 4 6 pwselbas 
 |-  ( ph -> G : I --> ( Base ` R ) )
39 38 feqmptd 
 |-  ( ph -> G = ( x e. I |-> ( G ` x ) ) )
40 4 33 34 37 39 offval2 
 |-  ( ph -> ( F oF .+ G ) = ( x e. I |-> ( ( F ` x ) .+ ( G ` x ) ) ) )
41 29 32 40 3eqtr4d 
 |-  ( ph -> ( F .+b G ) = ( F oF .+ G ) )