Definition df-hst 10421

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 9107	. 2 class CHStates
2		cch 9073	. . . . 5 class CH
3		chil 9063	. . . . 5 class H~
4		vf	. . . . . 6 set f
5	4	cv 991	. . . . 5 class f
6	2, 3, 5	wf 3259	. . . 4 wff f:CH-->H~
7	3, 5	cfv 3263	. . . . . 6 class (f` H~)
8		cno 9069	. . . . . 6 class normh
9	7, 8	cfv 3263	. . . . 5 class (normh` (f` H~))
10		c1 5389	. . . . 5 class 1
11	9, 10	wceq 992	. . . 4 wff (normh` (f` H~)) = 1
12		vx	. . . . . . . . 9 set x
13	12	cv 991	. . . . . . . 8 class x
14		vy	. . . . . . . . . 10 set y
15	14	cv 991	. . . . . . . . 9 class y
16		cort 9074	. . . . . . . . 9 class _|_
17	15, 16	cfv 3263	. . . . . . . 8 class (_|_` y)
18	13, 17	wss 2099	. . . . . . 7 wff x (_ (_|_` y)
19	13, 5	cfv 3263	. . . . . . . . . 10 class (f` x)
20	15, 5	cfv 3263	. . . . . . . . . 10 class (f` y)
21		csp 9068	. . . . . . . . . 10 class .ih
22	19, 20, 21	co 4021	. . . . . . . . 9 class ((f` x) .ih (f` y))
23		cc0 5388	. . . . . . . . 9 class 0
24	22, 23	wceq 992	. . . . . . . 8 wff ((f` x) .ih (f` y)) = 0
25		chj 9077	. . . . . . . . . . 11 class vH
26	13, 15, 25	co 4021	. . . . . . . . . 10 class (x vH y)
27	26, 5	cfv 3263	. . . . . . . . 9 class (f` (x vH y))
28		cva 9064	. . . . . . . . . 10 class +h
29	19, 20, 28	co 4021	. . . . . . . . 9 class ((f` x) +h (f` y))
30	27, 29	wceq 992	. . . . . . . 8 wff (f` (x vH y)) = ((f` x) +h (f` y))
31	24, 30	wa 221	. . . . . . 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 1691	. . . . 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 1691	. . . 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 781	. . 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 1505	. 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 992	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:  hstel 10423

Copyright terms: Public domain