# Metamath Proof Explorer

## Theorem atmd

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

Ref Expression
Assertion atmd ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}{𝑀}_{ℋ}{B}$

### Proof

Step Hyp Ref Expression
1 atdmd ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {A}{𝑀}_{ℋ}^{*}{x}$
2 1 ralrimiva ${⊢}{A}\in \mathrm{HAtoms}\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}^{*}{x}$
3 atelch ${⊢}{A}\in \mathrm{HAtoms}\to {A}\in {\mathbf{C}}_{ℋ}$
4 mddmd2 ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}^{*}{x}\right)$
5 3 4 syl ${⊢}{A}\in \mathrm{HAtoms}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}^{*}{x}\right)$
6 2 5 mpbird ${⊢}{A}\in \mathrm{HAtoms}\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}$
7 breq2 ${⊢}{x}={B}\to \left({A}{𝑀}_{ℋ}{x}↔{A}{𝑀}_{ℋ}{B}\right)$
8 7 rspcv ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}\to {A}{𝑀}_{ℋ}{B}\right)$
9 6 8 mpan9 ${⊢}\left({A}\in \mathrm{HAtoms}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}{𝑀}_{ℋ}{B}$