Metamath Proof Explorer
Description: The involution function in a star ring is an antiautomorphism.
(Contributed by Mario Carneiro, 6Oct2015)


Ref 
Expression 

Hypotheses 
issrng.o 
⊢ 𝑂 = ( opp_{r} ‘ 𝑅 ) 


issrng.i 
⊢ ∗ = ( *_{rf} ‘ 𝑅 ) 

Assertion 
srngrhm 
⊢ ( 𝑅 ∈ *Ring → ∗ ∈ ( 𝑅 RingHom 𝑂 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

issrng.o 
⊢ 𝑂 = ( opp_{r} ‘ 𝑅 ) 
2 

issrng.i 
⊢ ∗ = ( *_{rf} ‘ 𝑅 ) 
3 
1 2

issrng 
⊢ ( 𝑅 ∈ *Ring ↔ ( ∗ ∈ ( 𝑅 RingHom 𝑂 ) ∧ ∗ = ^{◡} ∗ ) ) 
4 
3

simplbi 
⊢ ( 𝑅 ∈ *Ring → ∗ ∈ ( 𝑅 RingHom 𝑂 ) ) 