srngstr

Description: A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 14-Aug-2015)

		Ref	Expression
	Hypothesis	srngstr.r	$⊢ R = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨_{ndx}, \underset{˙}{}⟩\}$
	Assertion	srngstr	$⊢ R Struct ⟨1, 4⟩$

Step	Hyp	Ref	Expression
1		srngstr.r	$⊢ R = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨_{ndx}, \underset{˙}{}⟩\}$
2		eqid	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}$
3	2	rngstr	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} Struct ⟨1, 3⟩$
4		4nn	$⊢ 4 \in ℕ$
5		starvndx	$⊢ *_{ndx} = 4$
6	4 5	strle1	$⊢ \{⟨_{ndx}, \underset{˙}{}⟩\} Struct ⟨4, 4⟩$
7		3lt4	$⊢ 3 < 4$
8	3 6 7	strleun	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨_{ndx}, \underset{˙}{}⟩\}) Struct ⟨1, 4⟩$
9	1 8	eqbrtri	$⊢ R Struct ⟨1, 4⟩$

Metamath Proof Explorer