odrngmulr

Description: The multiplication operation of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015)

		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	odrngmulr	$⊢ \underset{˙}{\cdot} \in V \to \underset{˙}{\cdot} = \cdot_{W}$

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	1	odrngstr	$⊢ W Struct ⟨1, 12⟩$
3		mulridx	$⊢ \cdot_{𝑟} = Slot \cdot_{ndx}$
4		snsstp3	$⊢ \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \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 \{⟨TopSet (ndx), J⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩, ⟨dist (ndx), D⟩\}$
6	5 1	sseqtrri	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \subseteq W$
7	4 6	sstri	$⊢ \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \subseteq W$
8	2 3 7	strfv	$⊢ \underset{˙}{\cdot} \in V \to \underset{˙}{\cdot} = \cdot_{W}$

Metamath Proof Explorer