Theorem pjssumi

Description: The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjco.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjssumi	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{+}_{\mathscr{H}}H\right)={\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjco.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjco.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	1 2	pjscji	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{\vee }_{\mathscr{H}}H\right)={\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)$$
6	4 5	eqtrd	$$⊢G\subseteq \perp \left(H\right)\to {\mathrm{proj}}_{ℎ}\left(G{+}_{\mathscr{H}}H\right)={\mathrm{proj}}_{ℎ}\left(G\right){+}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)$$