Theorem pjthlem8 5232

Description: Lemma for Theorem 3.7(i) of [Beran] p. 102.

Hypotheses

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

Assertion

Ref	Expression
pjthlem8	|- (-. D = 0v -> ((norm` (C -v (S .s D)))^2) = (((norm` C)^2) - (R x. ((abs` (C .i D))^2))))

Proof of Theorem pjthlem8

Step	Hyp	Ref	Expression
1		pjthlem6.1	. . . 4 |- D e. H~
2		pjthlem6.2	. . . 4 |- R = (1 / (D .i D))
3		pjthlem6.3	. . . 4 |- C e. H~
4		pjthlem6.4	. . . 4 |- S = (R x. (C .i D))
5	1, 2, 3, 4	pjthlem4 5228	. . 3 |- (-. D = 0v -> S e. CC)
6		opreq1 3006	. . . . . . . 8 |- (S = if(S e. CC, S, 0) -> (S .s D) = (if(S e. CC, S, 0) .s D))
7	6	opreq2d 3013	. . . . . . 7 |- (S = if(S e. CC, S, 0) -> (C -v (S .s D)) = (C -v (if(S e. CC, S, 0) .s D)))
8	7	fveq2d 2836	. . . . . 6 |- (S = if(S e. CC, S, 0) -> (norm` (C -v (S .s D))) = (norm` (C -v (if(S e. CC, S, 0) .s D))))
9	8	opreq1d 3012	. . . . 5 |- (S = if(S e. CC, S, 0) -> ((norm` (C -v (S .s D)))^2) = ((norm` (C -v (if(S e. CC, S, 0) .s D)))^2))
10		opreq1 3006	. . . . . . . 8 |- (S = if(S e. CC, S, 0) -> (S x. (D .i C)) = (if(S e. CC, S, 0) x. (D .i C)))
11	10	fveq2d 2836	. . . . . . 7 |- (S = if(S e. CC, S, 0) -> (*` (S x. (D .i C))) = (*` (if(S e. CC, S, 0) x. (D .i C))))
12	11	opreq2d 3013	. . . . . 6 |- (S = if(S e. CC, S, 0) -> (((norm` C)^2) - (*` (S x. (D .i C)))) = (((norm` C)^2) - (*` (if(S e. CC, S, 0) x. (D .i C)))))
13		id 9	. . . . . . . . 9 |- (S = if(S e. CC, S, 0) -> S = if(S e. CC, S, 0))
14		fveq2 2832	. . . . . . . . 9 |- (S = if(S e. CC, S, 0) -> (*` S) = (*` if(S e. CC, S, 0)))
15	13, 14	opreq12d 3014	. . . . . . . 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 3012	. . . . . . 7 |- (S = if(S e. CC, S, 0) -> ((S x. (*` S)) x. (D .i D)) = ((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .i D)))
17	16, 10	opreq12d 3014	. . . . . 6 |- (S = if(S e. CC, S, 0) -> (((S x. (*` S)) x. (D .i D)) - (S x. (D .i C))) = (((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .i D)) - (if(S e. CC, S, 0) x. (D .i C))))
18	12, 17	opreq12d 3014	. . . . 5 |- (S = if(S e. CC, S, 0) -> ((((norm` C)^2) - (*` (S x. (D .i C)))) + (((S x. (*` S)) x. (D .i D)) - (S x. (D .i C)))) = ((((norm` C)^2) - (*` (if(S e. CC, S, 0) x. (D .i C)))) + (((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .i D)) - (if(S e. CC, S, 0) x. (D .i C)))))
19	9, 18	cleq12d 1115	. . . 4 |- (S = if(S e. CC, S, 0) -> (((norm` (C -v (S .s D)))^2) = ((((norm` C)^2) - (*` (S x. (D .i C)))) + (((S x. (*` S)) x. (D .i D)) - (S x. (D .i C)))) <-> ((norm` (C -v (if(S e. CC, S, 0) .s D)))^2) = ((((norm` C)^2) - (*` (if(S e. CC, S, 0) x. (D .i C)))) + (((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .i D)) - (if(S e. CC, S, 0) x. (D .i C))))))
20		0cn 4100	. . . . . 6 |- 0 e. CC
21	20	elimel 1793	. . . . 5 |- if(S e. CC, S, 0) e. CC
22	1, 3, 21	pjthlem5 5229	. . . 4 |- ((norm` (C -v (if(S e. CC, S, 0) .s D)))^2) = ((((norm` C)^2) - (*` (if(S e. CC, S, 0) x. (D .i C)))) + (((if(S e. CC, S, 0) x. (*` if(S e. CC, S, 0))) x. (D .i D)) - (if(S e. CC, S, 0) x. (D .i C))))
23	19, 22	dedth 1784	. . 3 |- (S e. CC -> ((norm` (C -v (S .s D)))^2) = ((((norm` C)^2) - (*` (S x. (D .i C)))) + (((S x. (*` S)) x. (D .i D)) - (S x. (D .i C)))))
24	5, 23	syl 12	. 2 |- (-. D = 0v -> ((norm` (C -v (S .s D)))^2) = ((((norm` C)^2) - (*` (S x. (D .i C)))) + (((S x. (*` S)) x. (D .i D)) - (S x. (D .i C)))))
25	1, 2, 3, 4	pjthlem6 5230	. . . . . 6 |- (-. D = 0v -> (S x. (D .i C)) = (R x. ((abs` (C .i D))^2)))
26	25	fveq2d 2836	. . . . 5 |- (-. D = 0v -> (*` (S x. (D .i C))) = (*` (R x. ((abs` (C .i D))^2))))
27	1, 2	pjthlem2 5226	. . . . . 6 |- (-. D = 0v -> R e. RR)
28	3, 1	hicl 5044	. . . . . . . . 9 |- (C .i D) e. CC
29	28	abscl 4840	. . . . . . . 8 |- (abs` (C .i D)) e. RR
30	29	sqrecl 4699	. . . . . . 7 |- ((abs` (C .i D))^2) e. RR
31		axmulrcl 4069	. . . . . . 7 |- ((R e. RR /\ ((abs` (C .i D))^2) e. RR) -> (R x. ((abs` (C .i D))^2)) e. RR)
32	30, 31	mpan2 519	. . . . . 6 |- (R e. RR -> (R x. ((abs` (C .i D))^2)) e. RR)
33		cjret 4829	. . . . . 6 |- ((R x. ((abs` (C .i D))^2)) e. RR -> (*` (R x. ((abs` (C .i D))^2))) = (R x. ((abs` (C .i D))^2)))
34	27, 32, 33	3syl 21	. . . . 5 |- (-. D = 0v -> (*` (R x. ((abs` (C .i D))^2))) = (R x. ((abs` (C .i D))^2)))
35	26, 34	eqtrd 1128	. . . 4 |- (-. D = 0v -> (*` (S x. (D .i C))) = (R x. ((abs` (C .i D))^2)))
36	35	opreq2d 3013	. . 3 |- (-. D = 0v -> (((norm` C)^2) - (*` (S x. (D .i C)))) = (((norm` C)^2) - (R x. ((abs` (C .i D))^2))))
37	1, 2, 3, 4	pjthlem7 5231	. . . . 5 |- (-. D = 0v -> ((S x. (*` S)) x. (D .i D)) = (R x. ((abs` (C .i D))^2)))
38	37, 25	opreq12d 3014	. . . 4 |- (-. D = 0v -> (((S x. (*` S)) x. (D .i D)) - (S x. (D .i C))) = ((R x. ((abs` (C .i D))^2)) - (R x. ((abs` (C .i D))^2))))
39	27, 32	syl 12	. . . . . 6 |- (-. D = 0v -> (R x. ((abs` (C .i D))^2)) e. RR)
40	39	recnd 4099	. . . . 5 |- (-. D = 0v -> (R x. ((abs` (C .i D))^2)) e. CC)
41		subidt 4159	. . . . 5 |- ((R x. ((abs` (C .i D))^2)) e. CC -> ((R x. ((abs` (C .i D))^2)) - (R x. ((abs` (C .i D))^2))) = 0)
42	40, 41	syl 12	. . . 4 |- (-. D = 0v -> ((R x. ((abs` (C .i D))^2)) - (R x. ((abs` (C .i D))^2))) = 0)
43	38, 42	eqtrd