Theorem pjdsi

Description: Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjsumt.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjsumt.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjdsi	$$⊢\left(A\in \left(G{\vee }_{\mathscr{H}}H\right)\wedge G\subseteq \perp \left(H\right)\right)\to A={\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjsumt.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjsumt.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	osumi	$$⊢G\subseteq \perp \left(H\right)\to G{+}_{\mathscr{H}}H=G{\vee }_{\mathscr{H}}H$$
4	3	fveq2d	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{+}_{\mathscr{H}}H\right)={\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)$$
5	4	fveq1d	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{+}_{\mathscr{H}}H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(A\right)$$
6	1 2	chjcli	$$⊢G{\vee }_{\mathscr{H}}H\in {\mathbf{C}}_{\mathscr{H}}$$
7		pjid	$$⊢\left(G{\vee }_{\mathscr{H}}H\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \left(G{\vee }_{\mathscr{H}}H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(A\right)=A$$
8	6 7	mpan	$$⊢A\in \left(G{\vee }_{\mathscr{H}}H\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)\left(A\right)=A$$
9	5 8	sylan9eqr	$$⊢\left(A\in \left(G{\vee }_{\mathscr{H}}H\right)\wedge G\subseteq \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(G{+}_{\mathscr{H}}H\right)\left(A\right)=A$$
10	6	cheli	$$⊢A\in \left(G{\vee }_{\mathscr{H}}H\right)\to A\in \mathscr{H}$$
11	1 2	pjsumi	$$⊢A\in \mathscr{H}\to \left(G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{+}_{\mathscr{H}}H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)$$
12	11	imp	$$⊢\left(A\in \mathscr{H}\wedge G\subseteq \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(G{+}_{\mathscr{H}}H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
13	10 12	sylan	$$⊢\left(A\in \left(G{\vee }_{\mathscr{H}}H\right)\wedge G\subseteq \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(G{+}_{\mathscr{H}}H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$
14	9 13	eqtr3d	$$⊢\left(A\in \left(G{\vee }_{\mathscr{H}}H\right)\wedge G\subseteq \perp \left(H\right)\right)\to A={\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)$$