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

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	$⊢ \underset{˙}{} = _{𝑟𝑓} (R)$
	Assertion	srngcnv	$⊢ R \in -Ring \to \underset{˙}{} = {\underset{˙}{*}}^{-1}$

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