Theorem 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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}$$
Assertion	rngstr	$$⊢R\mathrm{Struct}⟨1,3⟩$$

Proof

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