Metamath Proof Explorer


Definition df-st

Description: Define the set of states on a Hilbert lattice. Definition of Kalmbach p. 266. (Contributed by NM, 23-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion df-st States = f 0 1 C | f = 1 x C y C x y f x y = f x + f y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cst class States
1 vf setvar f
2 cc0 class 0
3 cicc class .
4 c1 class 1
5 2 4 3 co class 0 1
6 cmap class 𝑚
7 cch class C
8 5 7 6 co class 0 1 C
9 1 cv setvar f
10 chba class
11 10 9 cfv class f
12 11 4 wceq wff f = 1
13 vx setvar x
14 vy setvar y
15 13 cv setvar x
16 cort class
17 14 cv setvar y
18 17 16 cfv class y
19 15 18 wss wff x y
20 chj class
21 15 17 20 co class x y
22 21 9 cfv class f x y
23 15 9 cfv class f x
24 caddc class +
25 17 9 cfv class f y
26 23 25 24 co class f x + f y
27 22 26 wceq wff f x y = f x + f y
28 19 27 wi wff x y f x y = f x + f y
29 28 14 7 wral wff y C x y f x y = f x + f y
30 29 13 7 wral wff x C y C x y f x y = f x + f y
31 12 30 wa wff f = 1 x C y C x y f x y = f x + f y
32 31 1 8 crab class f 0 1 C | f = 1 x C y C x y f x y = f x + f y
33 0 32 wceq wff States = f 0 1 C | f = 1 x C y C x y f x y = f x + f y