Theorem pjpj0 5259

Description: Decomposition of a vector into projections.

Hypotheses

Ref	Expression
pjcli.1	|- H e. CH
pjcli.2	|- A e. H~

Assertion

Ref	Expression
pjpj0	|- A = (((Proj` H)` A) +v ((Proj` (_|_` H))` A))

Proof of Theorem pjpj0

Step	Hyp	Ref	Expression
1		pjcli.1	. . . . . . . . 9 |- H e. CH
2	1	chocl 5192	. . . . . . . 8 |- (_|_` H) e. CH
3		pjcli.2	. . . . . . . 8 |- A e. H~
4		pjvalt 5246	. . . . . . . 8 |- (((_|_` H) e. CH /\ A e. H~) -> ((Proj` (_|_` H))` A) = U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +v x)})
5	2, 3, 4	mp2an 520	. . . . . . 7 |- ((Proj` (_|_` H))` A) = U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +v x)}
6	5	cleqcomi 1105	. . . . . 6 |- U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +v x)} = ((Proj` (_|_` H))` A)
7	2, 3	pjcli 5257	. . . . . . 7 |- ((Proj` (_|_` H))` A) e. (_|_` H)
8	2	pjthu 5241	. . . . . . . 8 |- (A e. H~ -> E!y e. (_|_` H)E.x e. (_|_` (_|_` H))A = (y +v x))
9	3, 8	ax-mp 6	. . . . . . 7 |- E!y e. (_|_` H)E.x e. (_|_` (_|_` H))A = (y +v x)
10		opreq1 3006	. . . . . . . . . 10 |- (y = ((Proj` (_|_` H))` A) -> (y +v x) = (((Proj` (_|_` H))` A) +v x))
11	10	cleq2d 1112	. . . . . . . . 9 |- (y = ((Proj` (_|_` H))` A) -> (A = (y +v x) <-> A = (((Proj` (_|_` H))` A) +v x)))
12	11	birexdv 1220	. . . . . . . 8 |- (y = ((Proj` (_|_` H))` A) -> (E.x e. (_|_` (_|_` H))A = (y +v x) <-> E.x e. (_|_` (_|_` H))A = (((Proj` (_|_` H))` A) +v x)))
13	12	reuuni2 1956	. . . . . . 7 |- ((((Proj` (_|_` H))` A) e. (_|_` H) /\ E!y e. (_|_` H)E.x e. (_|_` (_|_` H))A = (y +v x)) -> (E.x e. (_|_` (_|_` H))A = (((Proj` (_|_` H))` A) +v x) <-> U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +v x)} = ((Proj` (_|_` H))` A)))
14	7, 9, 13	mp2an 520	. . . . . 6 |- (E.x e. (_|_` (_|_` H))A = (((Proj` (_|_` H))` A) +v x) <-> U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +v x)} = ((Proj` (_|_` H))` A))
15	6, 14	mpbir 165	. . . . 5 |- E.x e. (_|_` (_|_` H))A = (((Proj` (_|_` H))` A) +v x)
16	1	ococ 5252	. . . . . . 7 |- (_|_` (_|_` H)) = H
17		rexeq 1325	. . . . . . 7 |- ((_|_` (_|_` H)) = H -> (E.x e. (_|_` (_|_` H))A = (x +v ((Proj` (_|_` H))` A)) <-> E.x e. H A = (x +v ((Proj` (_|_` H))` A))))
18	16, 17	ax-mp 6	. . . . . 6 |- (E.x e. (_|_` (_|_` H))A = (x +v ((Proj` (_|_` H))` A)) <-> E.x e. H A = (x +v ((Proj` (_|_` H))` A)))
19	2	chocl 5192	. . . . . . . . 9 |- (_|_` (_|_` H)) e. CH
20	19	chel 5137	. . . . . . . 8 |- (x e. (_|_` (_|_` H)) -> x e. H~)
21	2, 3	pjhcli 5258	. . . . . . . . . 10 |- ((Proj` (_|_` H))` A) e. H~
22		ax-hvcom 4985	. . . . . . . . . 10 |- ((x e. H~ /\ ((Proj` (_|_` H))` A) e. H~) -> (x +v ((Proj` (_|_` H))` A)) = (((Proj` (_|_` H))` A) +v x))
23	21, 22	mpan2 519	. . . . . . . . 9 |- (x e. H~ -> (x +v ((Proj` (_|_` H))` A)) = (((Proj` (_|_` H))` A) +v x))
24	23	cleq2d 1112	. . . . . . . 8 |- (x e. H~ -> (A = (x +v ((Proj` (_|_` H))` A)) <-> A = (((Proj` (_|_` H))` A) +v x)))
25	20, 24	syl 12	. . . . . . 7 |- (x e. (_|_` (_|_` H)) -> (A = (x +v ((Proj` (_|_` H))` A)) <-> A = (((Proj` (_|_` H))` A) +v x)))
26	25	birexa 1229	. . . . . 6 |- (E.x e. (_|_` (_|_` H))A = (x +v ((Proj` (_|_` H))` A)) <-> E.x e. (_|_` (_|_` H))A = (((Proj` (_|_` H))` A) +v x))
27	18, 26	bitr3 153	. . . . 5 |- (E.x e. H A = (x +v ((Proj` (_|_` H))` A)) <-> E.x e. (_|_` (_|_` H))A = (((Proj` (_|_` H))` A) +v x))
28	15, 27	mpbir 165	. . . 4 |- E.x e. H A = (x +v ((Proj` (_|_` H))` A))
29		pjvalt 5246	. . . . . . 7 |- ((H e. CH /\ A e. H~) -> ((Proj` H)` A) = U.{x e. H | E.y e. (_|_` H)A = (x +v y)})
30	1, 3, 29	mp2an 520	. . . . . 6 |- ((Proj` H)` A) = U.{x e. H | E.y e. (_|_` H)A = (x +v y)}
31	30	cleqcomi 1105	. . . . 5 |- U.{x e. H | E.y e. (_|_` H)A = (x +v y)} = ((Proj` H)` A)
32	1, 3	pjcli 5257	. . . . . 6 |- ((Proj` H)` A) e. H
33	1	pjthu 5241	. . . . . . 7 |- (A e. H~ -> E!x e. H E.y e. (_|_` H)A = (x +v y))
34	3, 33	ax-mp 6	. . . . . 6 |- E!x e. H E.y e. (_|_` H)A = (x +v y)
35		opreq1 3006	. . . . . . . . 9 |- (x = ((Proj` H)` A) -> (x +v y) = (((Proj` H)` A) +v y))
36	35	cleq2d 1112	. . . . . . . 8 |- (x = ((Proj` H)` A) -> (A = (x +v y) <-> A = (((Proj` H)` A) +v y)))
37	36	birexdv 1220	. . . . . . 7 |- (x = ((Proj` H)` A) -> (E.y e. (_|_` H)A = (x +v y) <-> E.y e. (_|_` H)A = (((Proj` H)` A) +v y)))
38	37	reuuni2 1956	. . . . . 6 |- ((((Proj` H)` A) e. H /\ E!x e. H E.y e. (_|_` H)A = (x +v y)) -> (E.y e. (_|_` H)A = (((Proj` H)` A) +v y) <-> U.{x e. H | E.y e. (_|_` H)A = (x +v y)} = ((Proj` H)` A)))
39	32, 34, 38	mp2an 520	. . . . 5 |- (E.y e. (_|_` H)A = (((Proj` H)` A) +v y) <-> U.{x e. H | E.y e. (_|_` H)A = (x +v y)} = ((Proj` H)` A))
40	31, 39	mpbir 165	. . . 4 |- E.y e. (_|_` H)A = (((Proj` H)` A) +v y)
41	28, 40	pm3.2i 234	. . 3 |- (E.x e. H A = (x +v ((Proj` (_|_` H))` A)) /\ E.y e. (_|_` H)A = (((Proj` H)` A) +v y))
42		r2ex 1241	. . . 4 |- (E.x e. H E.y e. (_|_` H)(A = (x +v ((Proj` (_|_` H))` A)) /\ A = (((Proj` H)` A) +v y)) <-> E.xE.y((x e. H /\ y e. (_|_` H)) /\ (A = (x +v ((Proj` (_|_` H))` A)) /\ A = (((Proj` H)` A) +v y))))
43		reeanv 1316	. . . 4 |- (E.x e. H E.y e. (_|_` H)(A = (x +v ((Proj` (_|_` H))` A)) /\ A = (((Proj` H)` A) +v y)) <-> (E.x e. H A = (x +v ((Proj` (_|_` H))` A)) /\ E.y e. (_|_` H)A = (((Proj` H)` A) +v y)))
44	42, 43	bitr3 153	. . 3 |- (E.xE.y((x e. H /\ y e. (_|_` H)) /\ (A = (x +v ((Proj` (_|_` H))` A)) /\ A = (((Proj` H)` A) +v y))) <-> (E.x e. H A = (x +v ((Proj` (_|_` H))` A)) /\ E.y e. (_|_` H)A = (((Proj` H)` A) +v y)))
45	41, 44	mpbir 165	. 2 |- E.xE.y((x e. H /\ y e. (_|_` H)) /\ (A = (x +v ((Proj` (_|_` H))` A