Theorem pjthlem8 9141

Description: Lemma for pjth 9148.

Hypotheses

Ref	Expression
pjthlem6.1	|- D e. H~
pjthlem6.2	|- R = (1 / (D .ih D))
pjthlem6.3	|- C e. H~
pjthlem6.4	|- S = (R x. (C .ih D))

Assertion

Ref	Expression
pjthlem8	|- (D =/= 0h -> ((normh` (C -h (S .h D)))^2) = (((normh` C)^2) - (R x. ((abs` (C .ih D))^2))))

Proof of Theorem pjthlem8

Step	Hyp	Ref	Expression
1		pjthlem6.1	. . . 4 |- D e. H~
2		pjthlem6.2	. . . 4 |- R = (1 / (D .ih D))
3		pjthlem6.3	. . . 4 |- C e. H~
4		pjthlem6.4	. . . 4 |- S = (R x. (C .ih D))
5	1, 2, 3, 4	pjthlem4 9137	. . 3 |- (D =/= 0h -> S e. CC)
6		opreq1 3953	. . . . . . . 8 |- (S = if(S e. CC, S, 0) -> (S .h D) = (if(S e. CC, S, 0) .h D))
7	6	opreq2d 3961	. . . . . . 7 |- (S = if(S e. CC, S, 0) -> (C -h (S .h D)) = (C -h (if(S e. CC, S, 0) .h D)))
8	7	fveq2d 3713	. . . . . 6 |- (S = if(S e. CC, S, 0) -> (normh` (C -h (S .h D))) = (normh` (C -h (if(S e. CC, S, 0) .h D))))
9	8	opreq1d 3960	. . . . 5 |- (S = if(S e. CC, S, 0) -> ((normh` (C -h (S .h D)))^2) = ((normh` (C -h (if(S e. CC, S, 0) .h D)))^2))
10		opreq1 3953	. . . . . . . 8 |- (S = if(S e. CC, S, 0) -> (S x. (D .ih C)) = (if(S e. CC, S, 0) x. (D .ih C)))
11	10	fveq2d 3713	. . . . . . 7 |- (S = if(S e. CC, S, 0) -> (*` (S x. (D .ih C))) = (*` (if(S e. CC, S, 0) x. (D .ih C))))
12	11	opreq2d 3961	. . . . . 6 |- (S = if(S e. CC, S, 0) -> (((normh` C)^2) - (*` (S x. (D .ih C)))) = (((normh` C)^2) - (*` (if(S e. CC, S, 0) x. (D .ih C)))))
13		id 59	. . . . . . . . 9 |- (S = if(S e. CC, S, 0) -> S = if(S e. CC, S, 0))
14		fveq2 3709	. . . . . . . . 9 |- (S = if(S e. CC, S, 0) -> (*` S) = (*` if(S e. CC, S, 0)))
15	13, 14	opreq12d 3963	. . . . . . . 8 |- (S = if(S e. CC, S, 0) -> (S x. (*` S)) = (if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))))
16	15	opreq1d 3960	. . . . . . 7 |- (S = if(S e. CC, S, 0) -> ((S x. (*` S)) x. (D .ih D)) = ((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .ih D)))
17	16, 10	opreq12d 3963	. . . . . 6 |- (S = if(S e. CC, S, 0) -> (((S x. (*` S)) x. (D .ih D)) - (S x. (D .ih C))) = (((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .ih D)) - (if(S e. CC, S, 0) x. (D .ih C))))
18	12, 17	opreq12d 3963	. . . . 5 |- (S = if(S e. CC, S, 0) -> ((((normh` C)^2) - (*` (S x. (D .ih C)))) + (((S x. (*` S)) x. (D .ih D)) - (S x. (D .ih C)))) = ((((normh` C)^2) - (*` (if(S e. CC, S, 0) x. (D .ih C)))) + (((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .ih D)) - (if(S e. CC, S, 0) x. (D .ih C)))))
19	9, 18	eqeq12d 1481	. . . 4 |- (S = if(S e. CC, S, 0) -> (((normh` (C -h (S .h D)))^2) = ((((normh` C)^2) - (*` (S x. (D .ih C)))) + (((S x. (*` S)) x. (D .ih D)) - (S x. (D .ih C)))) <-> ((normh` (C -h (if(S e. CC, S, 0) .h D)))^2) = ((((normh` C)^2) - (*` (if(S e. CC, S, 0) x. (D .ih C)))) + (((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .ih D)) - (if(S e. CC, S, 0) x. (D .ih C))))))
20		0cn 5300	. . . . . 6 |- 0 e. CC
21	20	elimel 2384	. . . . 5 |- if(S e. CC, S, 0) e. CC
22	1, 3, 21	pjthlem5 9138	. . . 4 |- ((normh` (C -h (if(S e. CC, S, 0) .h D)))^2) = ((((normh` C)^2) - (*` (if(S e. CC, S, 0) x. (D .ih C)))) + (((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .ih D)) - (if(S e. CC, S, 0) x. (D .ih C))))
23	19, 22	dedth 2373	. . 3 |- (S e. CC -> ((normh` (C -h (S .h D)))^2) = ((((normh` C)^2) - (*` (S x. (D .ih C)))) + (((S x. (*` S)) x. (D .ih D)) - (S x. (D .ih C)))))
24	5, 23	syl 10	. 2 |- (D =/= 0h -> ((normh` (C -h (S .h D)))^2) = ((((normh` C)^2) - (*` (S x. (D .ih C)))) + (((S x. (*` S)) x. (D .ih D)) - (S x. (D .ih C)))))
25	1, 2, 3, 4	pjthlem6 9139	. . . . . 6 |- (D =/= 0h -> (S x. (D .ih C)) = (R x. ((abs` (C .ih D))^2)))
26	25	fveq2d 3713	. . . . 5 |- (D =/= 0h -> (*` (S x. (D .ih C))) = (*` (R x. ((abs` (C .ih D))^2))))
27	1, 2	pjthlem2 9135	. . . . . 6 |- (D =/= 0h -> R e. RR)
28	3, 1	hicl 8869	. . . . . . . . 9 |- (C .ih D) e. CC
29	28	abscl 6774	. . . . . . . 8 |- (abs` (C .ih D)) e. RR
30	29	resqcl 6554	. . . . . . 7 |- ((abs` (C .ih D))^2) e. RR
31		axmulrcl 5246	. . . . . . 7 |- ((R e. RR /\ ((abs` (C .ih D))^2) e. RR) -> (R x. ((abs` (C .ih D))^2)) e. RR)
32	30, 31	mpan2 694	. . . . . 6 |- (R e. RR -> (R x. ((abs` (C .ih D))^2)) e. RR)
33		cjret 6745	. . . . . 6 |- ((R x. ((abs` (C .ih D))^2)) e. RR -> (*` (R x. ((abs` (C .ih D))^2))) = (R x. ((abs` (C .ih D))^2)))
34	27, 32, 33	3syl 20	. . . . 5 |- (D =/= 0h -> (*` (R x. ((abs` (C .ih D))^2))) = (R x. ((abs` (C .ih D))^2)))
35	26, 34	eqtrd 1499	. . . 4 |- (D =/= 0h -> (*` (S x. (D .ih C))) = (R x. ((abs` (C .ih D))^2)))
36	35	opreq2d 3961	. . 3 |- (D =/= 0h -> (((normh` C)^2) - (*` (S x. (D .ih C)))) = (((normh` C)^2) - (R x. ((abs` (C .ih D))^2))))
37	1, 2, 3, 4	pjthlem7 9140	. . . . 5 |- (D =/= 0h -> ((S x. (*` S)) x. (D .ih D)) = (R x. ((abs` (C .ih D))^2)))
38	37, 25	opreq12d 3963	. . . 4 |- (D =/= 0h -> (((S x. (*` S)) x. (D .ih D)) - (S x. (D .ih C))) = ((R x. ((abs` (C .ih D))^2)) - (R x. ((abs` (C .ih D))^2))))
39	27, 32	syl 10	. . . . . 6 |- (D =/= 0h -> (R x. ((abs` (C .ih D))^2)) e. RR)
40	39	recnd 5287	. . . . 5 |- (D =/= 0h -> (R x. ((abs` (C .ih D))^2)) e. CC)
41		subidt 5367	. . . . 5 |- ((R x. ((abs` (C .ih D))^2)) e. CC -> ((R x. ((abs` (C .ih D))^2)) - (R x. ((abs` (C .ih D))^2))) = 0)
42	40, 41	syl 10	. . . 4 |- (D =/= 0h -> ((R x. ((abs` (C .ih D)