Theorem idlsrgstr

Description: A constructed semiring of ideals is a structure. (Contributed by Thierry Arnoux, 1-Jun-2024)

	Ref	Expression
Hypothesis	idlsrgstr.1	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}$$
Assertion	idlsrgstr	$$⊢W\mathrm{Struct}⟨1,10⟩$$

Proof

Step	Hyp	Ref	Expression
1		idlsrgstr.1	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\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		9nn	$$⊢9\in \mathbb{N}$$
5		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
6		9lt10	$$⊢9<10$$
7		10nn	$$⊢10\in \mathbb{N}$$
8		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
9	4 5 6 7 8	strle2	$$⊢\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}\mathrm{Struct}⟨9,10⟩$$
10		3lt9	$$⊢3<9$$
11	3 9 10	strleun	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right\}\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}\right)\mathrm{Struct}⟨1,10⟩$$
12	1 11	eqbrtri	$$⊢W\mathrm{Struct}⟨1,10⟩$$