Theorem srngrhm

Description: The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Hypotheses	issrng.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
	issrng.i	⊢ ∗ = ( *rf ‘ 𝑅 )
Assertion	srngrhm	⊢ ( 𝑅 ∈ *-Ring → ∗ ∈ ( 𝑅 RingHom 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		issrng.o	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2		issrng.i	⊢ ∗ = ( *rf ‘ 𝑅 )
3	1 2	issrng	⊢ ( 𝑅 ∈ *-Ring ↔ ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) ∧ ∗ = ◡ ∗ ) )
4	3	simplbi	⊢ ( 𝑅 ∈ *-Ring → ∗ ∈ ( 𝑅 RingHom 𝑂 ) )