Metamath Proof Explorer

Theorem ishlat1

Description: The predicate "is a Hilbert lattice", which is: is orthomodular ( K e. OML ), complete ( K e. CLat ), atomic and satisfies the exchange (or covering) property ( K e. CvLat ), satisfies the superposition principle, and has a minimum height of 4 (witnessed here by 0, x, y, z, 1). (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses ishlat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ishlat.l ⊢ ≤ = ( le ‘ 𝐾 )
ishlat.s ⊢ < = ( lt ‘ 𝐾 )
ishlat.j ⊢ ∨ = ( join ‘ 𝐾 )
ishlat.z ⊢ 0 = ( 0. ‘ 𝐾 )
ishlat.u ⊢ 1 = ( 1. ‘ 𝐾 )
ishlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion ishlat1 ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ishlat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ishlat.l ⊢ ≤ = ( le ‘ 𝐾 )
3 ishlat.s ⊢ < = ( lt ‘ 𝐾 )
4 ishlat.j ⊢ ∨ = ( join ‘ 𝐾 )
5 ishlat.z ⊢ 0 = ( 0. ‘ 𝐾 )
6 ishlat.u ⊢ 1 = ( 1. ‘ 𝐾 )
7 ishlat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
8 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
9 8 7 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
10 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
11 10 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
12 11 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ↔ 𝑧 ≤ ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ) )
13 fveq2 ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ( join ‘ 𝐾 ) )
14 13 4 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ∨ )
15 14 oveqd ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) = ( 𝑥 ∨ 𝑦 ) )
16 15 breq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑧 ≤ ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ↔ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) )
17 12 16 bitrd ⊢ ( 𝑘 = 𝐾 → ( 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ↔ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) )
18 17 3anbi3d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ) ↔ ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) )
19 9 18 rexeqbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑧 ∈ ( Atoms ‘ 𝑘 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ) ↔ ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) )
20 19 imbi2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝑘 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ) ) ↔ ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ) )
21 9 20 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑦 ∈ ( Atoms ‘ 𝑘 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝑘 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ) )
22 9 21 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑦 ∈ ( Atoms ‘ 𝑘 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝑘 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ) )
23 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
24 23 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
25 fveq2 ⊢ ( 𝑘 = 𝐾 → ( lt ‘ 𝑘 ) = ( lt ‘ 𝐾 ) )
26 25 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( lt ‘ 𝑘 ) = < )
27 26 breqd ⊢ ( 𝑘 = 𝐾 → ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ↔ ( 0. ‘ 𝑘 ) < 𝑥 ) )
28 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 0. ‘ 𝑘 ) = ( 0. ‘ 𝐾 ) )
29 28 5 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( 0. ‘ 𝑘 ) = 0 )
30 29 breq1d ⊢ ( 𝑘 = 𝐾 → ( ( 0. ‘ 𝑘 ) < 𝑥 ↔ 0 < 𝑥 ) )
31 27 30 bitrd ⊢ ( 𝑘 = 𝐾 → ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ↔ 0 < 𝑥 ) )
32 26 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ( lt ‘ 𝑘 ) 𝑦 ↔ 𝑥 < 𝑦 ) )
33 31 32 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝑘 ) 𝑦 ) ↔ ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ) )
34 26 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑦 ( lt ‘ 𝑘 ) 𝑧 ↔ 𝑦 < 𝑧 ) )
35 26 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ↔ 𝑧 < ( 1. ‘ 𝑘 ) ) )
36 fveq2 ⊢ ( 𝑘 = 𝐾 → ( 1. ‘ 𝑘 ) = ( 1. ‘ 𝐾 ) )
37 36 6 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( 1. ‘ 𝑘 ) = 1 )
38 37 breq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑧 < ( 1. ‘ 𝑘 ) ↔ 𝑧 < 1 ) )
39 35 38 bitrd ⊢ ( 𝑘 = 𝐾 → ( 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ↔ 𝑧 < 1 ) )
40 34 39 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑦 ( lt ‘ 𝑘 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ) ↔ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) )
41 33 40 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝑘 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝑘 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ) ) ↔ ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) )
42 24 41 rexeqbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑧 ∈ ( Base ‘ 𝑘 ) ( ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝑘 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝑘 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ) ) ↔ ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) )
43 24 42 rexeqbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑦 ∈ ( Base ‘ 𝑘 ) ∃ 𝑧 ∈ ( Base ‘ 𝑘 ) ( ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝑘 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝑘 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ) ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) )
44 24 43 rexeqbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑘 ) ∃ 𝑦 ∈ ( Base ‘ 𝑘 ) ∃ 𝑧 ∈ ( Base ‘ 𝑘 ) ( ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝑘 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝑘 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ) ) ↔ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) )
45 22 44 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( ∀ 𝑥 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑦 ∈ ( Atoms ‘ 𝑘 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝑘 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑘 ) ∃ 𝑦 ∈ ( Base ‘ 𝑘 ) ∃ 𝑧 ∈ ( Base ‘ 𝑘 ) ( ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝑘 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝑘 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
46 df-hlat ⊢ HL = { 𝑘 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ∣ ( ∀ 𝑥 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑦 ∈ ( Atoms ‘ 𝑘 ) ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ ( Atoms ‘ 𝑘 ) ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ( le ‘ 𝑘 ) ( 𝑥 ( join ‘ 𝑘 ) 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝑘 ) ∃ 𝑦 ∈ ( Base ‘ 𝑘 ) ∃ 𝑧 ∈ ( Base ‘ 𝑘 ) ( ( ( 0. ‘ 𝑘 ) ( lt ‘ 𝑘 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝑘 ) 𝑦 ) ∧ ( 𝑦 ( lt ‘ 𝑘 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑘 ) ( 1. ‘ 𝑘 ) ) ) ) }
47 45 46 elrab2 ⊢ ( 𝐾 ∈ HL ↔ ( 𝐾 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
48 elin ⊢ ( 𝐾 ∈ ( OML ∩ CLat ) ↔ ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ) )
49 48 anbi1i ⊢ ( ( 𝐾 ∈ ( OML ∩ CLat ) ∧ 𝐾 ∈ CvLat ) ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ) ∧ 𝐾 ∈ CvLat ) )
50 elin ⊢ ( 𝐾 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ↔ ( 𝐾 ∈ ( OML ∩ CLat ) ∧ 𝐾 ∈ CvLat ) )
51 df-3an ⊢ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ) ∧ 𝐾 ∈ CvLat ) )
52 49 50 51 3bitr4ri ⊢ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ↔ 𝐾 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) )
53 52 anbi1i ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) ↔ ( 𝐾 ∈ ( ( OML ∩ CLat ) ∩ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )
54 47 53 bitr4i ⊢ ( 𝐾 ∈ HL ↔ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ ( 𝑥 ∨ 𝑦 ) ) ) ∧ ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐵 ( ( 0 < 𝑥 ∧ 𝑥 < 𝑦 ) ∧ ( 𝑦 < 𝑧 ∧ 𝑧 < 1 ) ) ) ) )