Theorem pjcjt2 5580

Description: The projection on a subspace join is the sum of the projections.

Assertion

Ref	Expression
pjcjt2	|- ((H e. CH /\ G e. CH /\ A e. H~) -> (H (_ (_|_` G) -> ((Proj` (H vH G))` A) = (((Proj` H)` A) +v ((Proj` G)` A))))

Proof of Theorem pjcjt2

Step	Hyp	Ref	Expression
1		sseq1 1521	. . 3 |- (H = if(H e. CH, H, H~) -> (H (_ (_|_` G) <-> if(H e. CH, H, H~) (_ (_|_` G)))
2		opreq1 3006	. . . . . 6 |- (H = if(H e. CH, H, H~) -> (H vH G) = (if(H e. CH, H, H~) vH G))
3	2	fveq2d 2836	. . . . 5 |- (H = if(H e. CH, H, H~) -> (Proj` (H vH G)) = (Proj` (if(H e. CH, H, H~) vH G)))
4	3	fveq1d 2834	. . . 4 |- (H = if(H e. CH, H, H~) -> ((Proj` (H vH G))` A) = ((Proj` (if(H e. CH, H, H~) vH G))` A))
5		fveq2 2832	. . . . . 6 |- (H = if(H e. CH, H, H~) -> (Proj` H) = (Proj` if(H e. CH, H, H~)))
6	5	fveq1d 2834	. . . . 5 |- (H = if(H e. CH, H, H~) -> ((Proj` H)` A) = ((Proj` if(H e. CH, H, H~))` A))
7	6	opreq1d 3012	. . . 4 |- (H = if(H e. CH, H, H~) -> (((Proj` H)` A) +v ((Proj` G)` A)) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))
8	4, 7	cleq12d 1115	. . 3 |- (H = if(H e. CH, H, H~) -> (((Proj` (H vH G))` A) = (((Proj` H)` A) +v ((Proj` G)` A)) <-> ((Proj` (if(H e. CH, H, H~) vH G))` A) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A))))
9	1, 8	imbi12d 474	. 2 |- (H = if(H e. CH, H, H~) -> ((H (_ (_|_` G) -> ((Proj` (H vH G))` A) = (((Proj` H)` A) +v ((Proj` G)` A))) <-> (if(H e. CH, H, H~) (_ (_|_` G) -> ((Proj` (if(H e. CH, H, H~) vH G))` A) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)))))
10		fveq2 2832	. . . 4 |- (G = if(G e. CH, G, H~) -> (_|_` G) = (_|_` if(G e. CH, G, H~)))
11	10	sseq2d 1528	. . 3 |- (G = if(G e. CH, G, H~) -> (if(H e. CH, H, H~) (_ (_|_` G) <-> if(H e. CH, H, H~) (_ (_|_` if(G e. CH, G, H~))))
12		opreq2 3007	. . . . . 6 |- (G = if(G e. CH, G, H~) -> (if(H e. CH, H, H~) vH G) = (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))
13	12	fveq2d 2836	. . . . 5 |- (G = if(G e. CH, G, H~) -> (Proj` (if(H e. CH, H, H~) vH G)) = (Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~))))
14	13	fveq1d 2834	. . . 4 |- (G = if(G e. CH, G, H~) -> ((Proj` (if(H e. CH, H, H~) vH G))` A) = ((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` A))
15		fveq2 2832	. . . . . 6 |- (G = if(G e. CH, G, H~) -> (Proj` G) = (Proj` if(G e. CH, G, H~)))
16	15	fveq1d 2834	. . . . 5 |- (G = if(G e. CH, G, H~) -> ((Proj` G)` A) = ((Proj` if(G e. CH, G, H~))` A))
17	16	opreq2d 3013	. . . 4 |- (G = if(G e. CH, G, H~) -> (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A)))
18	14, 17	cleq12d 1115	. . 3 |- (G = if(G e. CH, G, H~) -> (((Proj` (if(H e. CH, H, H~) vH G))` A) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A)) <-> ((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` A) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A))))
19	11, 18	imbi12d 474	. 2 |- (G = if(G e. CH, G, H~) -> ((if(H e. CH, H, H~) (_ (_|_` G) -> ((Proj` (if(H e. CH, H, H~) vH G))` A) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` G)` A))) <-> (if(H e. CH, H, H~) (_ (_|_` if(G e. CH, G, H~)) -> ((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` A) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A)))))
20		fveq2 2832	. . . 4 |- (A = if(A e. H~, A, 0v) -> ((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` A) = ((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` if(A e. H~, A, 0v)))
21		fveq2 2832	. . . . 5 |- (A = if(A e. H~, A, 0v) -> ((Proj` if(H e. CH, H, H~))` A) = ((Proj` if(H e. CH, H, H~))` if(A e. H~, A, 0v)))
22		fveq2 2832	. . . . 5 |- (A = if(A e. H~, A, 0v) -> ((Proj` if(G e. CH, G, H~))` A) = ((Proj` if(G e. CH, G, H~))` if(A e. H~, A, 0v)))
23	21, 22	opreq12d 3014	. . . 4 |- (A = if(A e. H~, A, 0v) -> (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A)) = (((Proj` if(H e. CH, H, H~))` if(A e. H~, A, 0v)) +v ((Proj` if(G e. CH, G, H~))` if(A e. H~, A, 0v))))
24	20, 23	cleq12d 1115	. . 3 |- (A = if(A e. H~, A, 0v) -> (((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` A) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A)) <-> ((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` if(A e. H~, A, 0v)) = (((Proj` if(H e. CH, H, H~))` if(A e. H~, A, 0v)) +v ((Proj` if(G e. CH, G, H~))` if(A e. H~, A, 0v)))))
25	24	imbi2d 464	. 2 |- (A = if(A e. H~, A, 0v) -> ((if(H e. CH, H, H~) (_ (_|_` if(G e. CH, G, H~)) -> ((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` A) = (((Proj` if(H e. CH, H, H~))` A) +v ((Proj` if(G e. CH, G, H~))` A))) <-> (if(H e. CH, H, H~) (_ (_|_` if(G e. CH, G, H~)) -> ((Proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` if(A e. H~, A, 0v)) = (((Proj` if(H e. CH, H, H~))` if(A e. H~, A, 0v)) +v ((Proj` if(G e. CH, G, H~))` if(A e. H~, A, 0v))))))
26		helch 5151	. . . 4 |- H~ e. CH
27	26	elimel 1793	. . 3 |- if(H e. CH, H<