Theorem mdi

Description: Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		mdbr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}B\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
2	1	biimpd	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}B\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
3		sseq1	$$⊢x=C\to \left(x\subseteq B\leftrightarrow C\subseteq B\right)$$
4		oveq1	$$⊢x=C\to x{\vee }_{\mathscr{H}}A=C{\vee }_{\mathscr{H}}A$$
5	4	ineq1d	$$⊢x=C\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=\left(C{\vee }_{\mathscr{H}}A\right)\cap B$$
6		oveq1	$$⊢x=C\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)=C{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
7	5 6	eqeq12d	$$⊢x=C\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
8	3 7	imbi12d	$$⊢x=C\to \left(\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \left(C\subseteq B\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
9	8	rspcv	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\to \left(C\subseteq B\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
10	2 9	sylan9	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}B\to \left(C\subseteq B\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
11	10	3impa	$$⊢\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{𝑀}_{\mathscr{H}}B\to \left(C\subseteq B\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
12	11	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(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)$$