srngplusg

Description: The addition operation 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	srngplusg	$⊢ \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		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
4		snsstp2	$⊢ \{⟨+_{ndx}, \underset{˙}{+}⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}$
5		ssun1	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨_{ndx}, \underset{˙}{}⟩\}$
6	5 1	sseqtrri	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \subseteq R$
7	4 6	sstri	$⊢ \{⟨+_{ndx}, \underset{˙}{+}⟩\} \subseteq R$
8	2 3 7	strfv	$⊢ \underset{˙}{+} \in X \to \underset{˙}{+} = +_{R}$

Metamath Proof Explorer