Theorem hlhilsca

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

	Ref	Expression
Hypotheses	hlhilbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hlhilbase.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
	hlhilbase.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hlhilsca.e	$$⊢E=\mathrm{EDRing}\left(K\right)\left(W\right)$$
	hlhilsca.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hlhilsca.r	$$⊢R=E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},G⟩$$
Assertion	hlhilsca	$$⊢\phi \to R=\mathrm{Scalar}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlhilbase.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hlhilbase.u	$$⊢U=\mathrm{HLHil}\left(K\right)\left(W\right)$$
3		hlhilbase.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
4		hlhilsca.e	$$⊢E=\mathrm{EDRing}\left(K\right)\left(W\right)$$
5		hlhilsca.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
6		hlhilsca.r	$$⊢R=E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},G⟩$$
7		ovex	$$⊢E\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},G⟩\in \mathrm{V}$$
8	6 7	eqeltri	$$⊢R\in \mathrm{V}$$
9		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)},y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)},y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}$$
10	9	phlsca	$$⊢R\in \mathrm{V}\to R=\mathrm{Scalar}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)},y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)$$
11	8 10	ax-mp	$$⊢R=\mathrm{Scalar}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)},y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)$$
12		eqid	$$⊢\mathrm{DVecH}\left(K\right)\left(W\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
13		eqid	$$⊢{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
14		eqid	$$⊢{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}={+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
15		eqid	$$⊢{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}={\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}$$
16		eqid	$$⊢\mathrm{HDMap}\left(K\right)\left(W\right)=\mathrm{HDMap}\left(K\right)\left(W\right)$$
17		eqid	$$⊢\left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)},y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)=\left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)},y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)$$
18	1 2 12 13 14 4 5 6 15 16 17 3	hlhilset	$$⊢\phi \to U=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)},y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}$$
19	18	fveq2d	$$⊢\phi \to \mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{+}_{\mathrm{ndx}},{+}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)},y\in {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(W\right)}⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)$$
20	11 19	eqtr4id	$$⊢\phi \to R=\mathrm{Scalar}\left(U\right)$$