srngcl

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

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

Step	Hyp	Ref	Expression
1		srngcl.i	$⊢ \underset{˙}{} = _{R}$
2		srngcl.b	$⊢ B = {Base}_{R}$
3		eqid	$⊢ _{𝑟𝑓} (R) = _{𝑟𝑓} (R)$
4	2 1 3	stafval	$⊢ X \in B \to _{𝑟𝑓} (R) (X) = \underset{˙}{} (X)$
5	4	adantl	$⊢ (R \in -Ring \land X \in B) \to _{𝑟𝑓} (R) (X) = \underset{˙}{*} (X)$
6	3 2	srngf1o	$⊢ R \in -Ring \to _{𝑟𝑓} (R) : B \underset{1-1 onto}{⟶} B$
7		f1of	$⊢ _{𝑟𝑓} (R) : B \underset{1-1 onto}{⟶} B \to _{𝑟𝑓} (R) : B ⟶ B$
8	6 7	syl	$⊢ R \in -Ring \to _{𝑟𝑓} (R) : B ⟶ B$
9	8	ffvelcdmda	$⊢ (R \in -Ring \land X \in B) \to _{𝑟𝑓} (R) (X) \in B$
10	5 9	eqeltrrd	$⊢ (R \in -Ring \land X \in B) \to \underset{˙}{} (X) \in B$

Metamath Proof Explorer