# Metamath Proof Explorer

## Theorem osumi

Description: If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of Kalmbach p. 67. Note that the (countable) Axiom of Choice is used for this proof via pjhth , although "the hard part" of this proof, chscl , requires no choice. (Contributed by NM, 28-Oct-1999) (Revised by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses osum.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
osum.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion osumi ${⊢}{A}\subseteq \perp \left({B}\right)\to {A}{+}_{ℋ}{B}={A}{\vee }_{ℋ}{B}$

### Proof

Step Hyp Ref Expression
1 osum.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 osum.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 1 a1i ${⊢}{A}\subseteq \perp \left({B}\right)\to {A}\in {\mathbf{C}}_{ℋ}$
4 2 a1i ${⊢}{A}\subseteq \perp \left({B}\right)\to {B}\in {\mathbf{C}}_{ℋ}$
5 1 2 chsscon2i ${⊢}{A}\subseteq \perp \left({B}\right)↔{B}\subseteq \perp \left({A}\right)$
6 5 biimpi ${⊢}{A}\subseteq \perp \left({B}\right)\to {B}\subseteq \perp \left({A}\right)$
7 3 4 6 chscl ${⊢}{A}\subseteq \perp \left({B}\right)\to {A}{+}_{ℋ}{B}\in {\mathbf{C}}_{ℋ}$
8 1 chshii ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
9 2 chshii ${⊢}{B}\in {\mathbf{S}}_{ℋ}$
10 8 9 shjshseli ${⊢}{A}{+}_{ℋ}{B}\in {\mathbf{C}}_{ℋ}↔{A}{+}_{ℋ}{B}={A}{\vee }_{ℋ}{B}$
11 7 10 sylib ${⊢}{A}\subseteq \perp \left({B}\right)\to {A}{+}_{ℋ}{B}={A}{\vee }_{ℋ}{B}$