Theorem ishlat1 36490

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 6672	. . . . . 6 ⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾))
2		ishlat.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
3	1, 2	syl6eqr 2876	. . . . 5 ⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴)
4		fveq2 6672	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾))
5		ishlat.l	. . . . . . . . . . . 12 ⊢ ≤ = (le‘𝐾)
6	4, 5	syl6eqr 2876	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ )
7	6	breqd 5079	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦) ↔ 𝑧 ≤ (𝑥(join‘𝑘)𝑦)))
8		fveq2 6672	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾))
9		ishlat.j	. . . . . . . . . . . . 13 ⊢ ∨ = (join‘𝐾)
10	8, 9	syl6eqr 2876	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ )
11	10	oveqd 7175	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐾 → (𝑥(join‘𝑘)𝑦) = (𝑥 ∨ 𝑦))
12	11	breq2d 5080	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (𝑧 ≤ (𝑥(join‘𝑘)𝑦) ↔ 𝑧 ≤ (𝑥 ∨ 𝑦)))
13	7, 12	bitrd 281	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦) ↔ 𝑧 ≤ (𝑥 ∨ 𝑦)))
14	13	3anbi3d 1438	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → ((𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦)) ↔ (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))))
15	3, 14	rexeqbidv 3404	. . . . . . 7 ⊢ (𝑘 = 𝐾 → (∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦)) ↔ ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))))
16	15	imbi2d 343	. . . . . 6 ⊢ (𝑘 = 𝐾 → ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))))
17	3, 16	raleqbidv 3403	. . . . 5 ⊢ (𝑘 = 𝐾 → (∀𝑦 ∈ (Atoms‘𝑘)(𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))))
18	3, 17	raleqbidv 3403	. . . 4 ⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (Atoms‘𝑘)∀𝑦 ∈ (Atoms‘𝑘)(𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)))))
19		fveq2 6672	. . . . . 6 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾))
20		ishlat.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
21	19, 20	syl6eqr 2876	. . . . 5 ⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵)
22		fveq2 6672	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → (lt‘𝑘) = (lt‘𝐾))
23		ishlat.s	. . . . . . . . . . . 12 ⊢ < = (lt‘𝐾)
24	22, 23	syl6eqr 2876	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐾 → (lt‘𝑘) = < )
25	24	breqd 5079	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → ((0.‘𝑘)(lt‘𝑘)𝑥 ↔ (0.‘𝑘) < 𝑥))
26		fveq2 6672	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → (0.‘𝑘) = (0.‘𝐾))
27		ishlat.z	. . . . . . . . . . . 12 ⊢ 0 = (0.‘𝐾)
28	26, 27	syl6eqr 2876	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐾 → (0.‘𝑘) = 0 )
29	28	breq1d 5078	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → ((0.‘𝑘) < 𝑥 ↔ 0 < 𝑥))
30	25, 29	bitrd 281	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → ((0.‘𝑘)(lt‘𝑘)𝑥 ↔ 0 < 𝑥))
31	24	breqd 5079	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (𝑥(lt‘𝑘)𝑦 ↔ 𝑥 < 𝑦))
32	30, 31	anbi12d 632	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ↔ ( 0 < 𝑥 ∧ 𝑥 < 𝑦)))
33	24	breqd 5079	. . . . . . . . 9 ⊢ (𝑘 = 𝐾 → (𝑦(lt‘𝑘)𝑧 ↔ 𝑦 < 𝑧))
34	24	breqd 5079	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (𝑧(lt‘𝑘)(1.‘𝑘) ↔ 𝑧 < (1.‘𝑘)))
35		fveq2 6672	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝐾 → (1.‘𝑘) = (1.‘𝐾))
36		ishlat.u	. . . . . . . . . . . 12 ⊢ 1 = (1.‘𝐾)
37	35, 36	syl6eqr 2876	. . . . . . . . . . 11 ⊢ (𝑘 = 𝐾 → (1.‘𝑘) = 1 )
38	37	breq2d 5080	. . . . . . . . . 10 ⊢ (𝑘 = 𝐾 → (𝑧 < (1.‘𝑘) ↔ 𝑧 < 1 ))
39	34, 38	bitrd 281	. . . . . . . . 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 3404	. . . . . 6 ⊢ (𝑘 = 𝐾 → (∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘))) ↔ ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))
43	21, 42	rexeqbidv 3404	. . . . 5 ⊢ (𝑘 = 𝐾 → (∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘))) ↔ ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))
44	21, 43	rexeqbidv 3404	. . . 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 36489	. . 3 ⊢ HL = {𝑘 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑥 ∈ (Atoms‘𝑘)∀𝑦 ∈ (Atoms‘𝑘)(𝑥 ≠ 𝑦 → ∃𝑧 ∈ (Atoms‘𝑘)(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧(le‘𝑘)(𝑥(join‘𝑘)𝑦))) ∧ ∃𝑥 ∈ (Base‘𝑘)∃𝑦 ∈ (Base‘𝑘)∃𝑧 ∈ (Base‘𝑘)(((0.‘𝑘)(lt‘𝑘)𝑥 ∧ 𝑥(lt‘𝑘)𝑦) ∧ (𝑦(lt‘𝑘)𝑧 ∧ 𝑧(lt‘𝑘)(1.‘𝑘))))}
47	45, 46	elrab2 3685	. 2 ⊢ (𝐾 ∈ HL ↔ (𝐾 ∈ ((OML ∩ CLat) ∩ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
48		elin 4171	. . . . 5 ⊢ (𝐾 ∈ (OML ∩ CLat) ↔ (𝐾 ∈ OML ∧ 𝐾 ∈ CLat))
49	48	anbi1i 625	. . . 4 ⊢ ((𝐾 ∈ (OML ∩ CLat) ∧ 𝐾 ∈ CvLat) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ CvLat))
50		elin 4171	. . . 4 ⊢ (𝐾 ∈ ((OML ∩ CLat) ∩ CvLat) ↔ (𝐾 ∈ (OML ∩ CLat) ∧ 𝐾 ∈ CvLat))
51		df-3an 1085	. . . 4 ⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat) ∧ 𝐾 ∈ CvLat))
52	49, 50, 51	3bitr4ri 306	. . 3 ⊢ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ↔ 𝐾 ∈ ((OML ∩ CLat) ∩ CvLat))
53	52	anbi1i 625	. 2 ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))) ↔ (𝐾 ∈ ((OML ∩ CLat) ∩ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))
54	47, 53	bitr4i 280	1 ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ∀wral 3140  ∃wrex 3141   ∩ cin 3937   class class class wbr 5068  ‘cfv 6357  (class class class)co 7158  Basecbs 16485  lecple 16574  ltcplt 17553  joincjn 17556  0.cp0 17649  1.cp1 17650  CLatccla 17719  OMLcoml 36313  Atomscatm 36401  CvLatclc 36403  HLchlt 36488

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161  df-hlat 36489

This theorem is referenced by:  ishlat2  36491  ishlat3N  36492  hlomcmcv  36494