Theorem pjoi0

Description: The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	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$$

Proof

Step	Hyp	Ref	Expression
1		pjrn	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)=G$$
2	1	adantr	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\right)\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)=G$$
3		pjrn	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)=H$$
4	3	fveq2d	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)=\perp \left(H\right)$$
5	4	adantl	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\right)\to \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)=\perp \left(H\right)$$
6	2 5	sseq12d	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\leftrightarrow G\subseteq \perp \left(H\right)\right)$$
7	6	biimpar	$$⊢\left(\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge G\subseteq \perp \left(H\right)\right)\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
8	7	3adantl3	$$⊢\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{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
9		id	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to H\in {\mathbf{C}}_{\mathscr{H}}$$
10	3 9	eqeltrd	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
11		chsh	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\in {\mathbf{C}}_{\mathscr{H}}\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\in {\mathbf{S}}_{\mathscr{H}}$$
12	10 11	syl	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\in {\mathbf{S}}_{\mathscr{H}}$$
13	12	3ad2ant2	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\in {\mathbf{S}}_{\mathscr{H}}$$
14	13	adantr	$$⊢\left(\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\wedge \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\in {\mathbf{S}}_{\mathscr{H}}$$
15		simpr	$$⊢\left(\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\wedge \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\to \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
16		pjfn	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(G\right)Fn\mathscr{H}$$
17		fnfvelrn	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)Fn\mathscr{H}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)$$
18	16 17	sylan	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)$$
19	18	3adant2	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)$$
20		pjfn	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)Fn\mathscr{H}$$
21		fnfvelrn	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)Fn\mathscr{H}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)$$
22	20 21	sylan	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)$$
23	22	3adant1	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)$$
24	19 23	jca	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
25	24	adantr	$$⊢\left(\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\wedge \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
26		shorth	$$⊢\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\in {\mathbf{S}}_{\mathscr{H}}\to \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\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\right)\right)$$
27	14 15 25 26	syl3c	$$⊢\left(\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\wedge \mathrm{ran}{\mathrm{proj}}_{ℎ}\left(G\right)\subseteq \perp \left(\mathrm{ran}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)=0$$
28	8 27	syldan	$$⊢\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$$