Theorem shjshseli

Description: A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of MaedaMaeda p. 136. (Contributed by NM, 30-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	shjshs.1	⊢ 𝐴 ∈ Sℋ
	shjshs.2	⊢ 𝐵 ∈ Sℋ
Assertion	shjshseli	⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ ↔ ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		shjshs.1	⊢ 𝐴 ∈ Sℋ
2		shjshs.2	⊢ 𝐵 ∈ Sℋ
3	1 2	shjshsi	⊢ ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) )
4		ococ	⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ → ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 +ℋ 𝐵 ) ) ) = ( 𝐴 +ℋ 𝐵 ) )
5	3 4	eqtr2id	⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )
6	1 2	shjcli	⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
7		eleq1	⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ ↔ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) )
8	6 7	mpbiri	⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ )
9	5 8	impbii	⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ Cℋ ↔ ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )