Metamath Proof Explorer

Theorem xpsval

Description: Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Jim Kingdon, 25-Sep-2023)

Ref Expression
Hypotheses xpsval.t 
|- T = ( R Xs. S )
xpsval.x 
|- X = ( Base ` R )
xpsval.y 
|- Y = ( Base ` S )
xpsval.1 
|- ( ph -> R e. V )
xpsval.2 
|- ( ph -> S e. W )
xpsval.f 
|- F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
xpsval.k 
|- G = ( Scalar ` R )
xpsval.u 
|- U = ( G Xs_ { <. (/) , R >. , <. 1o , S >. } )
Assertion xpsval 
|- ( ph -> T = ( `' F "s U ) )

Proof

Step Hyp Ref Expression
1 xpsval.t 
 |-  T = ( R Xs. S )
2 xpsval.x 
 |-  X = ( Base ` R )
3 xpsval.y 
 |-  Y = ( Base ` S )
4 xpsval.1 
 |-  ( ph -> R e. V )
5 xpsval.2 
 |-  ( ph -> S e. W )
6 xpsval.f 
 |-  F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )
7 xpsval.k 
 |-  G = ( Scalar ` R )
8 xpsval.u 
 |-  U = ( G Xs_ { <. (/) , R >. , <. 1o , S >. } )
9 4 elexd 
 |-  ( ph -> R e. _V )
10 5 elexd 
 |-  ( ph -> S e. _V )
11 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
12 11 2 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = X )
13 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
14 13 3 eqtr4di 
 |-  ( s = S -> ( Base ` s ) = Y )
15 mpoeq12 
 |-  ( ( ( Base ` r ) = X /\ ( Base ` s ) = Y ) -> ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
16 12 14 15 syl2an 
 |-  ( ( r = R /\ s = S ) -> ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )
17 16 6 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) = F )
18 17 cnveqd 
 |-  ( ( r = R /\ s = S ) -> `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) = `' F )
19 fveq2 
 |-  ( r = R -> ( Scalar ` r ) = ( Scalar ` R ) )
20 19 adantr 
 |-  ( ( r = R /\ s = S ) -> ( Scalar ` r ) = ( Scalar ` R ) )
21 20 7 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( Scalar ` r ) = G )
22 simpl 
 |-  ( ( r = R /\ s = S ) -> r = R )
23 22 opeq2d 
 |-  ( ( r = R /\ s = S ) -> <. (/) , r >. = <. (/) , R >. )
24 simpr 
 |-  ( ( r = R /\ s = S ) -> s = S )
25 24 opeq2d 
 |-  ( ( r = R /\ s = S ) -> <. 1o , s >. = <. 1o , S >. )
26 23 25 preq12d 
 |-  ( ( r = R /\ s = S ) -> { <. (/) , r >. , <. 1o , s >. } = { <. (/) , R >. , <. 1o , S >. } )
27 21 26 oveq12d 
 |-  ( ( r = R /\ s = S ) -> ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) = ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
28 27 8 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) = U )
29 18 28 oveq12d 
 |-  ( ( r = R /\ s = S ) -> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) ) = ( `' F "s U ) )
30 df-xps 
 |-  Xs. = ( r e. _V , s e. _V |-> ( `' ( x e. ( Base ` r ) , y e. ( Base ` s ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` r ) Xs_ { <. (/) , r >. , <. 1o , s >. } ) ) )
31 ovex 
 |-  ( `' F "s U ) e. _V
32 29 30 31 ovmpoa 
 |-  ( ( R e. _V /\ S e. _V ) -> ( R Xs. S ) = ( `' F "s U ) )
33 9 10 32 syl2anc 
 |-  ( ph -> ( R Xs. S ) = ( `' F "s U ) )
34 1 33 syl5eq 
 |-  ( ph -> T = ( `' F "s U ) )