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	⊢ 𝐴 ∈ Cℋ
	sumdmdi.2	⊢ 𝐵 ∈ Cℋ
Assertion	sumdmdi	⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 𝑀ℋ* 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	⊢ 𝐴 ∈ Cℋ
2		sumdmdi.2	⊢ 𝐵 ∈ Cℋ
3	1 2	sumdmdii	⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 𝑀ℋ* 𝐵 )
4		dmdbr4	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
5	1 2 4	mp2an	⊢ ( 𝐴 𝑀ℋ* 𝐵 ↔ ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
6		atelch	⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
7	6	imim1i	⊢ ( ( 𝑥 ∈ Cℋ → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) → ( 𝑥 ∈ HAtoms → ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) ) )
8	7	ralimi2	⊢ ( ∀ 𝑥 ∈ Cℋ ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
9	5 8	sylbi	⊢ ( 𝐴 𝑀ℋ* 𝐵 → ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) )
10	1 2	sumdmdlem2	⊢ ( ∀ 𝑥 ∈ HAtoms ( ( 𝑥 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ ( ( ( 𝑥 ∨ℋ 𝐵 ) ∩ 𝐴 ) ∨ℋ 𝐵 ) → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )
11	9 10	syl	⊢ ( 𝐴 𝑀ℋ* 𝐵 → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )
12	3 11	impbii	⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ↔ 𝐴 𝑀ℋ* 𝐵 )