Metamath Proof Explorer

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 ` R )
Assertion srngcnv 
|- ( R e. *Ring -> .* = `' .* )

Proof

Step Hyp Ref Expression
1 srngcnv.i 
 |-  .* = ( *rf ` R )
2 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
3 2 1 issrng 
 |-  ( R e. *Ring <-> ( .* e. ( R RingHom ( oppR ` R ) ) /\ .* = `' .* ) )
4 3 simprbi 
 |-  ( R e. *Ring -> .* = `' .* )