Metamath Proof Explorer


Theorem osum

Description: If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of Kalmbach p. 67. (Contributed by NM, 31-Oct-2005) (New usage is discouraged.)

Ref Expression
Assertion osum A C B C A B A + B = A B

Proof

Step Hyp Ref Expression
1 sseq1 A = if A C A A B if A C A B
2 oveq1 A = if A C A A + B = if A C A + B
3 oveq1 A = if A C A A B = if A C A B
4 2 3 eqeq12d A = if A C A A + B = A B if A C A + B = if A C A B
5 1 4 imbi12d A = if A C A A B A + B = A B if A C A B if A C A + B = if A C A B
6 fveq2 B = if B C B B = if B C B
7 6 sseq2d B = if B C B if A C A B if A C A if B C B
8 oveq2 B = if B C B if A C A + B = if A C A + if B C B
9 oveq2 B = if B C B if A C A B = if A C A if B C B
10 8 9 eqeq12d B = if B C B if A C A + B = if A C A B if A C A + if B C B = if A C A if B C B
11 7 10 imbi12d B = if B C B if A C A B if A C A + B = if A C A B if A C A if B C B if A C A + if B C B = if A C A if B C B
12 ifchhv if A C A C
13 ifchhv if B C B C
14 12 13 osumi if A C A if B C B if A C A + if B C B = if A C A if B C B
15 5 11 14 dedth2h A C B C A B A + B = A B
16 15 3impia A C B C A B A + B = A B