srnginvl

Description: The involution function of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015)

		Ref	Expression
	Hypothesis	srngstr.r	$⊢ R = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨_{ndx}, \underset{˙}{}⟩\}$
	Assertion	srnginvl	$⊢ \underset{˙}{} \in X \to \underset{˙}{} = *_{R}$

Step	Hyp	Ref	Expression
1		srngstr.r	$⊢ R = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨_{ndx}, \underset{˙}{}⟩\}$
2	1	srngstr	$⊢ R Struct ⟨1, 4⟩$
3		starvid	$⊢ _{𝑟} = Slot _{ndx}$
4		ssun2	$⊢ \{⟨_{ndx}, \underset{˙}{}⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨_{ndx}, \underset{˙}{}⟩\}$
5	4 1	sseqtrri	$⊢ \{⟨_{ndx}, \underset{˙}{}⟩\} \subseteq R$
6	2 3 5	strfv	$⊢ \underset{˙}{} \in X \to \underset{˙}{} = *_{R}$

Metamath Proof Explorer