This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ((\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨\cdot_{ndx}, \underset{˙}{\times}⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) \cup (\{⟨TopSet (ndx), O⟩, ⟨\leq_{ndx}, L⟩, ⟨dist (ndx), D⟩\} \cup \{⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{∙}⟩\})) Struct ⟨1, 15⟩$

Proof

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