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	⊢ HLHil = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlh	⊢ HLHil
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		cdvh	⊢ DVecH
8	5 7	cfv	⊢ ( DVecH ‘ 𝑘 )
9	3	cv	⊢ 𝑤
10	9 8	cfv	⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
11		vu	⊢ 𝑢
12		cbs	⊢ Base
13	11	cv	⊢ 𝑢
14	13 12	cfv	⊢ ( Base ‘ 𝑢 )
15		vv	⊢ 𝑣
16		cnx	⊢ ndx
17	16 12	cfv	⊢ ( Base ‘ ndx )
18	15	cv	⊢ 𝑣
19	17 18	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑣 ⟩
20		cplusg	⊢ +g
21	16 20	cfv	⊢ ( +g ‘ ndx )
22	13 20	cfv	⊢ ( +g ‘ 𝑢 )
23	21 22	cop	⊢ ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩
24		csca	⊢ Scalar
25	16 24	cfv	⊢ ( Scalar ‘ ndx )
26		cedring	⊢ EDRing
27	5 26	cfv	⊢ ( EDRing ‘ 𝑘 )
28	9 27	cfv	⊢ ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 )
29		csts	⊢ sSet
30		cstv	⊢ *𝑟
31	16 30	cfv	⊢ ( *𝑟 ‘ ndx )
32		chg	⊢ HGMap
33	5 32	cfv	⊢ ( HGMap ‘ 𝑘 )
34	9 33	cfv	⊢ ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 )
35	31 34	cop	⊢ ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩
36	28 35 29	co	⊢ ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ )
37	25 36	cop	⊢ ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩
38	19 23 37	ctp	⊢ { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ }
39		cvsca	⊢ ·𝑠
40	16 39	cfv	⊢ ( ·𝑠 ‘ ndx )
41	13 39	cfv	⊢ ( ·𝑠 ‘ 𝑢 )
42	40 41	cop	⊢ ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩
43		cip	⊢ ·𝑖
44	16 43	cfv	⊢ ( ·𝑖 ‘ ndx )
45		vx	⊢ 𝑥
46		vy	⊢ 𝑦
47		chdma	⊢ HDMap
48	5 47	cfv	⊢ ( HDMap ‘ 𝑘 )
49	9 48	cfv	⊢ ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 )
50	46	cv	⊢ 𝑦
51	50 49	cfv	⊢ ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 )
52	45	cv	⊢ 𝑥
53	52 51	cfv	⊢ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 )
54	45 46 18 18 53	cmpo	⊢ ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) )
55	44 54	cop	⊢ ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩
56	42 55	cpr	⊢ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ }
57	38 56	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } )
58	15 14 57	csb	⊢ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } )
59	11 10 58	csb	⊢ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } )
60	3 6 59	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) )
61	1 2 60	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )
62	0 61	wceq	⊢ HLHil = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ⦋ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) / 𝑢 ⦌ ⦋ ( Base ‘ 𝑢 ) / 𝑣 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑣 ⟩ , ⟨ ( +g ‘ ndx ) , ( +g ‘ 𝑢 ) ⟩ , ⟨ ( Scalar ‘ ndx ) , ( ( ( EDRing ‘ 𝑘 ) ‘ 𝑤 ) sSet ⟨ ( *𝑟 ‘ ndx ) , ( ( HGMap ‘ 𝑘 ) ‘ 𝑤 ) ⟩ ) ⟩ } ∪ { ⟨ ( ·𝑠 ‘ ndx ) , ( ·𝑠 ‘ 𝑢 ) ⟩ , ⟨ ( ·𝑖 ‘ ndx ) , ( 𝑥 ∈ 𝑣 , 𝑦 ∈ 𝑣 ↦ ( ( ( ( HDMap ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑦 ) ‘ 𝑥 ) ) ⟩ } ) ) )