Metamath Proof Explorer


Theorem prds1

Description: Value of the ring unit 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 ) )