Theorem chocin

Description: Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of Kalmbach p. 65. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)$$
2		fveq2	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \perp \left(A\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\right)$$
3	1 2	ineq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to A\cap \perp \left(A\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\right)$$
4	3	eqeq1d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\to \left(A\cap \perp \left(A\right)=0_{\mathscr{H}}\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)$$
5		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
6	5	elimel	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7	6	chocini	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\cap \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}$$
8	4 7	dedth	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A\cap \perp \left(A\right)=0_{\mathscr{H}}$$