prds0g

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

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

Metamath Proof Explorer