# Metamath Proof Explorer

## Theorem mdsl3

Description: Sublattice mapping for a modular pair. Part of Theorem 1.3 of MaedaMaeda p. 2. (Contributed by NM, 26-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion mdsl3 ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}{𝑀}_{ℋ}{B}\wedge {A}\cap {B}\subseteq {C}\wedge {C}\subseteq {B}\right)\right)\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}$

### Proof

Step Hyp Ref Expression
1 mdi ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}{𝑀}_{ℋ}{B}\wedge {C}\subseteq {B}\right)\right)\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)$
2 1 3adantr2 ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}{𝑀}_{ℋ}{B}\wedge {A}\cap {B}\subseteq {C}\wedge {C}\subseteq {B}\right)\right)\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)$
3 chincl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {B}\in {\mathbf{C}}_{ℋ}$
4 chlejb2 ${⊢}\left({A}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\cap {B}\subseteq {C}↔{C}{\vee }_{ℋ}\left({A}\cap {B}\right)={C}\right)$
5 3 4 stoic3 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\cap {B}\subseteq {C}↔{C}{\vee }_{ℋ}\left({A}\cap {B}\right)={C}\right)$
6 5 biimpa ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge {A}\cap {B}\subseteq {C}\right)\to {C}{\vee }_{ℋ}\left({A}\cap {B}\right)={C}$
7 6 3ad2antr2 ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}{𝑀}_{ℋ}{B}\wedge {A}\cap {B}\subseteq {C}\wedge {C}\subseteq {B}\right)\right)\to {C}{\vee }_{ℋ}\left({A}\cap {B}\right)={C}$
8 2 7 eqtrd ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}{𝑀}_{ℋ}{B}\wedge {A}\cap {B}\subseteq {C}\wedge {C}\subseteq {B}\right)\right)\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}$