Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-dmd Structured version   Unicode version

Definition df-dmd 23776
 Description: Define the dual modular pair relation (on the Hilbert lattice). Definition 1.1 of [MaedaMaeda] p. 1, who use the notation (x,y)M* for "the ordered pair is a dual modular pair." See dmdbr 23794 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-dmd
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-dmd
StepHypRef Expression
1 cdmd 22462 . 2
2 vx . . . . . . 7
32cv 1651 . . . . . 6
4 cch 22424 . . . . . 6
53, 4wcel 1725 . . . . 5
6 vy . . . . . . 7
76cv 1651 . . . . . 6
87, 4wcel 1725 . . . . 5
95, 8wa 359 . . . 4
10 vz . . . . . . . 8
1110cv 1651 . . . . . . 7
127, 11wss 3312 . . . . . 6
1311, 3cin 3311 . . . . . . . 8
14 chj 22428 . . . . . . . 8
1513, 7, 14co 6073 . . . . . . 7
163, 7, 14co 6073 . . . . . . . 8
1711, 16cin 3311 . . . . . . 7
1815, 17wceq 1652 . . . . . 6
1912, 18wi 4 . . . . 5
2019, 10, 4wral 2697 . . . 4
219, 20wa 359 . . 3
2221, 2, 6copab 4257 . 2
231, 22wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  dmdbr  23794
 Copyright terms: Public domain W3C validator