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 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → 𝐴 𝑀ℋ 𝐵 )

Proof

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