Metamath Proof Explorer

Theorem xpssca

Description: Value of the scalar field of a binary structure product. For concreteness, we choose the scalar field to match the left argument, but in most cases where this slot is meaningful both factors will have the same scalar field, so that it doesn't matter which factor is chosen. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypotheses xpssca.t 
|- T = ( R Xs. S )
xpssca.g 
|- G = ( Scalar ` R )
xpssca.1 
|- ( ph -> R e. V )
xpssca.2 
|- ( ph -> S e. W )
Assertion xpssca 
|- ( ph -> G = ( Scalar ` T ) )

Proof

Step Hyp Ref Expression
1 xpssca.t 
 |-  T = ( R Xs. S )
2 xpssca.g 
 |-  G = ( Scalar ` R )
3 xpssca.1 
 |-  ( ph -> R e. V )
4 xpssca.2 
 |-  ( ph -> S e. W )
5 eqid 
 |-  ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( G Xs_ { <. (/) , R >. , <. 1o , S >. } )
6 2 fvexi 
 |-  G e. _V
7 6 a1i 
 |-  ( ph -> G e. _V )
8 prex 
 |-  { <. (/) , R >. , <. 1o , S >. } e. _V
9 8 a1i 
 |-  ( ph -> { <. (/) , R >. , <. 1o , S >. } e. _V )
10 5 7 9 prdssca 
 |-  ( ph -> G = ( Scalar ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 eqid 
 |-  ( Base ` S ) = ( Base ` S )
13 eqid 
 |-  ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )
14 1 11 12 3 4 13 2 5 xpsval 
 |-  ( ph -> T = ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
15 1 11 12 3 4 13 2 5 xpsrnbas 
 |-  ( ph -> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) )
16 13 xpsff1o2 
 |-  ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } )
17 f1ocnv 
 |-  ( ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ( ( Base ` R ) X. ( Base ` S ) ) -1-1-onto-> ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) )
18 16 17 mp1i 
 |-  ( ph -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) )
19 f1ofo 
 |-  ( `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( ( Base ` R ) X. ( Base ` S ) ) -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -onto-> ( ( Base ` R ) X. ( Base ` S ) ) )
20 18 19 syl 
 |-  ( ph -> `' ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. ( Base ` R ) , y e. ( Base ` S ) |-> { <. (/) , x >. , <. 1o , y >. } ) -onto-> ( ( Base ` R ) X. ( Base ` S ) ) )
21 ovexd 
 |-  ( ph -> ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V )
22 eqid 
 |-  ( Scalar ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Scalar ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) )
23 14 15 20 21 22 imassca 
 |-  ( ph -> ( Scalar ` ( G Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Scalar ` T ) )
24 10 23 eqtrd 
 |-  ( ph -> G = ( Scalar ` T ) )