Theorem hlhilplus

Description: The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-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)$$
	hlhilplus.a	$$⊢\underset{\dot{}}{+}={+}_L$$
Assertion	hlhilplus	$$⊢\phi \to \underset{\dot{}}{+}={+}_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		hlhilplus.a	$$⊢\underset{\dot{}}{+}={+}_L$$
6	5	fvexi	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
7		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\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 {\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}},\underset{\dot{}}{+}⟩,⟨\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 {\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	phlplusg	$$⊢\underset{\dot{}}{+}\in \mathrm{V}\to \underset{\dot{}}{+}={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\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 {\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{}}{+}={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\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 {\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	$$⊢\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 {\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 2 4 10 5 11 12 13 14 15 16 3	hlhilset	$$⊢\phi \to U=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\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 {\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 {+}_U={+}_{\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_L⟩,⟨{+}_{\mathrm{ndx}},\underset{\dot{}}{+}⟩,⟨\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 {\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{}}{+}={+}_U$$