Metamath Proof Explorer

Theorem srngnvl

Description: The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015)

		Ref	Expression
	Hypotheses	srngcl.i	$⊢ \underset{˙}{} = _{R}$
		srngcl.b	$⊢ B = {Base}_{R}$
	Assertion	srngnvl	$⊢ (R \in -Ring \land X \in B) \to \underset{˙}{} (\underset{˙}{*} (X)) = X$

Proof

Step	Hyp	Ref	Expression
1		srngcl.i	$⊢ \underset{˙}{} = _{R}$
2		srngcl.b	$⊢ B = {Base}_{R}$
3	1 2	srngcl	$⊢ (R \in -Ring \land X \in B) \to \underset{˙}{} (X) \in B$
4		eqid	$⊢ _{𝑟𝑓} (R) = _{𝑟𝑓} (R)$
5	2 1 4	stafval	$⊢ \underset{˙}{} (X) \in B \to _{𝑟𝑓} (R) (\underset{˙}{} (X)) = \underset{˙}{} (\underset{˙}{*} (X))$
6	3 5	syl	$⊢ (R \in -Ring \land X \in B) \to _{𝑟𝑓} (R) (\underset{˙}{} (X)) = \underset{˙}{} (\underset{˙}{*} (X))$
7	4	srngcnv	$⊢ R \in -Ring \to _{𝑟𝑓} (R) = {*_{𝑟𝑓} (R)}^{-1}$
8	7	adantr	$⊢ (R \in -Ring \land X \in B) \to _{𝑟𝑓} (R) = {*_{𝑟𝑓} (R)}^{-1}$
9	8	fveq1d	$⊢ (R \in -Ring \land X \in B) \to _{𝑟𝑓} (R) (_{𝑟𝑓} (R) (X)) = {_{𝑟𝑓} (R)}^{-1} (*_{𝑟𝑓} (R) (X))$
10	2 1 4	stafval	$⊢ X \in B \to _{𝑟𝑓} (R) (X) = \underset{˙}{} (X)$
11	10	adantl	$⊢ (R \in -Ring \land X \in B) \to _{𝑟𝑓} (R) (X) = \underset{˙}{*} (X)$
12	11	fveq2d	$⊢ (R \in -Ring \land X \in B) \to _{𝑟𝑓} (R) (_{𝑟𝑓} (R) (X)) = _{𝑟𝑓} (R) (\underset{˙}{*} (X))$
13	4 2	srngf1o	$⊢ R \in -Ring \to _{𝑟𝑓} (R) : B \underset{1-1 onto}{⟶} B$
14		f1ocnvfv1	$⊢ (_{𝑟𝑓} (R) : B \underset{1-1 onto}{⟶} B \land X \in B) \to {_{𝑟𝑓} (R)}^{-1} (*_{𝑟𝑓} (R) (X)) = X$
15	13 14	sylan	$⊢ (R \in -Ring \land X \in B) \to {_{𝑟𝑓} (R)}^{-1} (*_{𝑟𝑓} (R) (X)) = X$
16	9 12 15	3eqtr3d	$⊢ (R \in -Ring \land X \in B) \to _{𝑟𝑓} (R) (\underset{˙}{*} (X)) = X$
17	6 16	eqtr3d	$⊢ (R \in -Ring \land X \in B) \to \underset{˙}{} (\underset{˙}{*} (X)) = X$