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	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\subseteq \perp \left(B\right)\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$

Proof

Step	Hyp	Ref	Expression
1		sseq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(A\subseteq \perp \left(B\right)\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq \perp \left(B\right)\right)$$
2		oveq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A{+}_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}B$$
3		oveq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A{\vee }_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B$$
4	2 3	eqeq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B\right)$$
5	1 4	imbi12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\left(A\subseteq \perp \left(B\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq \perp \left(B\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B\right)\right)$$
6		fveq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \perp \left(B\right)=\perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
7	6	sseq2d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq \perp \left(B\right)\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq \perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\right)$$
8		oveq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
9		oveq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
10	8 9	eqeq12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
11	7 10	imbi12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq \perp \left(B\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq \perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\right)$$
12		ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
13		ifchhv	$$⊢if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
14	12 13	osumi	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq \perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){+}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
15	5 11 14	dedth2h	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq \perp \left(B\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B\right)$$
16	15	3impia	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\subseteq \perp \left(B\right)\right)\to A{+}_{\mathscr{H}}B=A{\vee }_{\mathscr{H}}B$$