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

Metamath Proof Explorer

Theorem pws1

Description: Value of the ring unity in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Hypotheses pws1.y 
|- Y = ( R ^s I )
pws1.o 
|- .1. = ( 1r ` R )
Assertion pws1 
|- ( ( R e. Ring /\ I e. V ) -> ( I X. { .1. } ) = ( 1r ` Y ) )

Proof

Step Hyp Ref Expression
1 pws1.y 
 |-  Y = ( R ^s I )
2 pws1.o 
 |-  .1. = ( 1r ` R )
3 eqid 
 |-  ( Scalar ` R ) = ( Scalar ` R )
4 1 3 pwsval 
 |-  ( ( R e. Ring /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
5 4 fveq2d 
 |-  ( ( R e. Ring /\ I e. V ) -> ( 1r ` Y ) = ( 1r ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
6 eqid 
 |-  ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
7 simpr 
 |-  ( ( R e. Ring /\ I e. V ) -> I e. V )
8 fvexd 
 |-  ( ( R e. Ring /\ I e. V ) -> ( Scalar ` R ) e. _V )
9 fconst6g 
 |-  ( R e. Ring -> ( I X. { R } ) : I --> Ring )
10 9 adantr 
 |-  ( ( R e. Ring /\ I e. V ) -> ( I X. { R } ) : I --> Ring )
11 6 7 8 10 prds1 
 |-  ( ( R e. Ring /\ I e. V ) -> ( 1r o. ( I X. { R } ) ) = ( 1r ` ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) ) )
12 fn0g 
 |-  0g Fn _V
13 fnmgp 
 |-  mulGrp Fn _V
14 ssv 
 |-  ran mulGrp C_ _V
15 14 a1i 
 |-  ( ( R e. Ring /\ I e. V ) -> ran mulGrp C_ _V )
16 fnco 
 |-  ( ( 0g Fn _V /\ mulGrp Fn _V /\ ran mulGrp C_ _V ) -> ( 0g o. mulGrp ) Fn _V )
17 12 13 15 16 mp3an12i 
 |-  ( ( R e. Ring /\ I e. V ) -> ( 0g o. mulGrp ) Fn _V )
18 df-ur 
 |-  1r = ( 0g o. mulGrp )
19 18 fneq1i 
 |-  ( 1r Fn _V <-> ( 0g o. mulGrp ) Fn _V )
20 17 19 sylibr 
 |-  ( ( R e. Ring /\ I e. V ) -> 1r Fn _V )
21 elex 
 |-  ( R e. Ring -> R e. _V )
22 21 adantr 
 |-  ( ( R e. Ring /\ I e. V ) -> R e. _V )
23 fcoconst 
 |-  ( ( 1r Fn _V /\ R e. _V ) -> ( 1r o. ( I X. { R } ) ) = ( I X. { ( 1r ` R ) } ) )
24 20 22 23 syl2anc 
 |-  ( ( R e. Ring /\ I e. V ) -> ( 1r o. ( I X. { R } ) ) = ( I X. { ( 1r ` R ) } ) )
25 2 sneqi 
 |-  { .1. } = { ( 1r ` R ) }
26 25 xpeq2i 
 |-  ( I X. { .1. } ) = ( I X. { ( 1r ` R ) } )
27 24 26 eqtr4di 
 |-  ( ( R e. Ring /\ I e. V ) -> ( 1r o. ( I X. { R } ) ) = ( I X. { .1. } ) )
28 5 11 27 3eqtr2rd 
 |-  ( ( R e. Ring /\ I e. V ) -> ( I X. { .1. } ) = ( 1r ` Y ) )