Definition df-hlhil

Description: Define our final Hilbert space constructed from a Hilbert lattice. (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Assertion	df-hlhil	$$⊢\mathrm{HLHil}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼⦋\mathrm{DVecH}\left(k\right)\left(w\right)/u⦌⦋{\mathrm{Base}}_u/v⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩,⟨{+}_{\mathrm{ndx}},{+}_u⟩,⟨\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 }_u⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlh	$$class\mathrm{HLHil}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vw	$$setvarw$$
4		clh	$$class\mathrm{LHyp}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class\mathrm{LHyp}\left(k\right)$$
7		cdvh	$$class\mathrm{DVecH}$$
8	5 7	cfv	$$class\mathrm{DVecH}\left(k\right)$$
9	3	cv	$$setvarw$$
10	9 8	cfv	$$class\mathrm{DVecH}\left(k\right)\left(w\right)$$
11		vu	$$setvaru$$
12		cbs	$$class\mathrm{Base}$$
13	11	cv	$$setvaru$$
14	13 12	cfv	$$class{\mathrm{Base}}_u$$
15		vv	$$setvarv$$
16		cnx	$$class\mathrm{ndx}$$
17	16 12	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
18	15	cv	$$setvarv$$
19	17 18	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩$$
20		cplusg	$$class{+}_{𝑔}$$
21	16 20	cfv	$$class{+}_{\mathrm{ndx}}$$
22	13 20	cfv	$$class{+}_u$$
23	21 22	cop	$$class⟨{+}_{\mathrm{ndx}},{+}_u⟩$$
24		csca	$$class\mathrm{Scalar}$$
25	16 24	cfv	$$class\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
26		cedring	$$class\mathrm{EDRing}$$
27	5 26	cfv	$$class\mathrm{EDRing}\left(k\right)$$
28	9 27	cfv	$$class\mathrm{EDRing}\left(k\right)\left(w\right)$$
29		csts	$$class\mathrm{sSet}$$
30		cstv	$$class{\ast }_{𝑟}$$
31	16 30	cfv	$$class{\mathrm{*}}_{\mathrm{ndx}}$$
32		chg	$$class\mathrm{HGMap}$$
33	5 32	cfv	$$class\mathrm{HGMap}\left(k\right)$$
34	9 33	cfv	$$class\mathrm{HGMap}\left(k\right)\left(w\right)$$
35	31 34	cop	$$class⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(k\right)\left(w\right)⟩$$
36	28 35 29	co	$$class\left(\mathrm{EDRing}\left(k\right)\left(w\right)\mathrm{sSet}⟨{\mathrm{*}}_{\mathrm{ndx}},\mathrm{HGMap}\left(k\right)\left(w\right)⟩\right)$$
37	25 36	cop	$$class⟨\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)⟩⟩$$
38	19 23 37	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩,⟨{+}_{\mathrm{ndx}},{+}_u⟩,⟨\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\}$$
39		cvsca	$$class{\cdot }_{𝑠}$$
40	16 39	cfv	$$class{\cdot }_{\mathrm{ndx}}$$
41	13 39	cfv	$$class{\cdot }_u$$
42	40 41	cop	$$class⟨{\cdot }_{\mathrm{ndx}},{\cdot }_u⟩$$
43		cip	$$class{\cdot }_{𝑖}$$
44	16 43	cfv	$$class{\cdot }_{𝑖}\left(\mathrm{ndx}\right)$$
45		vx	$$setvarx$$
46		vy	$$setvary$$
47		chdma	$$class\mathrm{HDMap}$$
48	5 47	cfv	$$class\mathrm{HDMap}\left(k\right)$$
49	9 48	cfv	$$class\mathrm{HDMap}\left(k\right)\left(w\right)$$
50	46	cv	$$setvary$$
51	50 49	cfv	$$class\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)$$
52	45	cv	$$setvarx$$
53	52 51	cfv	$$class\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)$$
54	45 46 18 18 53	cmpo	$$class\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)$$
55	44 54	cop	$$class⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩$$
56	42 55	cpr	$$class\left\{⟨{\cdot }_{\mathrm{ndx}},{\cdot }_u⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩\right\}$$
57	38 56	cun	$$class\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩,⟨{+}_{\mathrm{ndx}},{+}_u⟩,⟨\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 }_u⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)$$
58	15 14 57	csb	$$class⦋{\mathrm{Base}}_u/v⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩,⟨{+}_{\mathrm{ndx}},{+}_u⟩,⟨\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 }_u⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)$$
59	11 10 58	csb	$$class⦋\mathrm{DVecH}\left(k\right)\left(w\right)/u⦌⦋{\mathrm{Base}}_u/v⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩,⟨{+}_{\mathrm{ndx}},{+}_u⟩,⟨\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 }_u⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)$$
60	3 6 59	cmpt	$$class\left(w\in \mathrm{LHyp}\left(k\right)⟼⦋\mathrm{DVecH}\left(k\right)\left(w\right)/u⦌⦋{\mathrm{Base}}_u/v⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩,⟨{+}_{\mathrm{ndx}},{+}_u⟩,⟨\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 }_u⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)\right)$$
61	1 2 60	cmpt	$$class\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼⦋\mathrm{DVecH}\left(k\right)\left(w\right)/u⦌⦋{\mathrm{Base}}_u/v⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩,⟨{+}_{\mathrm{ndx}},{+}_u⟩,⟨\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 }_u⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)\right)\right)$$
62	0 61	wceq	$$wff\mathrm{HLHil}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼⦋\mathrm{DVecH}\left(k\right)\left(w\right)/u⦌⦋{\mathrm{Base}}_u/v⦌\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},v⟩,⟨{+}_{\mathrm{ndx}},{+}_u⟩,⟨\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 }_u⟩,⟨{\cdot }_{𝑖}\left(\mathrm{ndx}\right),\left(x\in v,y\in v⟼\mathrm{HDMap}\left(k\right)\left(w\right)\left(y\right)\left(x\right)\right)⟩\right\}\right)\right)\right)$$