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

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

Proof

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