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

### Proof

Step Hyp Ref Expression
1 cvp ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \mathrm{HAtoms}\right)\to \left({B}\cap {A}={0}_{ℋ}↔{B}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{A}\right)\right)$
2 atelch ${⊢}{A}\in \mathrm{HAtoms}\to {A}\in {\mathbf{C}}_{ℋ}$
3 chjcom ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {B}{\vee }_{ℋ}{A}={A}{\vee }_{ℋ}{B}$
4 2 3 sylan2 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \mathrm{HAtoms}\right)\to {B}{\vee }_{ℋ}{A}={A}{\vee }_{ℋ}{B}$
5 4 breq2d ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \mathrm{HAtoms}\right)\to \left({B}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{A}\right)↔{B}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\right)$
6 1 5 bitrd ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \mathrm{HAtoms}\right)\to \left({B}\cap {A}={0}_{ℋ}↔{B}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\right)$
7 6 ancoms ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}\cap {A}={0}_{ℋ}↔{B}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\right)$
8 cvdmd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {B}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\right)\to {A}{𝑀}_{ℋ}^{*}{B}$
9 8 3expia ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\to {A}{𝑀}_{ℋ}^{*}{B}\right)$
10 2 9 sylan ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}{⋖}_{ℋ}\left({A}{\vee }_{ℋ}{B}\right)\to {A}{𝑀}_{ℋ}^{*}{B}\right)$
11 7 10 sylbid ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}\cap {A}={0}_{ℋ}\to {A}{𝑀}_{ℋ}^{*}{B}\right)$
12 atnssm0 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in \mathrm{HAtoms}\right)\to \left(¬{A}\subseteq {B}↔{B}\cap {A}={0}_{ℋ}\right)$
13 12 ancoms ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(¬{A}\subseteq {B}↔{B}\cap {A}={0}_{ℋ}\right)$
14 13 con1bid ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(¬{B}\cap {A}={0}_{ℋ}↔{A}\subseteq {B}\right)$
15 ssdmd1 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq {B}\right)\to {A}{𝑀}_{ℋ}^{*}{B}$
16 15 3expia ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}\to {A}{𝑀}_{ℋ}^{*}{B}\right)$
17 2 16 sylan ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}\to {A}{𝑀}_{ℋ}^{*}{B}\right)$
18 14 17 sylbid ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(¬{B}\cap {A}={0}_{ℋ}\to {A}{𝑀}_{ℋ}^{*}{B}\right)$
19 11 18 pm2.61d ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}{𝑀}_{ℋ}^{*}{B}$