Theorem hlhilip

Description: Inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilip.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hlhilip.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hlhilip.v	$$⊢V={\mathrm{Base}}_L$$
	hlhilip.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hlhilip.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhilip.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhilip.p	$$⊢\underset{\dot{}}{,}=\left(x\in V,y\in V⟼S\left(y\right)\left(x\right)\right)$$
Assertion	hlhilip	$$⊢\phi \to \underset{\dot{}}{,}={\cdot }_{𝑖}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlhilip.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhilip.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hlhilip.v	$$⊢V={\mathrm{Base}}_L$$
4		hlhilip.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
5		hlhilip.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
6		hlhilip.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		hlhilip.p	$$⊢\underset{\dot{}}{,}=\left(x\in V,y\in V⟼S\left(y\right)\left(x\right)\right)$$
8	3	fvexi	$$⊢V\in \mathrm{V}$$
9	8 8	mpoex	$$⊢\left(x\in V,y\in V⟼S\left(y\right)\left(x\right)\right)\in \mathrm{V}$$
10	7 9	eqeltri	$$⊢\underset{\dot{}}{,}\in \mathrm{V}$$
11		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨{+}_{\mathrm{ndx}},{+}_L⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_L⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨{+}_{\mathrm{ndx}},{+}_L⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_L⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}$$
12	11	phlip	$$⊢\underset{\dot{}}{,}\in \mathrm{V}\to \underset{\dot{}}{,}={\cdot }_{𝑖}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨{+}_{\mathrm{ndx}},{+}_L⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_L⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)$$
13	10 12	ax-mp	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨{+}_{\mathrm{ndx}},{+}_L⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_L⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)$$
14		eqid	$$⊢{+}_L={+}_L$$
15		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
16		eqid	$$⊢\mathrm{HGMap}\left(K\right)\left(W\right)=\mathrm{HGMap}\left(K\right)\left(W\right)$$
17		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩=\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩$$
18		eqid	$$⊢{\cdot }_L={\cdot }_L$$
19	1 5 2 3 14 15 16 17 18 4 7 6	hlhilset	$$⊢\phi \to U=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨{+}_{\mathrm{ndx}},{+}_L⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_L⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}$$
20	19	fveq2d	$$⊢\phi \to {\cdot }_{𝑖}\left(U\right)={\cdot }_{𝑖}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨{+}_{\mathrm{ndx}},{+}_L⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),\mathrm{EDRing}\left(K\right)\left(W\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(K\right)\left(W\right)⟩⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_L⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\underset{\dot{}}{,}⟩\right\}\right)$$
21	13 20	eqtr4id	$$⊢\phi \to \underset{\dot{}}{,}={\cdot }_{𝑖}\left(U\right)$$