Theorem ishlat1 39551

Description: The predicate "is a Hilbert lattice", which is: is orthomodular (𝐾 ∈ OML), complete (𝐾 ∈ CLat), atomic and satisfies the exchange (or covering) property (𝐾 ∈ 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.)

Hypotheses

Ref	Expression
ishlat.b	⊢ 𝐵 = (Base‘𝐾)
ishlat.l	⊢ ≤ = (le‘𝐾)
ishlat.s	⊢ < = (lt‘𝐾)
ishlat.j	⊢ ∨ = (join‘𝐾)
ishlat.z	⊢ 0 = (0.‘𝐾)
ishlat.u	⊢ 1 = (1.‘𝐾)
ishlat.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
ishlat1	⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐾,𝑦,𝑧

Allowed substitution hints:   < (𝑥,𝑦,𝑧)   1 (𝑥,𝑦,𝑧)   ∨ (𝑥,𝑦,𝑧)   ≤ (𝑥,𝑦,𝑧)   0 (𝑥,𝑦,𝑧)

Proof of Theorem ishlat1

Dummy variable 𝑘 is distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  ∃wrex 3058   ∩ cin 3898   class class class wbr 5096  ‘cfv 6490  (class class class)co 7356  Basecbs 17134  lecple 17182  ltcplt 18229  joincjn 18232  0.cp0 18342  1.cp1 18343  CLatccla 18419  OMLcoml 39374  Atomscatm 39462  CvLatclc 39464  HLchlt 39549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-hlat 39550

This theorem is referenced by:  ishlat2  39552  ishlat3N  39553  hlomcmcv  39555