Theorem srngring

Description: A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Assertion	srngring	⊢ ( 𝑅 ∈ *-Ring → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
2		eqid	⊢ ( *rf ‘ 𝑅 ) = ( *rf ‘ 𝑅 )
3	1 2	srngrhm	⊢ ( 𝑅 ∈ *-Ring → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) )
4		rhmrcl1	⊢ ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
5	3 4	syl	⊢ ( 𝑅 ∈ *-Ring → 𝑅 ∈ Ring )