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	|- O = ( oppR ` R )
	issrng.i	|- .* = ( *rf ` R )
Assertion	srngrhm	|- ( R e. *Ring -> .* e. ( R RingHom O ) )

Proof

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