phlstr

Description: A constructed pre-Hilbert space is a structure. Starting from lmodstr (which has 4 members), we chain strleun once more, adding an ordered pair to the function, to get all 5 members. (Contributed by Mario Carneiro, 1-Oct-2013) (Revised by Mario Carneiro, 29-Aug-2015)

		Ref	Expression
	Hypothesis	phlfn.h	$⊢ H = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
	Assertion	phlstr	$⊢ H Struct ⟨1, 8⟩$

Proof

Step	Hyp	Ref	Expression
1		phlfn.h	$⊢ H = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
2		df-pr	$⊢ \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} = \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
3	2	uneq2i	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup (\{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\})$
4		unass	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}) \cup \{⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup (\{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} \cup \{⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\})$
5	3 1 4	3eqtr4i	$⊢ H = (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}) \cup \{⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
6		eqid	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}$
7	6	lmodstr	$⊢ (\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}) Struct ⟨1, 6⟩$
8		8nn	$⊢ 8 \in ℕ$
9		ipndx	$⊢ \cdot_{𝑖} (ndx) = 8$
10	8 9	strle1	$⊢ \{⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} Struct ⟨8, 8⟩$
11		6lt8	$⊢ 6 < 8$
12	7 10 11	strleun	$⊢ ((\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), T⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩\}) \cup \{⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}) Struct ⟨1, 8⟩$
13	5 12	eqbrtri	$⊢ H Struct ⟨1, 8⟩$

Metamath Proof Explorer

Theorem phlstr

Proof