Theorem sumdmdi

Description: The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of Holland p. 1519. (Contributed by NM, 14-Dec-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sumdmdi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	sumdmdi.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	sumdmdi	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\leftrightarrow A{𝑀}_{\mathscr{H}}^{*}B$$

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		sumdmdi.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	sumdmdii	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\to A{𝑀}_{\mathscr{H}}^{*}B$$
4		dmdbr4	$$⊢\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{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
5	1 2 4	mp2an	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
6		atelch	$$⊢x\in \mathrm{HAtoms}\to x\in {\mathbf{C}}_{\mathscr{H}}$$
7	6	imim1i	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)\to \left(x\in \mathrm{HAtoms}\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
8	7	ralimi2	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
9	5 8	sylbi	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\to \forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
10	1 2	sumdmdlem2	$$⊢\forall x\in \mathrm{HAtoms}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$
11	9 10	syl	$$⊢A{𝑀}_{\mathscr{H}}^{*}B\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$
12	3 11	impbii	$$⊢A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\leftrightarrow A{𝑀}_{\mathscr{H}}^{*}B$$