Theorem mddmd2

Description: Relationship between modular pairs and dual-modular pairs. Lemma 1.2 of MaedaMaeda p. 1. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	mddmd2	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}^{*}x\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢x=y\to \left(A{𝑀}_{\mathscr{H}}x\leftrightarrow A{𝑀}_{\mathscr{H}}y\right)$$
2	1	cbvralvw	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}y$$
3		mdbr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}y\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(x{\vee }_{\mathscr{H}}A\right)\cap y=x{\vee }_{\mathscr{H}}\left(A\cap y\right)\right)\right)$$
4		incom	$$⊢\left(A{\vee }_{\mathscr{H}}x\right)\cap y=y\cap \left(A{\vee }_{\mathscr{H}}x\right)$$
5		chjcom	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}x=x{\vee }_{\mathscr{H}}A$$
6	5	ineq1d	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{\vee }_{\mathscr{H}}x\right)\cap y=\left(x{\vee }_{\mathscr{H}}A\right)\cap y$$
7	4 6	syl5reqr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap y=y\cap \left(A{\vee }_{\mathscr{H}}x\right)$$
8	7	adantlr	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap y=y\cap \left(A{\vee }_{\mathscr{H}}x\right)$$
9		incom	$$⊢A\cap y=y\cap A$$
10	9	oveq1i	$$⊢\left(A\cap y\right){\vee }_{\mathscr{H}}x=\left(y\cap A\right){\vee }_{\mathscr{H}}x$$
11		chincl	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\cap y\in {\mathbf{C}}_{\mathscr{H}}$$
12		chjcom	$$⊢\left(A\cap y\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\cap y\right){\vee }_{\mathscr{H}}x=x{\vee }_{\mathscr{H}}\left(A\cap y\right)$$
13	11 12	sylan	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\cap y\right){\vee }_{\mathscr{H}}x=x{\vee }_{\mathscr{H}}\left(A\cap y\right)$$
14	10 13	syl5reqr	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}\left(A\cap y\right)=\left(y\cap A\right){\vee }_{\mathscr{H}}x$$
15	8 14	eqeq12d	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap y=x{\vee }_{\mathscr{H}}\left(A\cap y\right)\leftrightarrow y\cap \left(A{\vee }_{\mathscr{H}}x\right)=\left(y\cap A\right){\vee }_{\mathscr{H}}x\right)$$
16		eqcom	$$⊢y\cap \left(A{\vee }_{\mathscr{H}}x\right)=\left(y\cap A\right){\vee }_{\mathscr{H}}x\leftrightarrow \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)$$
17	15 16	syl6bb	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap y=x{\vee }_{\mathscr{H}}\left(A\cap y\right)\leftrightarrow \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)$$
18	17	imbi2d	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x\subseteq y\to \left(x{\vee }_{\mathscr{H}}A\right)\cap y=x{\vee }_{\mathscr{H}}\left(A\cap y\right)\right)\leftrightarrow \left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\right)$$
19	18	ralbidva	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(x{\vee }_{\mathscr{H}}A\right)\cap y=x{\vee }_{\mathscr{H}}\left(A\cap y\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\right)$$
20	3 19	bitrd	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}y\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\right)$$
21	20	ralbidva	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}y\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\right)$$
22	2 21	syl5bb	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\right)$$
23		ralcom	$$⊢\forall y\in {\mathbf{C}}_{\mathscr{H}}\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)$$
24	22 23	syl6bb	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\right)$$
25		dmdbr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}^{*}x\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\right)$$
26	25	ralbidva	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}^{*}x\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}x=y\cap \left(A{\vee }_{\mathscr{H}}x\right)\right)\right)$$
27	24 26	bitr4d	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}x\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}A{𝑀}_{\mathscr{H}}^{*}x\right)$$