# 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 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to {A}{𝑀}_{ℋ}{B}$

### Proof

Step Hyp Ref Expression
1 cvp ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({A}\cap {B}={0}_{ℋ}↔{A}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\right)$
2 atelch ${⊢}{B}\in \mathrm{HAtoms}\to {B}\in {\mathbf{C}}_{ℋ}$
3 cvexch ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\cap {B}\right){⋖}_{ℋ}{B}↔{A}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\right)$
4 cvmd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\cap {B}\right){⋖}_{ℋ}{B}\right)\to {A}{𝑀}_{ℋ}{B}$
5 4 3expia ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\cap {B}\right){⋖}_{ℋ}{B}\to {A}{𝑀}_{ℋ}{B}\right)$
6 3 5 sylbird ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\to {A}{𝑀}_{ℋ}{B}\right)$
7 2 6 sylan2 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({A}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\to {A}{𝑀}_{ℋ}{B}\right)$
8 1 7 sylbid ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({A}\cap {B}={0}_{ℋ}\to {A}{𝑀}_{ℋ}{B}\right)$
9 atnssm0 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left(¬{B}\subseteq {A}↔{A}\cap {B}={0}_{ℋ}\right)$
10 9 con1bid ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left(¬{A}\cap {B}={0}_{ℋ}↔{B}\subseteq {A}\right)$
11 ssmd2 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\wedge {B}\subseteq {A}\right)\to {A}{𝑀}_{ℋ}{B}$
12 11 3com12 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {B}\subseteq {A}\right)\to {A}{𝑀}_{ℋ}{B}$
13 2 12 syl3an2 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\wedge {B}\subseteq {A}\right)\to {A}{𝑀}_{ℋ}{B}$
14 13 3expia ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({B}\subseteq {A}\to {A}{𝑀}_{ℋ}{B}\right)$
15 10 14 sylbid ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left(¬{A}\cap {B}={0}_{ℋ}\to {A}{𝑀}_{ℋ}{B}\right)$
16 8 15 pm2.61d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to {A}{𝑀}_{ℋ}{B}$