Theorem chjo

Description: The join of a closed subspace and its orthocomplement is all of Hilbert space. (Contributed by NM, 31-Oct-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	chjo	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}\perp \left(A\right)=\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)$$
2		fveq2	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \perp \left(A\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)$$
3	1 2	oveq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A{\vee }_{\mathscr{H}}\perp \left(A\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)$$
4	3	eqeq1d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(A{\vee }_{\mathscr{H}}\perp \left(A\right)=\mathscr{H}\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)=\mathscr{H}\right)$$
5		ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
6	5	chjoi	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)=\mathscr{H}$$
7	4 6	dedth	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}\perp \left(A\right)=\mathscr{H}$$