Theorem pjcjt2

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

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

Proof

Step	Hyp	Ref	Expression
1		sseq1	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left(H\subseteq \perp \left(G\right)\leftrightarrow if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(G\right)\right)$$
2		fvoveq1	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G\right)$$
3	2	fveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G\right)\left(A\right)$$
4		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)$$
5	4	fveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)$$
6	5	oveq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)$$
7	3 6	eqeq12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$
8	1 7	imbi12d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\to \left(\left(H\subseteq \perp \left(G\right)\to {\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)\leftrightarrow \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(G\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)\right)$$
9		fveq2	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to \perp \left(G\right)=\perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)$$
10	9	sseq2d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(G\right)\leftrightarrow if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\right)$$
11		oveq2	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)$$
12	11	fveq2d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)$$
13	12	fveq1d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)$$
14		fveq2	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)$$
15	14	fveq1d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)$$
16	15	oveq2d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)$$
17	13 16	eqeq12d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)$$
18	10 17	imbi12d	$$⊢G=if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\to \left(\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(G\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)\leftrightarrow \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)\right)$$
19		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
20		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
21		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
22	20 21	oveq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
23	19 22	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)$$
24	23	imbi2d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left(\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(A\right)\right)\leftrightarrow \left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)\right)\right)$$
25		ifchhv	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
26		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
27		ifchhv	$$⊢if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
28	25 26 27	pjcji	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\subseteq \perp \left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\to {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(if\left(G\in {\mathbf{C}}_{\mathscr{H}},G,\mathscr{H}\right)\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
29	8 18 24 28	dedth3h	$$⊢\left(H\in {\mathbf{C}}_{\mathscr{H}}\wedge G\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in \mathscr{H}\right)\to \left(H\subseteq \perp \left(G\right)\to {\mathrm{proj}}_{ℎ}\left(H{\vee }_{\mathscr{H}}G\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\right)$$