Metamath Proof Explorer

Theorem pwsbas

Description: Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Hypotheses pwsbas.y 
|- Y = ( R ^s I )
pwsbas.f 
|- B = ( Base ` R )
Assertion pwsbas 
|- ( ( R e. V /\ I e. W ) -> ( B ^m I ) = ( Base ` Y ) )

Proof

Step Hyp Ref Expression
1 pwsbas.y 
 |-  Y = ( R ^s I )
2 pwsbas.f 
 |-  B = ( Base ` R )
3 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
4 1 3 pwsval 
 |-  ( ( R e. V /\ I e. W ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
5 4 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` Y ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
6 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
7 fvexd 
 |-  ( ( R e. V /\ I e. W ) -> ( Scalar ` R ) e. _V )
8 simpr 
 |-  ( ( R e. V /\ I e. W ) -> I e. W )
9 snex 
 |-  { R } e. _V
10 xpexg 
 |-  ( ( I e. W /\ { R } e. _V ) -> ( I X. { R } ) e. _V )
11 8 9 10 sylancl 
 |-  ( ( R e. V /\ I e. W ) -> ( I X. { R } ) e. _V )
12 eqid 
 |-  ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
13 snnzg 
 |-  ( R e. V -> { R } =/= (/) )
14 13 adantr 
 |-  ( ( R e. V /\ I e. W ) -> { R } =/= (/) )
15 dmxp 
 |-  ( { R } =/= (/) -> dom ( I X. { R } ) = I )
16 14 15 syl 
 |-  ( ( R e. V /\ I e. W ) -> dom ( I X. { R } ) = I )
17 6 7 11 12 16 prdsbas 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = X_ x e. I ( Base ` ( ( I X. { R } ) ` x ) ) )
18 fvconst2g 
 |-  ( ( R e. V /\ x e. I ) -> ( ( I X. { R } ) ` x ) = R )
19 18 fveq2d 
 |-  ( ( R e. V /\ x e. I ) -> ( Base ` ( ( I X. { R } ) ` x ) ) = ( Base ` R ) )
20 19 ralrimiva 
 |-  ( R e. V -> A. x e. I ( Base ` ( ( I X. { R } ) ` x ) ) = ( Base ` R ) )
21 20 adantr 
 |-  ( ( R e. V /\ I e. W ) -> A. x e. I ( Base ` ( ( I X. { R } ) ` x ) ) = ( Base ` R ) )
22 ixpeq2 
 |-  ( A. x e. I ( Base ` ( ( I X. { R } ) ` x ) ) = ( Base ` R ) -> X_ x e. I ( Base ` ( ( I X. { R } ) ` x ) ) = X_ x e. I ( Base ` R ) )
23 21 22 syl 
 |-  ( ( R e. V /\ I e. W ) -> X_ x e. I ( Base ` ( ( I X. { R } ) ` x ) ) = X_ x e. I ( Base ` R ) )
24 17 23 eqtrd 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) = X_ x e. I ( Base ` R ) )
25 fvex 
 |-  ( Base ` R ) e. _V
26 ixpconstg 
 |-  ( ( I e. W /\ ( Base ` R ) e. _V ) -> X_ x e. I ( Base ` R ) = ( ( Base ` R ) ^m I ) )
27 8 25 26 sylancl 
 |-  ( ( R e. V /\ I e. W ) -> X_ x e. I ( Base ` R ) = ( ( Base ` R ) ^m I ) )
28 2 oveq1i 
 |-  ( B ^m I ) = ( ( Base ` R ) ^m I )
29 27 28 eqtr4di 
 |-  ( ( R e. V /\ I e. W ) -> X_ x e. I ( Base ` R ) = ( B ^m I ) )
30 5 24 29 3eqtrrd 
 |-  ( ( R e. V /\ I e. W ) -> ( B ^m I ) = ( Base ` Y ) )