Theorem hlhilvsca

Description: The scalar product for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilvsca.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hlhilvsca.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hlhilvsca.t	$$⊢\underset{\dot{}}{·}={\cdot }_L$$
	hlhilvsca.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhilvsca.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	hlhilvsca	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_U$$

Proof

Step	Hyp	Ref	Expression
1		hlhilvsca.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhilvsca.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hlhilvsca.t	$$⊢\underset{\dot{}}{·}={\cdot }_L$$
4		hlhilvsca.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
5		hlhilvsca.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
6	3	fvexi	$$⊢\underset{\dot{}}{·}\in \mathrm{V}$$
7		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\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}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_L,y\in {\mathrm{Base}}_L⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\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}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_L,y\in {\mathrm{Base}}_L⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}$$
8	7	phlvsca	$$⊢\underset{\dot{}}{·}\in \mathrm{V}\to \underset{\dot{}}{·}={\cdot }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\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}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_L,y\in {\mathrm{Base}}_L⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)}$$
9	6 8	ax-mp	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\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}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_L,y\in {\mathrm{Base}}_L⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)}$$
10		eqid	$$⊢{\mathrm{Base}}_L={\mathrm{Base}}_L$$
11		eqid	$$⊢{+}_L={+}_L$$
12		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
13		eqid	$$⊢\mathrm{HGMap}\left(K\right)\left(W\right)=\mathrm{HGMap}\left(K\right)\left(W\right)$$
14		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)⟩$$
15		eqid	$$⊢\mathrm{HDMap}\left(K\right)\left(W\right)=\mathrm{HDMap}\left(K\right)\left(W\right)$$
16		eqid	$$⊢\left(x\in {\mathrm{Base}}_L,y\in {\mathrm{Base}}_L⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)=\left(x\in {\mathrm{Base}}_L,y\in {\mathrm{Base}}_L⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)$$
17	1 4 2 10 11 12 13 14 3 15 16 5	hlhilset	$$⊢\phi \to U=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\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}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_L,y\in {\mathrm{Base}}_L⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}$$
18	17	fveq2d	$$⊢\phi \to {\cdot }_U={\cdot }_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\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}},\underset{\dot{}}{·}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_L,y\in {\mathrm{Base}}_L⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)}$$
19	9 18	eqtr4id	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_U$$