Theorem pjoi0i

Description: The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoi0.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjoi0.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjoi0.3	$$⊢A\in \mathscr{H}$$
Assertion	pjoi0i	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		pjoi0.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjoi0.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjoi0.3	$$⊢A\in \mathscr{H}$$
4	1 2 3	3pm3.2i	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)$$
5		pjoi0	$$⊢\left(\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\wedge G\subseteq \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0$$
6	4 5	mpan	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0$$