Theorem pjthlem7 5231

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
pjthlem7	|- (-. D = 0v -> ((S x. (*` S)) x. (D .i D)) = (R x. ((abs` (C .i D))^2)))

Proof of Theorem pjthlem7

Step	Hyp	Ref	Expression
1		pjthlem6.1	. . . . 5 |- D e. H~
2		pjthlem6.2	. . . . 5 |- R = (1 / (D .i D))
3	1, 2	pjthlem2 5226	. . . 4 |- (-. D = 0v -> R e. RR)
4		pjthlem6.4	. . . . . . . . 9 |- S = (R x. (C .i D))
5	4	a1i 7	. . . . . . . 8 |- (R e. RR -> S = (R x. (C .i D)))
6		recnt 4097	. . . . . . . . . . 11 |- (R e. RR -> R e. CC)
7		pjthlem6.3	. . . . . . . . . . . . 13 |- C e. H~
8	7, 1	hicl 5044	. . . . . . . . . . . 12 |- (C .i D) e. CC
9		cjmult 4832	. . . . . . . . . . . 12 |- ((R e. CC /\ (C .i D) e. CC) -> (*` (R x. (C .i D))) = ((*` R) x. (*` (C .i D))))
10	8, 9	mpan2 519	. . . . . . . . . . 11 |- (R e. CC -> (*` (R x. (C .i D))) = ((*` R) x. (*` (C .i D))))
11	6, 10	syl 12	. . . . . . . . . 10 |- (R e. RR -> (*` (R x. (C .i D))) = ((*` R) x. (*` (C .i D))))
12		cjret 4829	. . . . . . . . . . 11 |- (R e. RR -> (*` R) = R)
13	12	opreq1d 3012	. . . . . . . . . 10 |- (R e. RR -> ((*` R) x. (*` (C .i D))) = (R x. (*` (C .i D))))
14	11, 13	eqtrd 1128	. . . . . . . . 9 |- (R e. RR -> (*` (R x. (C .i D))) = (R x. (*` (C .i D))))
15	4	fveq2i 2835	. . . . . . . . 9 |- (*` S) = (*` (R x. (C .i D)))
16	14, 15	syl5eq 1136	. . . . . . . 8 |- (R e. RR -> (*` S) = (R x. (*` (C .i D))))
17	5, 16	opreq12d 3014	. . . . . . 7 |- (R e. RR -> (S x. (*` S)) = ((R x. (C .i D)) x. (R x. (*` (C .i D)))))
18		mul4t 4177	. . . . . . . 8 |- (((R e. CC /\ (C .i D) e. CC) /\ (R e. CC /\ (*` (C .i D)) e. CC)) -> ((R x. (C .i D)) x. (R x. (*` (C .i D)))) = ((R x. R) x. ((C .i D) x. (*` (C .i D)))))
19	6, 8	jctir 241	. . . . . . . 8 |- (R e. RR -> (R e. CC /\ (C .i D) e. CC))
20	8	cjcl 4804	. . . . . . . . 9 |- (*` (C .i D)) e. CC
21	6, 20	jctir 241	. . . . . . . 8 |- (R e. RR -> (R e. CC /\ (*` (C .i D)) e. CC))
22	18, 19, 21	sylanc 361	. . . . . . 7 |- (R e. RR -> ((R x. (C .i D)) x. (R x. (*` (C .i D)))) = ((R x. R) x. ((C .i D) x. (*` (C .i D)))))
23	17, 22	eqtrd 1128	. . . . . 6 |- (R e. RR -> (S x. (*` S)) = ((R x. R) x. ((C .i D) x. (*` (C .i D)))))
24	23	opreq1d 3012	. . . . 5 |- (R e. RR -> ((S x. (*` S)) x. (D .i D)) = (((R x. R) x. ((C .i D) x. (*` (C .i D)))) x. (D .i D)))
25		axmulcl 4068	. . . . . . 7 |- ((R e. CC /\ R e. CC) -> (R x. R) e. CC)
26	25, 6, 6	sylanc 361	. . . . . 6 |- (R e. RR -> (R x. R) e. CC)
27	8, 20	mulcl 4105	. . . . . . 7 |- ((C .i D) x. (*` (C .i D))) e. CC
28	1, 1	hicl 5044	. . . . . . . 8 |- (D .i D) e. CC
29		mul23t 4176	. . . . . . . 8 |- (((R x. R) e. CC /\ ((C .i D) x. (*` (C .i D))) e. CC /\ (D .i D) e. CC) -> (((R x. R) x. ((C .i D) x. (*` (C .i D)))) x. (D .i D)) = (((R x. R) x. (D .i D)) x. ((C .i D) x. (*` (C .i D)))))
30	28, 29	mp3an3 641	. . . . . . 7 |- (((R x. R) e. CC /\ ((C .i D) x. (*` (C .i D))) e. CC) -> (((R x. R) x. ((C .i D) x. (*` (C .i D)))) x. (D .i D)) = (((R x. R) x. (D .i D)) x. ((C .i D) x. (*` (C .i D)))))
31	27, 30	mpan2 519	. . . . . 6 |- ((R x. R) e. CC -> (((R x. R) x. ((C .i D) x. (*` (C .i D)))) x. (D .i D)) = (((R x. R) x. (D .i D)) x. ((C .i D) x. (*` (C .i D)))))
32	26, 31	syl 12	. . . . 5 |- (R e. RR -> (((R x. R) x. ((C .i D) x. (*` (C .i D)))) x. (D .i D)) = (((R x. R) x. (D .i D)) x. ((C .i D) x. (*` (C .i D)))))
33	24, 32	eqtrd 1128	. . . 4 |- (R e. RR -> ((S x. (*` S)) x. (D .i D)) = (((R x. R) x. (D .i D)) x. ((C .i D) x. (*` (C .i D)))))
34	3, 33	syl 12	. . 3 |- (-. D = 0v -> ((S x. (*` S)) x. (D .i D)) = (((R x. R) x. (D .i D)) x. ((C .i D) x. (*` (C .i D)))))
35		mul23t 4176	. . . . . . . 8 |- ((R e. CC /\ R e. CC /\ (D .i D) e. CC) -> ((R x. R) x. (D .i D)) = ((R x. (D .i D)) x. R))
36	28, 35	mp3an3 641	. . . . . . 7 |- ((R e. CC /\ R e. CC) -> ((R x. R) x. (D .i D)) = ((R x. (D .i D)) x. R))
37	36, 6, 6	sylanc 361	. . . . . 6 |- (R e. RR -> ((R x. R) x. (D .i D)) = ((R x. (D .i D)) x. R))
38	3, 37	syl 12	. . . . 5 |- (-. D = 0v -> ((R x. R) x. (D .i D)) = ((R x. (D .i D)) x. R))
39		axhis42 5049	. . . . . . . . . . 11 |- ((D e. H~ /\ -. D = 0v) -> 0 < (D .i D))
40	1, 39	mpan 518	. . . . . . . . . 10 |- (-. D = 0v -> 0 < (D .i D))
41		hiidrclt 5053	. . . . . . . . . . . 12 |- (D e. H~ -> (D .i D) e. RR)
42	1, 41	ax-mp 6	. . . . . . . . . . 11 |- (D .i D) e. RR
43	42	gt0ne0 4340	. . . . . . . . . 10 |- (0 < (D .i D) -> (D .i D) =/= 0)
44	40, 43	syl 12	. . . . . . . . 9 |- (-. D = 0v -> (D .i D) =/= 0)
45		1cn 4101	. . . . . . . . . 10 |- 1 e. CC
46	45, 28	divclz 4222	. . . . . . . . 9 |- ((D .i D) =/= 0 -> (1 / (D .i D)) e. CC)
47		axmulcom 4071	. . . . . . . . . 10 |- (((1 / (D .i D)) e. CC /\ (D .i D) e. CC) -> ((1 / (D .i D)) x. (D .i D)) = ((D .i D) x. (1 / (D .i D))))
48	28, 47	mpan2 519	. . . . . . . . 9 |- ((1 / (D .i D)) e. CC -> ((1 / (D .i D)) x. (D .i D)) = ((D .i D) x. (1 / (D .i D))))
49	44, 46, 48	3syl 21	. . . . . . . 8 |- (-. D = 0v -> ((1 / (D .i D)) x. (D .i D)) = ((D .i D) x. (1 / (D .i D))))
50	28	recidz 4234	. . . . . . . . 9 |- ((D .i D) =/= 0 -> ((D .i D) x. (1 / (D .i D))) = 1)
51	40, 43, 50	3syl 21	. . . . . . . 8 |- (-. D = 0v -> ((D .i D) x. (1 / (D .i D))) = 1)
52	49, 51	eqtrd 1128	. . . . . . 7 |- (-. D = 0v -> ((1 / (D .i D)) x. (D .i D)) = 1)
53	2	opreq1i 3009	. . . . . . 7 |- (R x. (D .i D)) = ((1 / (D .i D)) x. (D .i D))
54	52, 53	syl5eq 1136	. . . . . 6 |- (-. D = 0v -> (R x. (D .i D)) = 1)
55	54	opreq1d 3012	. . . . 5 |- (-. D = 0v -> ((R x. (D .i D)) x. R) = (1 x. R))
56		mulid2t 4175	. . . . . 6 |- (R e. CC -> (1 x. R) = R)
57	3, 6, 56	3syl 21	. . . . 5 |- (-. D = 0v -> (1 x. R) = R)
58	38, 55, 57	3eqtrd 1132	. . . 4 |- (-. D = 0v -> ((R x. R) x. (D .i D)) = R)
59	58	opreq1d 3012	. . 3 |- (-. D = 0v -> (((R x. R) x. (D .i D)) x. ((C .i D) x. (*` (C .i D)))) = (R x. ((C .i D) x. (*` (C .i D)))))
60	34, 59	eqtrd 1128	. 2 |- (-. D = 0v -> ((S x. (*` S)) x. (D .i D)) = (R x. ((C .i D) x. (*` (C .i D)))))
61	8	absvalsq 4837	. . 3 |- ((abs` (C .i D))^2) = ((C .i D) x. (*` (C .i D)))
62	61	opreq2i 3010	. 2 |- (R x. ((abs` (C .i D))