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	$⊢ O = {opp}_{r} (R)$
	issrng.i	$⊢ \underset{˙}{} = _{𝑟𝑓} (R)$
Assertion	srngrhm	$⊢ R \in -Ring \to \underset{˙}{} \in (R RingHom O)$

Step	Hyp	Ref	Expression
1		issrng.o	$⊢ O = {opp}_{r} (R)$
2		issrng.i	$⊢ \underset{˙}{} = _{𝑟𝑓} (R)$
3	1 2	issrng	$⊢ R \in -Ring \leftrightarrow (\underset{˙}{} \in (R RingHom O) \land \underset{˙}{} = {\underset{˙}{}}^{-1})$
4	3	simplbi	$⊢ R \in -Ring \to \underset{˙}{} \in (R RingHom O)$