Theorem prds0g

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

	Ref	Expression
Hypotheses	prdsmndd.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
	prdsmndd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsmndd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsmndd.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
Assertion	prds0g	⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = ( 0g ‘ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		prdsmndd.y	⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2		prdsmndd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3		prdsmndd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsmndd.r	⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Mnd )
5		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
6		eqid	⊢ ( +g ‘ 𝑌 ) = ( +g ‘ 𝑌 )
7	3	elexd	⊢ ( 𝜑 → 𝑆 ∈ V )
8	2	elexd	⊢ ( 𝜑 → 𝐼 ∈ V )
9		eqid	⊢ ( 0g ∘ 𝑅 ) = ( 0g ∘ 𝑅 )
10	1 5 6 7 8 4 9	prdsidlem	⊢ ( 𝜑 → ( ( 0g ∘ 𝑅 ) ∈ ( Base ‘ 𝑌 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( ( 0g ∘ 𝑅 ) ( +g ‘ 𝑌 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑌 ) ( 0g ∘ 𝑅 ) ) = 𝑏 ) ) )
11		eqid	⊢ ( 0g ‘ 𝑌 ) = ( 0g ‘ 𝑌 )
12	1 2 3 4	prdsmndd	⊢ ( 𝜑 → 𝑌 ∈ Mnd )
13	5 6	mndid	⊢ ( 𝑌 ∈ Mnd → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑌 ) 𝑎 ) = 𝑏 ) )
14	12 13	syl	⊢ ( 𝜑 → ∃ 𝑎 ∈ ( Base ‘ 𝑌 ) ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( 𝑎 ( +g ‘ 𝑌 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑌 ) 𝑎 ) = 𝑏 ) )
15	5 11 6 14	ismgmid	⊢ ( 𝜑 → ( ( ( 0g ∘ 𝑅 ) ∈ ( Base ‘ 𝑌 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝑌 ) ( ( ( 0g ∘ 𝑅 ) ( +g ‘ 𝑌 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑌 ) ( 0g ∘ 𝑅 ) ) = 𝑏 ) ) ↔ ( 0g ‘ 𝑌 ) = ( 0g ∘ 𝑅 ) ) )
16	10 15	mpbid	⊢ ( 𝜑 → ( 0g ‘ 𝑌 ) = ( 0g ∘ 𝑅 ) )
17	16	eqcomd	⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) = ( 0g ‘ 𝑌 ) )