Theorem mdcompli

Description: A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of MaedaMaeda p. 4. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdcompl.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mdcompl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	mdcompli	$$⊢A{𝑀}_{\mathscr{H}}B\leftrightarrow \left(A\cap \perp \left(A\cap B\right)\right){𝑀}_{\mathscr{H}}\left(B\cap \perp \left(A\cap B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdcompl.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdcompl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	mdoc1i	$$⊢\left(A\cap B\right){𝑀}_{\mathscr{H}}\perp \left(A\cap B\right)$$
5	3	dmdoc2i	$$⊢\perp \left(A\cap B\right){𝑀}_{\mathscr{H}}^{*}\left(A\cap B\right)$$
6		ssid	$$⊢A\cap B\subseteq A\cap B$$
7	1 2	chjcli	$$⊢A{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
8	7	chssii	$$⊢A{\vee }_{\mathscr{H}}B\subseteq \mathscr{H}$$
9	3	chjoi	$$⊢\left(A\cap B\right){\vee }_{\mathscr{H}}\perp \left(A\cap B\right)=\mathscr{H}$$
10	8 9	sseqtrri	$$⊢A{\vee }_{\mathscr{H}}B\subseteq \left(A\cap B\right){\vee }_{\mathscr{H}}\perp \left(A\cap B\right)$$
11	3	choccli	$$⊢\perp \left(A\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
12	3 11 1 2	mdslmd1i	$$⊢\left(\left(\left(A\cap B\right){𝑀}_{\mathscr{H}}\perp \left(A\cap B\right)\wedge \perp \left(A\cap B\right){𝑀}_{\mathscr{H}}^{*}\left(A\cap B\right)\right)\wedge \left(A\cap B\subseteq A\cap B\wedge A{\vee }_{\mathscr{H}}B\subseteq \left(A\cap B\right){\vee }_{\mathscr{H}}\perp \left(A\cap B\right)\right)\right)\to \left(A{𝑀}_{\mathscr{H}}B\leftrightarrow \left(A\cap \perp \left(A\cap B\right)\right){𝑀}_{\mathscr{H}}\left(B\cap \perp \left(A\cap B\right)\right)\right)$$
13	4 5 6 10 12	mp4an	$$⊢A{𝑀}_{\mathscr{H}}B\leftrightarrow \left(A\cap \perp \left(A\cap B\right)\right){𝑀}_{\mathscr{H}}\left(B\cap \perp \left(A\cap B\right)\right)$$