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

Proof

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