Theorem prds0g

Description: The identity in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015)

	Ref	Expression
Hypotheses	prdsmndd.y	$$⊢Y=S{⨉}_{𝑠}R$$
	prdsmndd.i	$$⊢\phi \to I\in W$$
	prdsmndd.s	$$⊢\phi \to S\in V$$
	prdsmndd.r	$$⊢\phi \to R:I⟶\mathrm{Mnd}$$
Assertion	prds0g	$$⊢\phi \to 0_{𝑔}\circ R=0_Y$$

Proof

Step	Hyp	Ref	Expression
1		prdsmndd.y	$$⊢Y=S{⨉}_{𝑠}R$$
2		prdsmndd.i	$$⊢\phi \to I\in W$$
3		prdsmndd.s	$$⊢\phi \to S\in V$$
4		prdsmndd.r	$$⊢\phi \to R:I⟶\mathrm{Mnd}$$
5		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
6		eqid	$$⊢{+}_Y={+}_Y$$
7	3	elexd	$$⊢\phi \to S\in \mathrm{V}$$
8	2	elexd	$$⊢\phi \to I\in \mathrm{V}$$
9		eqid	$$⊢0_{𝑔}\circ R=0_{𝑔}\circ R$$
10	1 5 6 7 8 4 9	prdsidlem	$$⊢\phi \to \left(0_{𝑔}\circ R\in {\mathrm{Base}}_Y\wedge \forall b\in {\mathrm{Base}}_Y\left(\left(0_{𝑔}\circ R\right){+}_{Y}b=b\wedge b{+}_Y\left(0_{𝑔}\circ R\right)=b\right)\right)$$
11		eqid	$$⊢0_Y=0_Y$$
12	1 2 3 4	prdsmndd	$$⊢\phi \to Y\in \mathrm{Mnd}$$
13	5 6	mndid	$$⊢Y\in \mathrm{Mnd}\to \exists a\in {\mathrm{Base}}_Y\forall b\in {\mathrm{Base}}_Y\left(a{+}_{Y}b=b\wedge b{+}_{Y}a=b\right)$$
14	12 13	syl	$$⊢\phi \to \exists a\in {\mathrm{Base}}_Y\forall b\in {\mathrm{Base}}_Y\left(a{+}_{Y}b=b\wedge b{+}_{Y}a=b\right)$$
15	5 11 6 14	ismgmid	$$⊢\phi \to \left(\left(0_{𝑔}\circ R\in {\mathrm{Base}}_Y\wedge \forall b\in {\mathrm{Base}}_Y\left(\left(0_{𝑔}\circ R\right){+}_{Y}b=b\wedge b{+}_Y\left(0_{𝑔}\circ R\right)=b\right)\right)\leftrightarrow 0_Y=0_{𝑔}\circ R\right)$$
16	10 15	mpbid	$$⊢\phi \to 0_Y=0_{𝑔}\circ R$$
17	16	eqcomd	$$⊢\phi \to 0_{𝑔}\circ R=0_Y$$