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𝑠R
prds1.i φIW
prds1.s φSV
prds1.r φR:IRing
Assertion prds1 φ1rR=1Y

Proof

Step Hyp Ref Expression
1 prds1.y Y=S𝑠R
2 prds1.i φIW
3 prds1.s φSV
4 prds1.r φR:IRing
5 eqid S𝑠mulGrpR=S𝑠mulGrpR
6 mgpf mulGrpRing:RingMnd
7 fco2 mulGrpRing:RingMndR:IRingmulGrpR:IMnd
8 6 4 7 sylancr φmulGrpR:IMnd
9 5 2 3 8 prds0g φ0𝑔mulGrpR=0S𝑠mulGrpR
10 eqidd φBasemulGrpY=BasemulGrpY
11 eqid mulGrpY=mulGrpY
12 4 ffnd φRFnI
13 1 11 5 2 3 12 prdsmgp φBasemulGrpY=BaseS𝑠mulGrpR+mulGrpY=+S𝑠mulGrpR
14 13 simpld φBasemulGrpY=BaseS𝑠mulGrpR
15 13 simprd φ+mulGrpY=+S𝑠mulGrpR
16 15 oveqdr φxBasemulGrpYyBasemulGrpYx+mulGrpYy=x+S𝑠mulGrpRy
17 10 14 16 grpidpropd φ0mulGrpY=0S𝑠mulGrpR
18 9 17 eqtr4d φ0𝑔mulGrpR=0mulGrpY
19 df-ur 1r=0𝑔mulGrp
20 19 coeq1i 1rR=0𝑔mulGrpR
21 coass 0𝑔mulGrpR=0𝑔mulGrpR
22 20 21 eqtri 1rR=0𝑔mulGrpR
23 eqid 1Y=1Y
24 11 23 ringidval 1Y=0mulGrpY
25 18 22 24 3eqtr4g φ1rR=1Y