Definition df-hst 10050

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 8771	. 2 class CHStates
2		cch 8737	. . . . 5 class CH
3		chil 8727	. . . . 5 class H~
4		vf	. . . . . 6 set f
5	4	cv 952	. . . . 5 class f
6	2, 3, 5	wf 3168	. . . 4 wff f:CH-->H~
7	3, 5	cfv 3172	. . . . . 6 class (f` H~)
8		cno 8733	. . . . . 6 class normh
9	7, 8	cfv 3172	. . . . 5 class (normh` (f` H~))
10		c1 5207	. . . . 5 class 1
11	9, 10	wceq 953	. . . 4 wff (normh` (f` H~)) = 1
12		vx	. . . . . . . . 9 set x
13	12	cv 952	. . . . . . . 8 class x
14		vy	. . . . . . . . . 10 set y
15	14	cv 952	. . . . . . . . 9 class y
16		cort 8738	. . . . . . . . 9 class _|_
17	15, 16	cfv 3172	. . . . . . . 8 class (_|_` y)
18	13, 17	wss 2037	. . . . . . 7 wff x (_ (_|_` y)
19	13, 5	cfv 3172	. . . . . . . . . 10 class (f` x)
20	15, 5	cfv 3172	. . . . . . . . . 10 class (f` y)
21		csp 8732	. . . . . . . . . 10 class .ih
22	19, 20, 21	co 3948	. . . . . . . . 9 class ((f` x) .ih (f` y))
23		cc0 5206	. . . . . . . . 9 class 0
24	22, 23	wceq 953	. . . . . . . 8 wff ((f` x) .ih (f` y)) = 0
25		chj 8741	. . . . . . . . . . 11 class vH
26	13, 15, 25	co 3948	. . . . . . . . . 10 class (x vH y)
27	26, 5	cfv 3172	. . . . . . . . 9 class (f` (x vH y))
28		cva 8728	. . . . . . . . . 10 class +h
29	19, 20, 28	co 3948	. . . . . . . . 9 class ((f` x) +h (f` y))
30	27, 29	wceq 953	. . . . . . . 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 1637	. . . . 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 1637	. . . 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 773	. . 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 1456	. 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 953	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 10052

Copyright terms: Public domain