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	$$⊢\phi \to I\in W$$
	prds1.s	$$⊢\phi \to S\in V$$
	prds1.r	$$⊢\phi \to R:I⟶\mathrm{Ring}$$
Assertion	prds1	$$⊢\phi \to 1_r\circ R=1_Y$$

Proof

Step	Hyp	Ref	Expression
1		prds1.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prds1.i	$$⊢\phi \to I\in W$$
3		prds1.s	$$⊢\phi \to S\in V$$
4		prds1.r	$$⊢\phi \to R:I⟶\mathrm{Ring}$$
5		eqid	$$⊢S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)=S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)$$
6		mgpf	$$⊢\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right):\mathrm{Ring}⟶\mathrm{Mnd}$$
7		fco2	$$⊢\left(\left({\mathrm{mulGrp}\upharpoonright }_{\mathrm{Ring}}\right):\mathrm{Ring}⟶\mathrm{Mnd}\wedge R:I⟶\mathrm{Ring}\right)\to \left(\mathrm{mulGrp}\circ R\right):I⟶\mathrm{Mnd}$$
8	6 4 7	sylancr	$$⊢\phi \to \left(\mathrm{mulGrp}\circ R\right):I⟶\mathrm{Mnd}$$
9	5 2 3 8	prds0g	$$⊢\phi \to 0_{𝑔}\circ \left(\mathrm{mulGrp}\circ R\right)=0_{\left(S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)\right)}$$
10		eqidd	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}$$
11		eqid	$$⊢{\mathrm{mulGrp}}_Y={\mathrm{mulGrp}}_Y$$
12	4	ffnd	$$⊢\phi \to RFnI$$
13	1 11 5 2 3 12	prdsmgp	$$⊢\phi \to \left({\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}={\mathrm{Base}}_{\left(S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)\right)}\wedge {+}_{{\mathrm{mulGrp}}_Y}={+}_{\left(S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)\right)}\right)$$
14	13	simpld	$$⊢\phi \to {\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}={\mathrm{Base}}_{\left(S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)\right)}$$
15	13	simprd	$$⊢\phi \to {+}_{{\mathrm{mulGrp}}_Y}={+}_{\left(S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)\right)}$$
16	15	oveqdr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}\wedge y\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_Y}\right)\right)\to x{+}_{{\mathrm{mulGrp}}_Y}y=x{+}_{\left(S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)\right)}y$$
17	10 14 16	grpidpropd	$$⊢\phi \to 0_{{\mathrm{mulGrp}}_Y}=0_{\left(S{⨉}_{𝑠}\left(\mathrm{mulGrp}\circ R\right)\right)}$$
18	9 17	eqtr4d	$$⊢\phi \to 0_{𝑔}\circ \left(\mathrm{mulGrp}\circ R\right)=0_{{\mathrm{mulGrp}}_Y}$$
19		df-ur	$$⊢1_r=0_{𝑔}\circ \mathrm{mulGrp}$$
20	19	coeq1i	$$⊢1_r\circ R=\left(0_{𝑔}\circ \mathrm{mulGrp}\right)\circ R$$
21		coass	$$⊢\left(0_{𝑔}\circ \mathrm{mulGrp}\right)\circ R=0_{𝑔}\circ \left(\mathrm{mulGrp}\circ R\right)$$
22	20 21	eqtri	$$⊢1_r\circ R=0_{𝑔}\circ \left(\mathrm{mulGrp}\circ R\right)$$
23		eqid	$$⊢1_Y=1_Y$$
24	11 23	ringidval	$$⊢1_Y=0_{{\mathrm{mulGrp}}_Y}$$
25	18 22 24	3eqtr4g	$$⊢\phi \to 1_r\circ R=1_Y$$