This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atmd2

Description: Two Hilbert lattice elements have the dual modular pair property if the second is an atom. Part of Exercise 6 of Kalmbach p. 103. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atmd2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A 𝑀 ℋ B

Proof

Step Hyp Ref Expression
1 cvp ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ∩ B = 0 ℋ ↔ A ⋖ ℋ A ∨ ℋ B
2 atelch ⊢ B ∈ HAtoms → B ∈ C ℋ
3 cvexch ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ∩ B ⋖ ℋ B ↔ A ⋖ ℋ A ∨ ℋ B
4 cvmd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ∩ B ⋖ ℋ B → A 𝑀 ℋ B
5 4 3expia ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ∩ B ⋖ ℋ B → A 𝑀 ℋ B
6 3 5 sylbird ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ A ∨ ℋ B → A 𝑀 ℋ B
7 2 6 sylan2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ⋖ ℋ A ∨ ℋ B → A 𝑀 ℋ B
8 1 7 sylbid ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A ∩ B = 0 ℋ → A 𝑀 ℋ B
9 atnssm0 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ B ⊆ A ↔ A ∩ B = 0 ℋ
10 9 con1bid ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ A ∩ B = 0 ℋ ↔ B ⊆ A
11 ssmd2 ⊢ B ∈ C ℋ ∧ A ∈ C ℋ ∧ B ⊆ A → A 𝑀 ℋ B
12 11 3com12 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ B ⊆ A → A 𝑀 ℋ B
13 2 12 syl3an2 ⊢ A ∈ C ℋ ∧ B ∈ HAtoms ∧ B ⊆ A → A 𝑀 ℋ B
14 13 3expia ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → B ⊆ A → A 𝑀 ℋ B
15 10 14 sylbid ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → ¬ A ∩ B = 0 ℋ → A 𝑀 ℋ B
16 8 15 pm2.61d ⊢ A ∈ C ℋ ∧ B ∈ HAtoms → A 𝑀 ℋ B