Metamath Proof Explorer

Theorem atdmd

Description: Two Hilbert lattice elements have the dual modular pair property if the first is an atom. Theorem 7.6(c) of MaedaMaeda p. 31. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cvp ⊢ B ∈ C ℋ ∧ A ∈ HAtoms → B ∩ A = 0 ℋ ↔ B ⋖ ℋ B ∨ ℋ A
2 atelch ⊢ A ∈ HAtoms → A ∈ C ℋ
3 chjcom ⊢ B ∈ C ℋ ∧ A ∈ C ℋ → B ∨ ℋ A = A ∨ ℋ B
4 2 3 sylan2 ⊢ B ∈ C ℋ ∧ A ∈ HAtoms → B ∨ ℋ A = A ∨ ℋ B
5 4 breq2d ⊢ B ∈ C ℋ ∧ A ∈ HAtoms → B ⋖ ℋ B ∨ ℋ A ↔ B ⋖ ℋ A ∨ ℋ B
6 1 5 bitrd ⊢ B ∈ C ℋ ∧ A ∈ HAtoms → B ∩ A = 0 ℋ ↔ B ⋖ ℋ A ∨ ℋ B
7 6 ancoms ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → B ∩ A = 0 ℋ ↔ B ⋖ ℋ A ∨ ℋ B
8 cvdmd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ B ⋖ ℋ A ∨ ℋ B → A 𝑀 ℋ * B
9 8 3expia ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → B ⋖ ℋ A ∨ ℋ B → A 𝑀 ℋ * B
10 2 9 sylan ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → B ⋖ ℋ A ∨ ℋ B → A 𝑀 ℋ * B
11 7 10 sylbid ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → B ∩ A = 0 ℋ → A 𝑀 ℋ * B
12 atnssm0 ⊢ B ∈ C ℋ ∧ A ∈ HAtoms → ¬ A ⊆ B ↔ B ∩ A = 0 ℋ
13 12 ancoms ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → ¬ A ⊆ B ↔ B ∩ A = 0 ℋ
14 13 con1bid ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → ¬ B ∩ A = 0 ℋ ↔ A ⊆ B
15 ssdmd1 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → A 𝑀 ℋ * B
16 15 3expia ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊆ B → A 𝑀 ℋ * B
17 2 16 sylan ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → A ⊆ B → A 𝑀 ℋ * B
18 14 17 sylbid ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → ¬ B ∩ A = 0 ℋ → A 𝑀 ℋ * B
19 11 18 pm2.61d ⊢ A ∈ HAtoms ∧ B ∈ C ℋ → A 𝑀 ℋ * B