rngstr

Description: A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013) (Revised by Mario Carneiro, 29-Aug-2015)

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

Step	Hyp	Ref	Expression
1		rngfn.r	$⊢ R = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}$
2		1nn	$⊢ 1 \in ℕ$
3		basendx	$⊢ {Base}_{ndx} = 1$
4		1lt2	$⊢ 1 < 2$
5		2nn	$⊢ 2 \in ℕ$
6		plusgndx	$⊢ +_{ndx} = 2$
7		2lt3	$⊢ 2 < 3$
8		3nn	$⊢ 3 \in ℕ$
9		mulrndx	$⊢ \cdot_{ndx} = 3$
10	2 3 4 5 6 7 8 9	strle3	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} Struct ⟨1, 3⟩$
11	1 10	eqbrtri	$⊢ R Struct ⟨1, 3⟩$

Metamath Proof Explorer