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

Metamath Proof Explorer

Theorem prds1

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

Ref Expression
Hypotheses prds1.y 
|- Y = ( S Xs_ R )
prds1.i 
|- ( ph -> I e. W )
prds1.s 
|- ( ph -> S e. V )
prds1.r 
|- ( ph -> R : I --> Ring )
Assertion prds1 
|- ( ph -> ( 1r o. R ) = ( 1r ` Y ) )

Proof

Step Hyp Ref Expression
1 prds1.y 
 |-  Y = ( S Xs_ R )
2 prds1.i 
 |-  ( ph -> I e. W )
3 prds1.s 
 |-  ( ph -> S e. V )
4 prds1.r 
 |-  ( ph -> R : I --> Ring )
5 eqid 
 |-  ( S Xs_ ( mulGrp o. R ) ) = ( S Xs_ ( mulGrp o. R ) )
6 mgpf 
 |-  ( mulGrp |` Ring ) : Ring --> Mnd
7 fco2 
 |-  ( ( ( mulGrp |` Ring ) : Ring --> Mnd /\ R : I --> Ring ) -> ( mulGrp o. R ) : I --> Mnd )
8 6 4 7 sylancr 
 |-  ( ph -> ( mulGrp o. R ) : I --> Mnd )
9 5 2 3 8 prds0g 
 |-  ( ph -> ( 0g o. ( mulGrp o. R ) ) = ( 0g ` ( S Xs_ ( mulGrp o. R ) ) ) )
10 eqidd 
 |-  ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) ) )
11 eqid 
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
12 4 ffnd 
 |-  ( ph -> R Fn I )
13 1 11 5 2 3 12 prdsmgp 
 |-  ( ph -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) ) )
14 13 simpld 
 |-  ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( S Xs_ ( mulGrp o. R ) ) ) )
15 13 simprd 
 |-  ( ph -> ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) )
16 15 oveqdr 
 |-  ( ( ph /\ ( x e. ( Base ` ( mulGrp ` Y ) ) /\ y e. ( Base ` ( mulGrp ` Y ) ) ) ) -> ( x ( +g ` ( mulGrp ` Y ) ) y ) = ( x ( +g ` ( S Xs_ ( mulGrp o. R ) ) ) y ) )
17 10 14 16 grpidpropd 
 |-  ( ph -> ( 0g ` ( mulGrp ` Y ) ) = ( 0g ` ( S Xs_ ( mulGrp o. R ) ) ) )
18 9 17 eqtr4d 
 |-  ( ph -> ( 0g o. ( mulGrp o. R ) ) = ( 0g ` ( mulGrp ` Y ) ) )
19 df-ur 
 |-  1r = ( 0g o. mulGrp )
20 19 coeq1i 
 |-  ( 1r o. R ) = ( ( 0g o. mulGrp ) o. R )
21 coass 
 |-  ( ( 0g o. mulGrp ) o. R ) = ( 0g o. ( mulGrp o. R ) )
22 20 21 eqtri 
 |-  ( 1r o. R ) = ( 0g o. ( mulGrp o. R ) )
23 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
24 11 23 ringidval 
 |-  ( 1r ` Y ) = ( 0g ` ( mulGrp ` Y ) )
25 18 22 24 3eqtr4g 
 |-  ( ph -> ( 1r o. R ) = ( 1r ` Y ) )