This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A ∈ S ℋ
shjshs.2 ⊢ B ∈ S ℋ
Assertion shjshseli ⊢ A + ℋ B ∈ C ℋ ↔ A + ℋ B = A ∨ ℋ B

Proof

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