Theorem pjpj0 9170

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

Proof of Theorem pjpj0

Step	Hyp	Ref	Expression
1		r2ex 1683	. . . 4 |- (E.x e. H E.y e. (_|_` H)(A = (x +h ((proj` (_|_` H))` A)) /\ A = (((proj` H)` A) +h y)) <-> E.xE.y((x e. H /\ y e. (_|_` H)) /\ (A = (x +h ((proj` (_|_` H))` A)) /\ A = (((proj` H)` A) +h y))))
2		reeanv 1770	. . . 4 |- (E.x e. H E.y e. (_|_` H)(A = (x +h ((proj` (_|_` H))` A)) /\ A = (((proj` H)` A) +h y)) <-> (E.x e. H A = (x +h ((proj` (_|_` H))` A)) /\ E.y e. (_|_` H)A = (((proj` H)` A) +h y)))
3	1, 2	bitr3 175	. . 3 |- (E.xE.y((x e. H /\ y e. (_|_` H)) /\ (A = (x +h ((proj` (_|_` H))` A)) /\ A = (((proj` H)` A) +h y))) <-> (E.x e. H A = (x +h ((proj` (_|_` H))` A)) /\ E.y e. (_|_` H)A = (((proj` H)` A) +h y)))
4		pjcli.1	. . . . . . . 8 |- H e. CH
5	4	choccl 9101	. . . . . . 7 |- (_|_` H) e. CH
6		pjcli.2	. . . . . . 7 |- A e. H~
7		pjvalt 9154	. . . . . . 7 |- (((_|_` H) e. CH /\ A e. H~) -> ((proj` (_|_` H))` A) = U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +h x)})
8	5, 6, 7	mp2an 695	. . . . . 6 |- ((proj` (_|_` H))` A) = U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +h x)}
9	8	eqcomi 1471	. . . . 5 |- U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +h x)} = ((proj` (_|_` H))` A)
10	5, 6	pjcli 9168	. . . . . 6 |- ((proj` (_|_` H))` A) e. (_|_` H)
11	5	pjtheu 9150	. . . . . . 7 |- (A e. H~ -> E!y e. (_|_` H)E.x e. (_|_` (_|_` H))A = (y +h x))
12	6, 11	ax-mp 7	. . . . . 6 |- E!y e. (_|_` H)E.x e. (_|_` (_|_` H))A = (y +h x)
13		opreq1 3953	. . . . . . . . 9 |- (y = ((proj` (_|_` H))` A) -> (y +h x) = (((proj` (_|_` H))` A) +h x))
14	13	eqeq2d 1478	. . . . . . . 8 |- (y = ((proj` (_|_` H))` A) -> (A = (y +h x) <-> A = (((proj` (_|_` H))` A) +h x)))
15	14	rexbidv 1656	. . . . . . 7 |- (y = ((proj` (_|_` H))` A) -> (E.x e. (_|_` (_|_` H))A = (y +h x) <-> E.x e. (_|_` (_|_` H))A = (((proj` (_|_` H))` A) +h x)))
16	15	reuuni2 2874	. . . . . 6 |- ((((proj` (_|_` H))` A) e. (_|_` H) /\ E!y e. (_|_` H)E.x e. (_|_` (_|_` H))A = (y +h x)) -> (E.x e. (_|_` (_|_` H))A = (((proj` (_|_` H))` A) +h x) <-> U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +h x)} = ((proj` (_|_` H))` A)))
17	10, 12, 16	mp2an 695	. . . . 5 |- (E.x e. (_|_` (_|_` H))A = (((proj` (_|_` H))` A) +h x) <-> U.{y e. (_|_` H) | E.x e. (_|_` (_|_` H))A = (y +h x)} = ((proj` (_|_` H))` A))
18	9, 17	mpbir 190	. . . 4 |- E.x e. (_|_` (_|_` H))A = (((proj` (_|_` H))` A) +h x)
19	4	ococ 9162	. . . . . 6 |- (_|_` (_|_` H)) = H
20		rexeq1 1779	. . . . . 6 |- ((_|_` (_|_` H)) = H -> (E.x e. (_|_` (_|_` H))A = (x +h ((proj` (_|_` H))` A)) <-> E.x e. H A = (x +h ((proj` (_|_` H))` A))))
21	19, 20	ax-mp 7	. . . . 5 |- (E.x e. (_|_` (_|_` H))A = (x +h ((proj` (_|_` H))` A)) <-> E.x e. H A = (x +h ((proj` (_|_` H))` A)))
22	5	choccl 9101	. . . . . . . 8 |- (_|_` (_|_` H)) e. CH
23	22	chel 9023	. . . . . . 7 |- (x e. (_|_` (_|_` H)) -> x e. H~)
24	5, 6	pjhcli 9169	. . . . . . . . 9 |- ((proj` (_|_` H))` A) e. H~
25		ax-hvcom 8792	. . . . . . . . 9 |- ((x e. H~ /\ ((proj` (_|_` H))` A) e. H~) -> (x +h ((proj` (_|_` H))` A)) = (((proj` (_|_` H))` A) +h x))
26	24, 25	mpan2 694	. . . . . . . 8 |- (x e. H~ -> (x +h ((proj` (_|_` H))` A)) = (((proj` (_|_` H))` A) +h x))
27	26	eqeq2d 1478	. . . . . . 7 |- (x e. H~ -> (A = (x +h ((proj` (_|_` H))` A)) <-> A = (((proj` (_|_` H))` A) +h x)))
28	23, 27	syl 10	. . . . . 6 |- (x e. (_|_` (_|_` H)) -> (A = (x +h ((proj` (_|_` H))` A)) <-> A = (((proj` (_|_` H))` A) +h x)))
29	28	rexbiia 1666	. . . . 5 |- (E.x e. (_|_` (_|_` H))A = (x +h ((proj` (_|_` H))` A)) <-> E.x e. (_|_` (_|_` H))A = (((proj` (_|_` H))` A) +h x))
30	21, 29	bitr3 175	. . . 4 |- (E.x e. H A = (x +h ((proj` (_|_` H))` A)) <-> E.x e. (_|_` (_|_` H))A = (((proj` (_|_` H))` A) +h x))
31	18, 30	mpbir 190	. . 3 |- E.x e. H A = (x +h ((proj` (_|_` H))` A))
32		pjvalt 9154	. . . . . 6 |- ((H e. CH /\ A e. H~) -> ((proj` H)` A) = U.{x e. H | E.y e. (_|_` H)A = (x +h y)})
33	4, 6, 32	mp2an 695	. . . . 5 |- ((proj` H)` A) = U.{x e. H | E.y e. (_|_` H)A = (x +h y)}
34	33	eqcomi 1471	. . . 4 |- U.{x e. H | E.y e. (_|_` H)A = (x +h y)} = ((proj` H)` A)
35	4, 6	pjcli 9168	. . . . 5 |- ((proj` H)` A) e. H
36	4	pjtheu 9150	. . . . . 6 |- (A e. H~ -> E!x e. H E.y e. (_|_` H)A = (x +h y))
37	6, 36	ax-mp 7	. . . . 5 |- E!x e. H E.y e. (_|_` H)A = (x +h y)
38		opreq1 3953	. . . . . . . 8 |- (x = ((proj` H)` A) -> (x +h y) = (((proj` H)` A) +h y))
39	38	eqeq2d 1478	. . . . . . 7 |- (x = ((proj` H)` A) -> (A = (x +h y) <-> A = (((proj` H)` A) +h y)))
40	39	rexbidv 1656	. . . . . 6 |- (x = ((proj` H)` A) -> (E.y e. (_|_` H)A = (x +h y) <-> E.y e. (_|_` H)A = (((proj` H)` A) +h y)))
41	40	reuuni2 2874	. . . . 5 |- ((((proj` H)` A) e. H /\ E!x e. H E.y e. (_|_` H)A = (x +h y)) -> (E.y e. (_|_` H)A = (((proj` H)` A) +h y) <-> U.{x e. H | E.y e. (_|_` H)A = (x +h y)} = ((proj` H)` A)))
42	35, 37, 41	mp2an 695	. . . 4 |- (E.y e. (_|_` H)A = (((proj` H)` A) +h y) <-> U.{x e. H | E.y e. (_|_` H)A = (x +h y)} = ((proj` H)` A))
43	34, 42	mpbir 190	. . 3 |- E.y e. (_|_` H)A = (((proj` H)` A) +h y)
44	3, 31, 43	mpbir2an 728	. 2 |- E.xE.y((x e. H /\ y e. (_|_` H)) /\ (A = (x +h ((proj` (_|_` H))` A)) /\ A = (((proj` H)` A) +h y)))
45	4	chocuni 9088	. . . . . . 7 |- (((x e. H /\ ((proj` (_|_` H))` A) e. (_|_` H)) /\ (((proj` H)` A) e. H /\ y e. (_|_` H)))