HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-chj 9275
Description: Define Hilbert lattice join. See chjvalt 9322 for its value and chjclt 9329 for its closure law. Note that we define it over all Hilbert space subsets to allow proving more general theorems. Even for general subsets the join belongs to CH; see sshjclt 9327. For an alternate definition see dfchj2 9324.
Assertion
Ref Expression
df-chj |- vH = {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_`
(_|_` (x u. y))))}
Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-chj
StepHypRef Expression
1 chj 8802 . 2 class vH
2 vx . . . . . . 7 set x
32cv 955 . . . . . 6 class x
4 chil 8788 . . . . . 6 class H~
53, 4wss 2047 . . . . 5 wff x (_ H~
6 vy . . . . . . 7 set y
76cv 955 . . . . . 6 class y
87, 4wss 2047 . . . . 5 wff y (_ H~
95, 8wa 223 . . . 4 wff (x (_ H~ /\ y (_ H~)
10 vz . . . . . 6 set z
1110cv 955 . . . . 5 class z
123, 7cun 2045 . . . . . . 7 class (x u. y)
13 cort 8799 . . . . . . 7 class _|_
1412, 13cfv 3182 . . . . . 6 class (_|_`
(x u. y))
1514, 13cfv 3182 . . . . 5 class (_|_`
(_|_` (x u. y)))
1611, 15wceq 956 . . . 4 wff z = (_|_` (_|_` (x u. y)))
179, 16wa 223 . . 3 wff ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_`
(x u. y))))
1817, 2, 6, 10copab2 3964 . 2 class {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_` (_|_` (x u. y))))}
191, 18wceq 956 1 wff vH = {<.<.x, y>., z>. | ((x (_ H~ /\ y (_ H~) /\ z = (_|_`
(_|_` (x u. y))))}
Colors of variables: wff set class
This definition is referenced by:  sshjvalt 9320  dfchj2 9324  dfchj3 9325
Copyright terms: Public domain