Theorem 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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),T⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}$$
Assertion	phlstr	$$⊢H\mathrm{Struct}⟨1,8⟩$$

Proof

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