Definition df-hst 10264

Description: Define the set of complex Hilbert-space-valued states on a Hilbert lattice. Definition of CH-states in [Mayet3] p. 9.

Assertion

Ref	Expression
df-hst	|- CHStates = {f | (f:CH-->H~ /\ (normh` (f` H~)) = 1 /\ A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((f` x) .ih (f` y)) = 0 /\ (f` (x vH y)) = ((f` x) +h (f` y)))))}

Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-hst

Step	Hyp	Ref	Expression
1		chst 9012	. 2 class CHStates
2		cch 8978	. . . . 5 class CH
3		chil 8968	. . . . 5 class H~
4		vf	. . . . . 6 set f
5	4	cv 1098	. . . . 5 class f
6	2, 3, 5	wf 3141	. . . 4 wff f:CH-->H~
7	3, 5	cfv 3145	. . . . . 6 class (f` H~)
8		cno 8974	. . . . . 6 class normh
9	7, 8	cfv 3145	. . . . 5 class (normh` (f` H~))
10		c1 5158	. . . . 5 class 1
11	9, 10	wceq 1099	. . . 4 wff (normh` (f` H~)) = 1
12		vx	. . . . . . . . 9 set x
13	12	cv 1098	. . . . . . . 8 class x
14		vy	. . . . . . . . . 10 set y
15	14	cv 1098	. . . . . . . . 9 class y
16		cort 8979	. . . . . . . . 9 class _|_
17	15, 16	cfv 3145	. . . . . . . 8 class (_|_` y)
18	13, 17	wss 2018	. . . . . . 7 wff x (_ (_|_` y)
19	13, 5	cfv 3145	. . . . . . . . . 10 class (f` x)
20	15, 5	cfv 3145	. . . . . . . . . 10 class (f` y)
21		csp 8973	. . . . . . . . . 10 class .ih
22	19, 20, 21	co 3902	. . . . . . . . 9 class ((f` x) .ih (f` y))
23		cc0 5157	. . . . . . . . 9 class 0
24	22, 23	wceq 1099	. . . . . . . 8 wff ((f` x) .ih (f` y)) = 0
25		chj 8982	. . . . . . . . . . 11 class vH
26	13, 15, 25	co 3902	. . . . . . . . . 10 class (x vH y)
27	26, 5	cfv 3145	. . . . . . . . 9 class (f` (x vH y))
28		cva 8969	. . . . . . . . . 10 class +h
29	19, 20, 28	co 3902	. . . . . . . . 9 class ((f` x) +h (f` y))
30	27, 29	wceq 1099	. . . . . . . 8 wff (f` (x vH y)) = ((f` x) +h (f` y))
31	24, 30	wa 223	. . . . . . 7 wff (((f` x) .ih (f` y)) = 0 /\ (f` (x vH y)) = ((f` x) +h (f` y)))
32	18, 31	wi 3	. . . . . 6 wff (x (_ (_|_` y) -> (((f` x) .ih (f` y)) = 0 /\ (f` (x vH y)) = ((f` x) +h (f` y))))
33	32, 14, 2	wral 1621	. . . . 5 wff A.y e. CH (x (_ (_|_` y) -> (((f` x) .ih (f` y)) = 0 /\ (f` (x vH y)) = ((f` x) +h (f` y))))
34	33, 12, 2	wral 1621	. . . 4 wff A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((f` x) .ih (f` y)) = 0 /\ (f` (x vH y)) = ((f` x) +h (f` y))))
35	6, 11, 34	w3a 772	. . 3 wff (f:CH-->H~ /\ (normh` (f` H~)) = 1 /\ A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((f` x) .ih (f` y)) = 0 /\ (f` (x vH y)) = ((f` x) +h (f` y)))))
36	35, 4	cab 1440	. 2 class {f | (f:CH-->H~ /\ (normh` (f` H~)) = 1 /\ A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((f` x) .ih (f` y)) = 0 /\ (f` (x vH y)) = ((f` x) +h (f` y)))))}
37	1, 36	wceq 1099	1 wff CHStates = {f | (f:CH-->H~ /\ (normh` (f` H~)) = 1 /\ A.x e. CH A.y e. CH (x (_ (_|_` y) -> (((f` x) .ih (f` y)) = 0 /\ (f` (x vH y)) = ((f` x) +h (f` y)))))}

This definition is referenced by:  hstelt 10266

Copyright terms: Public domain