Theorem srngcnv

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

	Ref	Expression
Hypothesis	srngcnv.i	⊢ ∗ = ( *rf ‘ 𝑅 )
Assertion	srngcnv	⊢ ( 𝑅 ∈ *-Ring → ∗ = ◡ ∗ )

Proof

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