Metamath Proof Explorer

Theorem xpsrnbas

Description: The indexed structure product that appears in xpsval has the same base as the target of the function F . (Contributed by Mario Carneiro, 15-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 xpsrnbas 
|- ( ph -> ran F = ( Base ` 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 eqid 
 |-  ( Base ` U ) = ( Base ` U )
10 7 fvexi 
 |-  G e. _V
11 10 a1i 
 |-  ( ph -> G e. _V )
12 2on 
 |-  2o e. On
13 12 a1i 
 |-  ( ph -> 2o e. On )
14 fnpr2o 
 |-  ( ( R e. V /\ S e. W ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
15 4 5 14 syl2anc 
 |-  ( ph -> { <. (/) , R >. , <. 1o , S >. } Fn 2o )
16 8 9 11 13 15 prdsbas2 
 |-  ( ph -> ( Base ` U ) = X_ k e. 2o ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) )
17 fvprif 
 |-  ( ( R e. V /\ S e. W /\ k e. 2o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = if ( k = (/) , R , S ) )
18 17 3expia 
 |-  ( ( R e. V /\ S e. W ) -> ( k e. 2o -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = if ( k = (/) , R , S ) ) )
19 4 5 18 syl2anc 
 |-  ( ph -> ( k e. 2o -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = if ( k = (/) , R , S ) ) )
20 19 imp 
 |-  ( ( ph /\ k e. 2o ) -> ( { <. (/) , R >. , <. 1o , S >. } ` k ) = if ( k = (/) , R , S ) )
21 20 fveq2d 
 |-  ( ( ph /\ k e. 2o ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( Base ` if ( k = (/) , R , S ) ) )
22 ifeq12 
 |-  ( ( X = ( Base ` R ) /\ Y = ( Base ` S ) ) -> if ( k = (/) , X , Y ) = if ( k = (/) , ( Base ` R ) , ( Base ` S ) ) )
23 2 3 22 mp2an 
 |-  if ( k = (/) , X , Y ) = if ( k = (/) , ( Base ` R ) , ( Base ` S ) )
24 fvif 
 |-  ( Base ` if ( k = (/) , R , S ) ) = if ( k = (/) , ( Base ` R ) , ( Base ` S ) )
25 23 24 eqtr4i 
 |-  if ( k = (/) , X , Y ) = ( Base ` if ( k = (/) , R , S ) )
26 21 25 eqtr4di 
 |-  ( ( ph /\ k e. 2o ) -> ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = if ( k = (/) , X , Y ) )
27 26 ixpeq2dva 
 |-  ( ph -> X_ k e. 2o ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = X_ k e. 2o if ( k = (/) , X , Y ) )
28 6 xpsfrn 
 |-  ran F = X_ k e. 2o if ( k = (/) , X , Y )
29 27 28 eqtr4di 
 |-  ( ph -> X_ k e. 2o ( Base ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ran F )
30 16 29 eqtr2d 
 |-  ( ph -> ran F = ( Base ` U ) )