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}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\wedge C\subseteq B\right)\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C$$

Proof

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