odrngstr

Description: Functionality of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015) (Proof shortened by AV, 15-Sep-2021)

		Ref	Expression
	Hypothesis	odrngstr.w	$⊢ W = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨TopSet (ndx), J⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$
	Assertion	odrngstr	$⊢ W Struct ⟨1, 12⟩$

Step	Hyp	Ref	Expression
1		odrngstr.w	$⊢ W = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨TopSet (ndx), J⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$
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		9nn	$⊢ 9 \in ℕ$
5		tsetndx	$⊢ TopSet (ndx) = 9$
6		9lt10	$⊢ 9 < 10$
7		10nn	$⊢ 10 \in ℕ$
8		plendx	$⊢ \leq_{ndx} = 10$
9		1nn0	$⊢ 1 \in ℕ_{0}$
10		0nn0	$⊢ 0 \in ℕ_{0}$
11		2nn	$⊢ 2 \in ℕ$
12		2pos	$⊢ 0 < 2$
13	9 10 11 12	declt	$⊢ 10 < 12$
14	9 11	decnncl	$⊢ 12 \in ℕ$
15		dsndx	$⊢ dist (ndx) = 12$
16	4 5 6 7 8 13 14 15	strle3	$⊢ \{⟨TopSet (ndx), J⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\} Struct ⟨9, 12⟩$
17		3lt9	$⊢ 3 < 9$
18	3 16 17	strleun	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨TopSet (ndx), J⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}) Struct ⟨1, 12⟩$
19	1 18	eqbrtri	$⊢ W Struct ⟨1, 12⟩$

Metamath Proof Explorer