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