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

Metamath Proof Explorer

Theorem oppr0

Description: Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
oppr0.2 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion oppr0 0 = ( 0g ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 oppr0.2 ⊢ 0 = ( 0g ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
5 3 4 2 grpidval ⊢ 0 = ( ℩ 𝑦 ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑥 ) ) )
6 1 3 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
7 1 4 oppradd ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
8 eqid ⊢ ( 0g ‘ 𝑂 ) = ( 0g ‘ 𝑂 )
9 6 7 8 grpidval ⊢ ( 0g ‘ 𝑂 ) = ( ℩ 𝑦 ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 𝑥 ) ) )
10 5 9 eqtr4i ⊢ 0 = ( 0g ‘ 𝑂 )