Theorem pjcjt2 9637

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) +h ((proj` G)` A))))

Proof of Theorem pjcjt2

Step	Hyp	Ref	Expression
1		sseq1 2082	. . 3 |- (H = if(H e. CH, H, H~) -> (H (_ (_|_` G) <-> if(H e. CH, H, H~) (_ (_|_` G)))
2		opreq1 3968	. . . . . 6 |- (H = if(H e. CH, H, H~) -> (H vH G) = (if(H e. CH, H, H~) vH G))
3	2	fveq2d 3728	. . . . 5 |- (H = if(H e. CH, H, H~) -> (proj` (H vH G)) = (proj` (if(H e. CH, H, H~) vH G)))
4	3	fveq1d 3726	. . . 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 3724	. . . . . 6 |- (H = if(H e. CH, H, H~) -> (proj` H) = (proj` if(H e. CH, H, H~)))
6	5	fveq1d 3726	. . . . 5 |- (H = if(H e. CH, H, H~) -> ((proj` H)` A) = ((proj` if(H e. CH, H, H~))` A))
7	6	opreq1d 3975	. . . 4 |- (H = if(H e. CH, H, H~) -> (((proj` H)` A) +h ((proj` G)` A)) = (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)))
8	4, 7	eqeq12d 1489	. . 3 |- (H = if(H e. CH, H, H~) -> (((proj` (H vH G))` A) = (((proj` H)` A) +h ((proj` G)` A)) <-> ((proj` (if(H e. CH, H, H~) vH G))` A) = (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A))))
9	1, 8	imbi12d 626	. 2 |- (H = if(H e. CH, H, H~) -> ((H (_ (_|_` G) -> ((proj` (H vH G))` A) = (((proj` H)` A) +h ((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) +h ((proj` G)` A)))))
10		fveq2 3724	. . . 4 |- (G = if(G e. CH, G, H~) -> (_|_` G) = (_|_` if(G e. CH, G, H~)))
11	10	sseq2d 2089	. . 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 3969	. . . . . 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 3728	. . . . 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 3726	. . . 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 3724	. . . . . 6 |- (G = if(G e. CH, G, H~) -> (proj` G) = (proj` if(G e. CH, G, H~)))
16	15	fveq1d 3726	. . . . 5 |- (G = if(G e. CH, G, H~) -> ((proj` G)` A) = ((proj` if(G e. CH, G, H~))` A))
17	16	opreq2d 3976	. . . 4 |- (G = if(G e. CH, G, H~) -> (((proj` if(H e. CH, H, H~))` A) +h ((proj` G)` A)) = (((proj` if(H e. CH, H, H~))` A) +h ((proj` if(G e. CH, G, H~))` A)))
18	14, 17	eqeq12d 1489	. . 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) +h ((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) +h ((proj` if(G e. CH, G, H~))` A))))
19	11, 18	imbi12d 626	. 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) +h ((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) +h ((proj` if(G e. CH, G, H~))` A)))))
20		fveq2 3724	. . . 4 |- (A = if(A e. H~, A, 0h) -> ((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, 0h)))
21		fveq2 3724	. . . . 5 |- (A = if(A e. H~, A, 0h) -> ((proj` if(H e. CH, H, H~))` A) = ((proj` if(H e. CH, H, H~))` if(A e. H~, A, 0h)))
22		fveq2 3724	. . . . 5 |- (A = if(A e. H~, A, 0h) -> ((proj` if(G e. CH, G, H~))` A) = ((proj` if(G e. CH, G, H~))` if(A e. H~, A, 0h)))
23	21, 22	opreq12d 3978	. . . 4 |- (A = if(A e. H~, A, 0h) -> (((proj` if(H e. CH, H, H~))` A) +h ((proj` if(G e. CH, G, H~))` A)) = (((proj` if(H e. CH, H, H~))` if(A e. H~, A, 0h)) +h ((proj` if(G e. CH, G, H~))` if(A e. H~, A, 0h))))
24	20, 23	eqeq12d 1489	. . 3 |- (A = if(A e. H~, A, 0h) -> (((proj` (if(H e. CH, H, H~) vH if(G e. CH, G, H~)))` A) = (((proj` if(H e. CH, H, H~))` A) +h ((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, 0h)) = (((proj` if(H e. CH, H, H~))` if(A e. H~, A, 0h)) +h ((proj` if(G e. CH, G, H~))` if(A e. H~, A, 0h)))))
25	24	imbi2d 612	. 2 |- (A = if(A e. H~, A, 0h) -> ((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) +h ((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, 0h)) = (((proj` if(H e. CH, H, H~))` if(A e. H~, A, 0h)) +h ((proj` if(G e. CH, G, H~))` if(A e. H~, A, 0h))))))
26		helch 9116	. . . 4 |- H~ e. CH
27	26	elimel 2394	. . 3 |- if(H e. CH, H, H~) e. CH
28		ax-hv0cl 8873	. . . 4 |- 0h e. H~
29	28	elimel 2394	. . 3 |- if(A e. H~, A, 0h) e. H~
30	26	elimel 2394	. . 3 |- if(G e. CH, G