This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑌 ) )