Theorem mdslmd1lem3

Description: Lemma for mdslmd1i . (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslmd.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslmd.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslmd.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslmd.4	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	mdslmd1lem3	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdslmd.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdslmd.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		mdslmd.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		mdslmd.4	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
5		oveq1	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}A=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A$$
6	5	sseq1d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}A\subseteq D\leftrightarrow if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\subseteq D\right)$$
7	5	oveq1d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C=\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C$$
8	7	ineq1d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D=\left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D$$
9	5	oveq1d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)=\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)$$
10	8 9	sseq12d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\leftrightarrow \left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)$$
11	6 10	imbi12d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\leftrightarrow \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\right)$$
12		sseq2	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\leftrightarrow \left(C\cap B\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\right)$$
13		sseq1	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(x\subseteq D\cap B\leftrightarrow if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\subseteq D\cap B\right)$$
14	12 13	anbi12d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\leftrightarrow \left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\wedge if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\subseteq D\cap B\right)\right)$$
15		oveq1	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}\left(C\cap B\right)=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(C\cap B\right)$$
16	15	ineq1d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)=\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)$$
17		oveq1	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)$$
18	16 17	sseq12d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\leftrightarrow \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)$$
19	14 18	imbi12d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\leftrightarrow \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\wedge if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\subseteq D\cap B\right)\to \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
20	11 19	imbi12d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(\left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)\leftrightarrow \left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\wedge if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\subseteq D\cap B\right)\to \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)\right)$$
21	20	imbi2d	$$⊢x=if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\to \left(\left(\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)\right)\leftrightarrow \left(\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\wedge if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\subseteq D\cap B\right)\to \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)\right)\right)$$
22		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
23	22	elimel	$$⊢if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
24	1 2 3 4 23	mdslmd1lem1	$$⊢\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\wedge if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right)\subseteq D\cap B\right)\to \left(if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq if\left(x\in {\mathbf{C}}_{\mathscr{H}},x,0_{\mathscr{H}}\right){\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$
25	21 24	dedth	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)\right)$$
26	25	imp	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(\left(A{𝑀}_{\mathscr{H}}B\wedge B{𝑀}_{\mathscr{H}}^{*}A\right)\wedge \left(\left(A\subseteq C\wedge A\subseteq D\right)\wedge \left(C\subseteq A{\vee }_{\mathscr{H}}B\wedge D\subseteq A{\vee }_{\mathscr{H}}B\right)\right)\right)\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\subseteq D\to \left(\left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}C\right)\cap D\subseteq \left(x{\vee }_{\mathscr{H}}A\right){\vee }_{\mathscr{H}}\left(C\cap D\right)\right)\to \left(\left(\left(C\cap B\right)\cap \left(D\cap B\right)\subseteq x\wedge x\subseteq D\cap B\right)\to \left(x{\vee }_{\mathscr{H}}\left(C\cap B\right)\right)\cap \left(D\cap B\right)\subseteq x{\vee }_{\mathscr{H}}\left(\left(C\cap B\right)\cap \left(D\cap B\right)\right)\right)\right)$$