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

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 ) )