Theorem hlhilbase

Description: The base set of the final constructed Hilbert space. (Contributed by NM, 21-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)$$
	hlhilbase.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hlhilbase.m	$$⊢M={\mathrm{Base}}_L$$
Assertion	hlhilbase	$$⊢\phi \to M={\mathrm{Base}}_U$$

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		hlhilbase.l	$$⊢L=\mathrm{DVecH}\left(K\right)\left(W\right)$$
5		hlhilbase.m	$$⊢M={\mathrm{Base}}_L$$
6	5	fvexi	$$⊢M\in \mathrm{V}$$
7		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\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),\left(x\in M,y\in M⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\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),\left(x\in M,y\in M⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}$$
8	7	phlbase	$$⊢M\in \mathrm{V}\to M={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\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),\left(x\in M,y\in M⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)}$$
9	6 8	ax-mp	$$⊢M={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\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),\left(x\in M,y\in M⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)}$$
10		eqid	$$⊢{+}_L={+}_L$$
11		eqid	$$⊢\mathrm{EDRing}\left(K\right)\left(W\right)=\mathrm{EDRing}\left(K\right)\left(W\right)$$
12		eqid	$$⊢\mathrm{HGMap}\left(K\right)\left(W\right)=\mathrm{HGMap}\left(K\right)\left(W\right)$$
13		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)⟩$$
14		eqid	$$⊢{\cdot }_L={\cdot }_L$$
15		eqid	$$⊢\mathrm{HDMap}\left(K\right)\left(W\right)=\mathrm{HDMap}\left(K\right)\left(W\right)$$
16		eqid	$$⊢\left(x\in M,y\in M⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)=\left(x\in M,y\in M⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)$$
17	1 2 4 5 10 11 12 13 14 15 16 3	hlhilset	$$⊢\phi \to U=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\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),\left(x\in M,y\in M⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}$$
18	17	fveq2d	$$⊢\phi \to {\mathrm{Base}}_U={\mathrm{Base}}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},M⟩,⟨{+}_{\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),\left(x\in M,y\in M⟼\mathrm{HDMap}\left(K\right)\left(W\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)}$$
19	9 18	eqtr4id	$$⊢\phi \to M={\mathrm{Base}}_U$$