# Metamath Proof Explorer

## Theorem dmdbr4ati

Description: Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses sumdmdi.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
sumdmdi.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion dmdbr4ati ${⊢}{A}{𝑀}_{ℋ}^{*}{B}↔\forall {x}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}$

### Proof

Step Hyp Ref Expression
1 sumdmdi.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 sumdmdi.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 dmdbr4 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}^{*}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)$
4 1 2 3 mp2an ${⊢}{A}{𝑀}_{ℋ}^{*}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}$
5 atelch ${⊢}{x}\in \mathrm{HAtoms}\to {x}\in {\mathbf{C}}_{ℋ}$
6 5 imim1i ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\to \left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)\to \left({x}\in \mathrm{HAtoms}\to \left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}\right)$
7 6 ralimi2 ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}\to \forall {x}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}$
8 4 7 sylbi ${⊢}{A}{𝑀}_{ℋ}^{*}{B}\to \forall {x}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}$
9 1 2 sumdmdlem2 ${⊢}\forall {x}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}\to {A}{+}_{ℋ}{B}={A}{\vee }_{ℋ}{B}$
10 1 2 sumdmdi ${⊢}{A}{+}_{ℋ}{B}={A}{\vee }_{ℋ}{B}↔{A}{𝑀}_{ℋ}^{*}{B}$
11 9 10 sylib ${⊢}\forall {x}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}\to {A}{𝑀}_{ℋ}^{*}{B}$
12 8 11 impbii ${⊢}{A}{𝑀}_{ℋ}^{*}{B}↔\forall {x}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({x}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{B}\right)\subseteq \left(\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\right){\vee }_{ℋ}{B}$