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

Metamath Proof Explorer

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