Theorem pjthlem7 9140

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

Proof of Theorem pjthlem7

Step	Hyp	Ref	Expression
1		pjthlem6.1	. . . . 5 |- D e. H~
2		pjthlem6.2	. . . . 5 |- R = (1 / (D .ih D))
3	1, 2	pjthlem2 9135	. . . 4 |- (D =/= 0h -> R e. RR)
4		pjthlem6.4	. . . . . . . . 9 |- S = (R x. (C .ih D))
5	4	a1i 8	. . . . . . . 8 |- (R e. RR -> S = (R x. (C .ih D)))
6		recnt 5285	. . . . . . . . . . 11 |- (R e. RR -> R e. CC)
7		pjthlem6.3	. . . . . . . . . . . . 13 |- C e. H~
8	7, 1	hicl 8869	. . . . . . . . . . . 12 |- (C .ih D) e. CC
9		cjmult 6748	. . . . . . . . . . . 12 |- ((R e. CC /\ (C .ih D) e. CC) -> (*` (R x. (C .ih D))) = ((*` R) x. (*` (C .ih D))))
10	8, 9	mpan2 694	. . . . . . . . . . 11 |- (R e. CC -> (*` (R x. (C .ih D))) = ((*` R) x. (*` (C .ih D))))
11	6, 10	syl 10	. . . . . . . . . 10 |- (R e. RR -> (*` (R x. (C .ih D))) = ((*` R) x. (*` (C .ih D))))
12		cjret 6745	. . . . . . . . . . 11 |- (R e. RR -> (*` R) = R)
13	12	opreq1d 3960	. . . . . . . . . 10 |- (R e. RR -> ((*` R) x. (*` (C .ih D))) = (R x. (*` (C .ih D))))
14	11, 13	eqtrd 1499	. . . . . . . . 9 |- (R e. RR -> (*` (R x. (C .ih D))) = (R x. (*` (C .ih D))))
15	4	fveq2i 3712	. . . . . . . . 9 |- (*` S) = (*` (R x. (C .ih D)))
16	14, 15	syl5eq 1511	. . . . . . . 8 |- (R e. RR -> (*` S) = (R x. (*` (C .ih D))))
17	5, 16	opreq12d 3963	. . . . . . 7 |- (R e. RR -> (S x. (*` S)) = ((R x. (C .ih D)) x. (R x. (*` (C .ih D)))))
18		mul4t 5392	. . . . . . . 8 |- (((R e. CC /\ (C .ih D) e. CC) /\ (R e. CC /\ (*` (C .ih D)) e. CC)) -> ((R x. (C .ih D)) x. (R x. (*` (C .ih D)))) = ((R x. R) x. ((C .ih D) x. (*` (C .ih D)))))
19	6, 8	jctir 293	. . . . . . . 8 |- (R e. RR -> (R e. CC /\ (C .ih D) e. CC))
20	8	cjcl 6699	. . . . . . . . 9 |- (*` (C .ih D)) e. CC
21	6, 20	jctir 293	. . . . . . . 8 |- (R e. RR -> (R e. CC /\ (*` (C .ih D)) e. CC))
22	18, 19, 21	sylanc 471	. . . . . . 7 |- (R e. RR -> ((R x. (C .ih D)) x. (R x. (*` (C .ih D)))) = ((R x. R) x. ((C .ih D) x. (*` (C .ih D)))))
23	17, 22	eqtrd 1499	. . . . . 6 |- (R e. RR -> (S x. (*` S)) = ((R x. R) x. ((C .ih D) x. (*` (C .ih D)))))
24	23	opreq1d 3960	. . . . 5 |- (R e. RR -> ((S x. (*` S)) x. (D .ih D)) = (((R x. R) x. ((C .ih D) x. (*` (C .ih D)))) x. (D .ih D)))
25		axmulcl 5245	. . . . . . 7 |- ((R e. CC /\ R e. CC) -> (R x. R) e. CC)
26	25, 6, 6	sylanc 471	. . . . . 6 |- (R e. RR -> (R x. R) e. CC)
27	8, 20	mulcl 5293	. . . . . . 7 |- ((C .ih D) x. (*` (C .ih D))) e. CC
28	1, 1	hicl 8869	. . . . . . 7 |- (D .ih D) e. CC
29		mul23t 5391	. . . . . . 7 |- (((R x. R) e. CC /\ ((C .ih D) x. (*` (C .ih D))) e. CC /\ (D .ih D) e. CC) -> (((R x. R) x. ((C .ih D) x. (*` (C .ih D)))) x. (D .ih D)) = (((R x. R) x. (D .ih D)) x. ((C .ih D) x. (*` (C .ih D)))))
30	27, 28, 29	mp3an23 905	. . . . . 6 |- ((R x. R) e. CC -> (((R x. R) x. ((C .ih D) x. (*` (C .ih D)))) x. (D .ih D)) = (((R x. R) x. (D .ih D)) x. ((C .ih D) x. (*` (C .ih D)))))
31	26, 30	syl 10	. . . . 5 |- (R e. RR -> (((R x. R) x. ((C .ih D) x. (*` (C .ih D)))) x. (D .ih D)) = (((R x. R) x. (D .ih D)) x. ((C .ih D) x. (*` (C .ih D)))))
32	24, 31	eqtrd 1499	. . . 4 |- (R e. RR -> ((S x. (*` S)) x. (D .ih D)) = (((R x. R) x. (D .ih D)) x. ((C .ih D) x. (*` (C .ih D)))))
33	3, 32	syl 10	. . 3 |- (D =/= 0h -> ((S x. (*` S)) x. (D .ih D)) = (((R x. R) x. (D .ih D)) x. ((C .ih D) x. (*` (C .ih D)))))
34		mul23t 5391	. . . . . . . 8 |- ((R e. CC /\ R e. CC /\ (D .ih D) e. CC) -> ((R x. R) x. (D .ih D)) = ((R x. (D .ih D)) x. R))
35	28, 34	mp3an3 902	. . . . . . 7 |- ((R e. CC /\ R e. CC) -> ((R x. R) x. (D .ih D)) = ((R x. (D .ih D)) x. R))
36	35, 6, 6	sylanc 471	. . . . . 6 |- (R e. RR -> ((R x. R) x. (D .ih D)) = ((R x. (D .ih D)) x. R))
37	3, 36	syl 10	. . . . 5 |- (D =/= 0h -> ((R x. R) x. (D .ih D)) = ((R x. (D .ih D)) x. R))
38		ax-his4 8873	. . . . . . . . . . 11 |- ((D e. H~ /\ D =/= 0h) -> 0 < (D .ih D))
39	1, 38	mpan 693	. . . . . . . . . 10 |- (D =/= 0h -> 0 < (D .ih D))
40		hiidrclt 8882	. . . . . . . . . . . 12 |- (D e. H~ -> (D .ih D) e. RR)
41	1, 40	ax-mp 7	. . . . . . . . . . 11 |- (D .ih D) e. RR
42	41	gt0ne0 5585	. . . . . . . . . 10 |- (0 < (D .ih D) -> (D .ih D) =/= 0)
43	39, 42	syl 10	. . . . . . . . 9 |- (D =/= 0h -> (D .ih D) =/= 0)
44	28	recclz 5683	. . . . . . . . 9 |- ((D .ih D) =/= 0 -> (1 / (D .ih D)) e. CC)
45		axmulcom 5248	. . . . . . . . . 10 |- (((1 / (D .ih D)) e. CC /\ (D .ih D) e. CC) -> ((1 / (D .ih D)) x. (D .ih D)) = ((D .ih D) x. (1 / (D .ih D))))
46	28, 45	mpan2 694	. . . . . . . . 9 |- ((1 / (D .ih D)) e. CC -> ((1 / (D .ih D)) x. (D .ih D)) = ((D .ih D) x. (1 / (D .ih D))))
47	43, 44, 46	3syl 20	. . . . . . . 8 |- (D =/= 0h -> ((1 / (D .ih D)) x. (D .ih D)) = ((D .ih D) x. (1 / (D .ih D))))
48	28	recidz 5697	. . . . . . . . 9 |- ((D .ih D) =/= 0 -> ((D .ih D) x. (1 / (D .ih D))) = 1)
49	39, 42, 48	3syl 20	. . . . . . . 8 |- (D =/= 0h -> ((D .ih D) x. (1 / (D .ih D))) = 1)
50	47, 49	eqtrd 1499	. . . . . . 7 |- (D =/= 0h -> ((1 / (D .ih D)) x. (D .ih D)) = 1)
51	2	opreq1i 3956	. . . . . . 7 |- (R x. (D .ih D)) = ((1 / (D .ih D)) x. (D .ih D))
52	50, 51	syl5eq 1511	. . . . . 6 |- (D =/= 0h -> (R x. (D .ih D)) = 1)
53	52	opreq1d 3960	. . . . 5 |- (D =/= 0h -> ((R x. (D .ih D)) x. R) = (1 x. R))
54		mulid2t 5389	. . . . . 6 |- (R e. CC -> (1 x. R) = R)
55	3, 6, 54	3syl 20	. . . . 5 |- (D =/= 0h -> (1 x. R) = R)
56	37, 53, 55	3eqtrd 1503	. . . 4 |- (D =/= 0h -> ((R x. R) x. (D .ih D)) = R)
57	56	opreq1d 3960	. . 3 |- (D =/= 0h -> (((R x. R) x. (D .ih D)) x. ((C .ih D) x. (*` (C .ih D)))) = (R x. ((C .ih D) x. (*` (C .ih D)))))
58	33, 57	eqtrd 1499	. 2 |- (D =/= 0h -> ((S x. (*` S)) x. (D .ih D)) = (R x. ((C .ih D) x. (*` (C .ih D)))))
59	8	absvalsq 6772	. . 3 |- ((abs` (C .ih D))^2) = ((C .ih D) x. (*` (C .ih D)))
60	59	opreq2i 3957	. 2 |- (R x. ((abs` (C .ih D))^2)) = (R x. ((C .ih D) x. (*` (C .ih D))))
61	58, 60	syl6eqr 1517	1 |- (D =/= 0h -> ((S x. (*` S)) x. (D .ih D)) = (R x. ((abs`