Theorem prdsvalstr

Description: Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 30-Apr-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Assertion	prdsvalstr	$$⊢\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{\bullet }⟩\right\}\right)\right)\mathrm{Struct}⟨1,15⟩$$

Proof

Step	Hyp	Ref	Expression
1		unass	$$⊢\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\right)\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{\bullet }⟩\right\}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{\bullet }⟩\right\}\right)$$
2		eqid	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}$$
3	2	imasvalstr	$$⊢\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\right)\mathrm{Struct}⟨1,12⟩$$
4		1nn0	$$⊢1\in {\mathbb{N}}_0$$
5		4nn	$$⊢4\in \mathbb{N}$$
6	4 5	decnncl	$$⊢14\in \mathbb{N}$$
7		homndx	$$⊢\mathrm{Hom}\left(\mathrm{ndx}\right)=14$$
8		4nn0	$$⊢4\in {\mathbb{N}}_0$$
9		5nn	$$⊢5\in \mathbb{N}$$
10		4lt5	$$⊢4<5$$
11	4 8 9 10	declt	$$⊢14<15$$
12	4 9	decnncl	$$⊢15\in \mathbb{N}$$
13		ccondx	$$⊢\mathrm{comp}\left(\mathrm{ndx}\right)=15$$
14	6 7 11 12 13	strle2	$$⊢\left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{\bullet }⟩\right\}\mathrm{Struct}⟨14,15⟩$$
15		2nn0	$$⊢2\in {\mathbb{N}}_0$$
16		2lt4	$$⊢2<4$$
17	4 15 5 16	declt	$$⊢12<14$$
18	3 14 17	strleun	$$⊢\left(\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\right)\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{\bullet }⟩\right\}\right)\mathrm{Struct}⟨1,15⟩$$
19	1 18	eqbrtrri	$$⊢\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{\times }⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),S⟩,⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),O⟩,⟨{\le }_{\mathrm{ndx}},L⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩\right\}\cup \left\{⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{\bullet }⟩\right\}\right)\right)\mathrm{Struct}⟨1,15⟩$$