Metamath Proof Explorer


Theorem prds0g

Description: Zero 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𝑌 ) )