Theorem dmdsl3

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

	Ref	Expression
Assertion	dmdsl3	$$⊢\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(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\wedge C\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C$$

Proof

Step	Hyp	Ref	Expression
1		dmdi	$$⊢\left(\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
2	1	exp32	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B{𝑀}_{\mathscr{H}}^{*}A\to \left(A\subseteq C\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)\right)\right)$$
3	2	3com12	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B{𝑀}_{\mathscr{H}}^{*}A\to \left(A\subseteq C\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)\right)\right)$$
4	3	imp32	$$⊢\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(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
5	4	3adantr3	$$⊢\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(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\wedge C\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
6		chjcom	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}B=B{\vee }_{\mathscr{H}}A$$
7	6	ineq2d	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to C\cap \left(A{\vee }_{\mathscr{H}}B\right)=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
8	7	3adant3	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to C\cap \left(A{\vee }_{\mathscr{H}}B\right)=C\cap \left(B{\vee }_{\mathscr{H}}A\right)$$
9		df-ss	$$⊢C\subseteq A{\vee }_{\mathscr{H}}B\leftrightarrow C\cap \left(A{\vee }_{\mathscr{H}}B\right)=C$$
10	9	biimpi	$$⊢C\subseteq A{\vee }_{\mathscr{H}}B\to C\cap \left(A{\vee }_{\mathscr{H}}B\right)=C$$
11	8 10	sylan9req	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge C\subseteq A{\vee }_{\mathscr{H}}B\right)\to C\cap \left(B{\vee }_{\mathscr{H}}A\right)=C$$
12	11	3ad2antr3	$$⊢\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(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\wedge C\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to C\cap \left(B{\vee }_{\mathscr{H}}A\right)=C$$
13	5 12	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(B{𝑀}_{\mathscr{H}}^{*}A\wedge A\subseteq C\wedge C\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\to \left(C\cap B\right){\vee }_{\mathscr{H}}A=C$$