Theorem pjspansnt 9500

Description: A projection on the span of a singleton.

Assertion

Ref	Expression
pjspansnt	|- ((A e. H~ /\ B e. H~ /\ A =/= 0h) -> ((proj` (span` {A}))` B) = (((B .ih A) / ((normh` A)^2)) .h A))

Proof of Theorem pjspansnt

Step	Hyp	Ref	Expression
1		pjvalt 9239	. . . 4 |- (((span` {A}) e. CH /\ B e. H~) -> ((proj` (span` {A}))` B) = U.{x e. (span` {A}) | E.y e. (_|_` (span` {A}))B = (x +h y)})
2		spansncht 9483	. . . 4 |- (A e. H~ -> (span` {A}) e. CH)
3	1, 2	sylan 448	. . 3 |- ((A e. H~ /\ B e. H~) -> ((proj` (span` {A}))` B) = U.{x e. (span` {A}) | E.y e. (_|_` (span` {A}))B = (x +h y)})
4	3	3adant3 799	. 2 |- ((A e. H~ /\ B e. H~ /\ A =/= 0h) -> ((proj` (span` {A}))` B) = U.{x e. (span` {A}) | E.y e. (_|_` (span` {A}))B = (x +h y)})
5		opreq1 3968	. . . . . . . . . . . . . 14 |- (B = (x +h y) -> (B .ih A) = ((x +h y) .ih A))
6	5	ad2antll 407	. . . . . . . . . . . . 13 |- (((A e. H~ /\ x e. (span` {A})) /\ (y e. (_|_` (span` {A})) /\ B = (x +h y))) -> (B .ih A) = ((x +h y) .ih A))
7		chelt 9100	. . . . . . . . . . . . . . . . . . 19 |- (((_|_` (span` {A})) e. CH /\ y e. (_|_` (span` {A}))) -> y e. H~)
8		chocclt 9184	. . . . . . . . . . . . . . . . . . . 20 |- ((span` {A}) e. CH -> (_|_` (span` {A})) e. CH)
9	2, 8	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (A e. H~ -> (_|_` (span` {A})) e. CH)
10	7, 9	sylan 448	. . . . . . . . . . . . . . . . . 18 |- ((A e. H~ /\ y e. (_|_` (span` {A}))) -> y e. H~)
11	10	adantlr 393	. . . . . . . . . . . . . . . . 17 |- (((A e. H~ /\ x e. H~) /\ y e. (_|_` (span` {A}))) -> y e. H~)
12		ax-his2 8950	. . . . . . . . . . . . . . . . . . 19 |- ((x e. H~ /\ y e. H~ /\ A e. H~) -> ((x +h y) .ih A) = ((x .ih A) + (y .ih A)))
13	12	3comr 841	. . . . . . . . . . . . . . . . . 18 |- ((A e. H~ /\ x e. H~ /\ y e. H~) -> ((x +h y) .ih A) = ((x .ih A) + (y .ih A)))
14	13	3expa 833	. . . . . . . . . . . . . . . . 17 |- (((A e. H~ /\ x e. H~) /\ y e. H~) -> ((x +h y) .ih A) = ((x .ih A) + (y .ih A)))
15	11, 14	syldan 467	. . . . . . . . . . . . . . . 16 |- (((A e. H~ /\ x e. H~) /\ y e. (_|_` (span` {A}))) -> ((x +h y) .ih A) = ((x .ih A) + (y .ih A)))
16		shocorth 9165	. . . . . . . . . . . . . . . . . . . . 21 |- ((span` {A}) e. SH -> ((A e. (span` {A}) /\ y e. (_|_` (span` {A}))) -> (A .ih y) = 0))
17	16	3impib 831	. . . . . . . . . . . . . . . . . . . 20 |- (((span` {A}) e. SH /\ A e. (span` {A}) /\ y e. (_|_` (span` {A}))) -> (A .ih y) = 0)
18		spansnsht 9484	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. H~ -> (span` {A}) e. SH)
19	18	adantr 389	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. H~ /\ y e. (_|_` (span` {A}))) -> (span` {A}) e. SH)
20		spansnid 9486	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. H~ -> A e. (span` {A}))
21	20	adantr 389	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. H~ /\ y e. (_|_` (span` {A}))) -> A e. (span` {A}))
22		pm3.27 323	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. H~ /\ y e. (_|_` (span` {A}))) -> y e. (_|_` (span` {A})))
23	17, 19, 21, 22	syl3anc 858	. . . . . . . . . . . . . . . . . . 19 |- ((A e. H~ /\ y e. (_|_` (span` {A}))) -> (A .ih y) = 0)
24		orthcom 8974	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. H~ /\ y e. H~) -> ((A .ih y) = 0 <-> (y .ih A) = 0))
25	10, 24	syldan 467	. . . . . . . . . . . . . . . . . . 19 |- ((A e. H~ /\ y e. (_|_` (span` {A}))) -> ((A .ih y) = 0 <-> (y .ih A) = 0))
26	23, 25	mpbid 195	. . . . . . . . . . . . . . . . . 18 |- ((A e. H~ /\ y e. (_|_` (span` {A}))) -> (y .ih A) = 0)
27	26	adantlr 393	. . . . . . . . . . . . . . . . 17 |- (((A e. H~ /\ x e. H~) /\ y e. (_|_` (span` {A}))) -> (y .ih A) = 0)
28	27	opreq2d 3976	. . . . . . . . . . . . . . . 16 |- (((A e. H~ /\ x e. H~) /\ y e. (_|_` (span` {A}))) -> ((x .ih A) + (y .ih A)) = ((x .ih A) + 0))
29		hiclt 8947	. . . . . . . . . . . . . . . . . . 19 |- ((x e. H~ /\ A e. H~) -> (x .ih A) e. CC)
30	29	ancoms 436	. . . . . . . . . . . . . . . . . 18 |- ((A e. H~ /\ x e. H~) -> (x .ih A) e. CC)
31		ax0id 5281	. . . . . . . . . . . . . . . . . 18 |- ((x .ih A) e. CC -> ((x .ih A) + 0) = (x .ih A))
32	30, 31	syl 10	. . . . . . . . . . . . . . . . 17 |- ((A e. H~ /\ x e. H~) -> ((x .ih A) + 0) = (x .ih A))
33	32	adantr 389	. . . . . . . . . . . . . . . 16 |- (((A e. H~ /\ x e. H~) /\ y e. (_|_` (span` {A}))) -> ((x .ih A) + 0) = (x .ih A))
34	15, 28, 33	3eqtrd 1511	. . . . . . . . . . . . . . 15 |- (((A e. H~ /\ x e. H~) /\ y e. (_|_` (span` {A}))) -> ((x +h y) .ih A) = (x .ih A))
35		pm3.26 319	. . . . . . . . . . . . . . . 16 |- ((A e. H~ /\ x e. (span` {A})) -> A e. H~)
36		elspansnclt 9488	. . . . . . . . . . . . . . . 16 |- ((A e. H~ /\ x e. (span` {A})) -> x e. H~)
37	35, 36	jca 288	. . . . . . . . . . . . . . 15 |- ((A e. H~ /\ x e. (span` {A})) -> (A e. H~ /\ x e. H~))
38	34, 37	sylan 448	. . . . . . . . . . . . . 14 |- (((A e. H~ /\ x e. (span` {A})) /\ y e. (_|_` (span` {A}))) -> ((x +h y) .ih A) = (x .ih A))
39	38	adantrr 395	. . . . . . . . . . . . 13 |- (((A e. H~ /\ x e. (span` {A})) /\ (y e. (_|_` (span` {A})) /\ B = (x +h y))) -> ((x +h y) .ih A) = (x .ih A))
40	6, 39	eqtrd 1507	. . . . . . . . . . . 12 |- (((A e. H~ /\ x e. (span` {A})) /\ (y e. (_|_` (span` {A})) /\ B = (x +h y))) -> (B .ih A) = (x .ih A))
41	40	adantllr 397	. . . . . . . . . . 11 |- ((((A e. H~ /\ A =/= 0h) /\ x e. (span` {A})) /\ (y e. (_|_` (span` {A})) /\ B = (x +h y))) -> (B .ih A) = (x .ih A))
42	41	opreq1d 3975	. . . . . . . . . 10 |- ((((A e. H~ /\ A =/= 0h) /\ x e. (span` {A})) /\ (y e. (_|_` (span` {A})) /\ B = (x +h y))) -> ((B .ih A) / ((normh` A)^2)) = ((x .ih A) / ((normh` A)^2)))
43	42	opreq1d 3975	. . . . . . . . 9 |- ((((A e. H~ /\ A =/= 0h) /\ x e. (span` {A})) /\ (y e. (_|_` (span` {A})) /\ B = (x +h y))) -> (((B .ih A) / ((normh` A)^2)) .h A) = (((x .ih A) / ((normh` A)^2)) .h A))
44		normcant 9499	. . . . . . . . . . 11 |- ((A e. H~ /\ A =/= 0h /\ x e. (span` {A})) -> (((x .ih A) / ((normh` A)^2)) .h A) = x)
45	44	3expa 833	. . . . . . . . . 10 |- (((A e. H~ /\ A =/= 0h) /\ x e. (span` {A})) -> (((x .ih A) / ((normh` A)^2)) .h A) = x)
46	45	adantr 389	. . . . . . . . 9 |- ((((A e. H~ /\ A =/= 0h) /\ x e. (span` {A})) /\ (y e. (_|_` (span` {A})) /\ B = (x +h y))) -> (((x .ih A) / ((normh` A)^2)) .h A) = x)
47	43, 46	eqtr2d 1508	. . . . . . . 8 |- ((((A e. H~ /\ A =/= 0h) /\ x e. (span` {A})) /\ (y e. (_|_` (span` {A})) /\ B = (x +h y))) -> x = (((B .ih A) / ((normh` A)^2)) .h A))
48	47	exp32 377	. . . . . . 7 |- (((A e. H~ /\ A =/= 0h) /\ x e. (span` {A})) -> (y e. (_|_` (