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 e. CH
	sumdmdi.2	|- B e. CH
Assertion	sumdmdi	|- ( ( A +H B ) = ( A vH B ) <-> A MH* B )

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	|- A e. CH
2		sumdmdi.2	|- B e. CH
3	1 2	sumdmdii	|- ( ( A +H B ) = ( A vH B ) -> A MH* B )
4		dmdbr4	|- ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
5	1 2 4	mp2an	|- ( A MH* B <-> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )
6		atelch	|- ( x e. HAtoms -> x e. CH )
7	6	imim1i	|- ( ( x e. CH -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) -> ( x e. HAtoms -> ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
8	7	ralimi2	|- ( A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )
9	5 8	sylbi	|- ( A MH* B -> A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) )
10	1 2	sumdmdlem2	|- ( A. x e. HAtoms ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( A +H B ) = ( A vH B ) )
11	9 10	syl	|- ( A MH* B -> ( A +H B ) = ( A vH B ) )
12	3 11	impbii	|- ( ( A +H B ) = ( A vH B ) <-> A MH* B )