Theorem dmdi

Description: Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dmdbr	$$⊢\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(B\subseteq x\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}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(B\subseteq x\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
3		sseq2	$$⊢x=C\to \left(B\subseteq x\leftrightarrow B\subseteq C\right)$$
4		ineq1	$$⊢x=C\to x\cap A=C\cap A$$
5	4	oveq1d	$$⊢x=C\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=\left(C\cap A\right){\vee }_{\mathscr{H}}B$$
6		ineq1	$$⊢x=C\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)=C\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
7	5 6	eqeq12d	$$⊢x=C\to \left(\left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(C\cap A\right){\vee }_{\mathscr{H}}B=C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
8	3 7	imbi12d	$$⊢x=C\to \left(\left(B\subseteq x\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \left(B\subseteq C\to \left(C\cap A\right){\vee }_{\mathscr{H}}B=C\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
9	8	rspcv	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq x\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\to \left(B\subseteq C\to \left(C\cap A\right){\vee }_{\mathscr{H}}B=C\cap \left(A{\vee }_{\mathscr{H}}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(B\subseteq C\to \left(C\cap A\right){\vee }_{\mathscr{H}}B=C\cap \left(A{\vee }_{\mathscr{H}}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(B\subseteq C\to \left(C\cap A\right){\vee }_{\mathscr{H}}B=C\cap \left(A{\vee }_{\mathscr{H}}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 B\subseteq C\right)\right)\to \left(C\cap A\right){\vee }_{\mathscr{H}}B=C\cap \left(A{\vee }_{\mathscr{H}}B\right)$$