Theorem shftefif1olemOLD 8662

Description: Lemma for shftefif1o 8663.

Hypotheses

Ref	Expression
shftefif1o.1	|- D = (A[,)(A + (2 x. pi)))
shftefif1o.2	|- G = {<.x, y>. | (x e. D /\ y = (exp` (i x. x)))}
shftefif1o.3	|- C = {w e. CC | (abs` w) = 1}
shftefif1o.4	|- F = {<.x, y>. | (x e. (0[,)(2 x. pi)) /\ y = (exp` (i x. x)))}
shftefif1o.5	|- S = {<.x, y>. | (x e. (A[,)(A + (2 x. pi))) /\ y = (x + -uA))}
shftefif1o.6	|- T = ( x. |` (C X. C))
shftefif1o.7	|- L = {<.u, v>. | (u e. C /\ v = {<.x, y>. | (x e. C /\ y = (uTx))})}
shftefif1o.8	|- H = ((L` (exp` (i x. A))) o. (F o. S))

Assertion

Ref	Expression
shftefif1olemOLD	|- (A e. RR -> G:D-1-1-onto->C)

Distinct variable groups:   v,A,x,y,w   v,C,x,y   x,D,y   w,v   u,A,w   u,C   w,F   u,T,v,x,y

Proof of Theorem shftefif1olemOLD

Step	Hyp	Ref	Expression
1		f1oco 3692	. . . 4 |- (((L` (exp` (i x. A))):C-1-1-onto->C /\ (F o. S):D-1-1-onto->C) -> ((L` (exp` (i x. A))) o. (F o. S)):D-1-1-onto->C)
2		shftefif1o.8	. . . . 5 |- H = ((L` (exp` (i x. A))) o. (F o. S))
3		f1oeq1 3669	. . . . 5 |- (H = ((L` (exp` (i x. A))) o. (F o. S)) -> (H:D-1-1-onto->C <-> ((L` (exp` (i x. A))) o. (F o. S)):D-1-1-onto->C))
4	2, 3	ax-mp 7	. . . 4 |- (H:D-1-1-onto->C <-> ((L` (exp` (i x. A))) o. (F o. S)):D-1-1-onto->C)
5	1, 4	sylibr 200	. . 3 |- (((L` (exp` (i x. A))):C-1-1-onto->C /\ (F o. S):D-1-1-onto->C) -> H:D-1-1-onto->C)
6		shftefif1o.3	. . . . 5 |- C = {w e. CC | (abs` w) = 1}
7	6	efielcircOLD 8655	. . . 4 |- (A e. RR -> (exp` (i x. A)) e. C)
8		shftefif1o.6	. . . . . . 7 |- T = ( x. |` (C X. C))
9	6, 8	circgrpOLD 8658	. . . . . 6 |- T e. Abel
10		ablgrp 8038	. . . . . 6 |- (T e. Abel -> T e. Grp)
11	9, 10	ax-mp 7	. . . . 5 |- T e. Grp
12		shftefif1o.7	. . . . . 6 |- L = {<.u, v>. | (u e. C /\ v = {<.x, y>. | (x e. C /\ y = (uTx))})}
13		axmulopr 5238	. . . . . . 7 |- x. :(CC X. CC)-->CC
14		ssrab2 2121	. . . . . . . 8 |- {w e. CC | (abs` w) = 1} (_ CC
15	6, 14	eqsstr 2081	. . . . . . 7 |- C (_ CC
16	8	resgrprnOLD 8031	. . . . . . 7 |- (( x. :(CC X. CC)-->CC /\ T e. Grp /\ C (_ CC) -> C = ran T)
17	13, 11, 15, 16	mp3an 913	. . . . . 6 |- C = ran T
18	12, 17	grplactf1o 8034	. . . . 5 |- ((T e. Grp /\ (exp` (i x. A)) e. C) -> (L` (exp` (i x. A))):C-1-1-onto->C)
19	11, 18	mpan 693	. . . 4 |- ((exp` (i x. A)) e. C -> (L` (exp` (i x. A))):C-1-1-onto->C)
20	7, 19	syl 10	. . 3 |- (A e. RR -> (L` (exp` (i x. A))):C-1-1-onto->C)
21		2re 5926	. . . . . . . 8 |- 2 e. RR
22		pire 8596	. . . . . . . 8 |- pi e. RR
23	21, 22	remulcl 5307	. . . . . . 7 |- (2 x. pi) e. RR
24		axaddrcl 5244	. . . . . . 7 |- ((A e. RR /\ (2 x. pi) e. RR) -> (A + (2 x. pi)) e. RR)
25	23, 24	mpan2 694	. . . . . 6 |- (A e. RR -> (A + (2 x. pi)) e. RR)
26		renegclt 5409	. . . . . 6 |- (A e. RR -> -uA e. RR)
27		shftefif1o.5	. . . . . . . 8 |- S = {<.x, y>. | (x e. (A[,)(A + (2 x. pi))) /\ y = (x + -uA))}
28	27	icoshftf1o 6344	. . . . . . 7 |- ((A e. RR /\ (A + (2 x. pi)) e. RR /\ -uA e. RR) -> S:(A[,)(A + (2 x. pi)))-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)))
29		shftefif1o.1	. . . . . . . 8 |- D = (A[,)(A + (2 x. pi)))
30		f1oeq2 3670	. . . . . . . 8 |- (D = (A[,)(A + (2 x. pi))) -> (S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)) <-> S:(A[,)(A + (2 x. pi)))-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA))))
31	29, 30	ax-mp 7	. . . . . . 7 |- (S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)) <-> S:(A[,)(A + (2 x. pi)))-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)))
32	28, 31	sylibr 200	. . . . . 6 |- ((A e. RR /\ (A + (2 x. pi)) e. RR /\ -uA e. RR) -> S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)))
33	25, 26, 32	mpd3an23 915	. . . . 5 |- (A e. RR -> S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)))
34		recnt 5285	. . . . . . . 8 |- (A e. RR -> A e. CC)
35		negidt 5351	. . . . . . . 8 |- (A e. CC -> (A + -uA) = 0)
36	34, 35	syl 10	. . . . . . 7 |- (A e. RR -> (A + -uA) = 0)
37		negsubt 5354	. . . . . . . . 9 |- (((A + (2 x. pi)) e. CC /\ A e. CC) -> ((A + (2 x. pi)) + -uA) = ((A + (2 x. pi)) - A))
38	25	recnd 5287	. . . . . . . . 9 |- (A e. RR -> (A + (2 x. pi)) e. CC)
39	37, 38, 34	sylanc 471	. . . . . . . 8 |- (A e. RR -> ((A + (2 x. pi)) + -uA) = ((A + (2 x. pi)) - A))
40	23	recn 5286	. . . . . . . . . 10 |- (2 x. pi) e. CC
41		pncan2t 5370	. . . . . . . . . 10 |- ((A e. CC /\ (2 x. pi) e. CC) -> ((A + (2 x. pi)) - A) = (2 x. pi))
42	40, 41	mpan2 694	. . . . . . . . 9 |- (A e. CC -> ((A + (2 x. pi)) - A) = (2 x. pi))
43	34, 42	syl 10	. . . . . . . 8 |- (A e. RR -> ((A + (2 x. pi)) - A) = (2 x. pi))
44	39, 43	eqtrd 1499	. . . . . . 7 |- (A e. RR -> ((A + (2 x. pi)) + -uA) = (2 x. pi))
45	36, 44	opreq12d 3963	. . . . . 6 |- (A e. RR -> ((A + -uA)[,)((A + (2 x. pi)) + -uA)) = (0[,)(2 x. pi)))
46		f1oeq3 3671	. . . . . 6 |- (((A + -uA)[,)((A + (2 x. pi)) + -uA)) = (0[,)(2 x. pi)) -> (S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)) <-> S:D-1-1-onto->(0[,)(2 x. pi))))
47	45, 46	syl 10	. . . . 5 |- (A e. RR -> (S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)) <-> S:D-1-1-onto->(0[,)(2 x. pi))))
48	33, 47	mpbid 195	. . . 4 |- (A e. RR -> S:D-1-1-onto->(0[,)(2 x. pi)))
49		shftefif1o.4	. . . . . 6 |- F = {<.x, y>. | (x e. (0[,)(2 x. pi)) /\ y = (exp` (i x. x)))}
50	49, 6	efif1o 8653	. . . . 5 |- F:(0[,)(2 x. pi))-1-1-onto->C
51		f1oco 3692	. . . . 5 |- ((F:(0[,)(2 x. pi))-1-1-onto->C /\ S:D-1-1-onto->(0[,)(2 x. pi))) -> (F o. S):D-1-1-onto->C)
52	50, 51	mpan 693	. . . 4 |- (S:D-1-1-onto->(0[,)(2 x. pi)) -> (F o. S):D-1-1-onto->C)
53	48, 52	syl 10	. . 3 |- (A e. RR -> (F o. S):D-1-1-onto->C)
54	5, 20, 53	sylanc 471	. 2 |- (A e. RR -> H:D-1-1-onto->C)
55		opreq2 3954	. . . . . . . . 9 |- (x = z -> (i x. x) = (i x. z))
56	55	fveq2d 3713	. . . . . . . 8 |- (x = z -> (exp` (i x. x)) = (exp` (i x. z)))
57		shftefif1o.2	. . . . . . . 8 |- G = {<.x, y>. | (x e. D /\ y = (exp` (i x. x)))}
58		fvex 3717	. . . . . . . 8 |- (exp` (i x. z)) e. V
59	56, 57, 58	fvopab4 3765	. . . . . . 7 |- (z e. D -> (G` z) = (exp` (i x. z)))
60	59	adantl 388	. . . . . 6 |- ((A e. RR /\ z e. D) -> (G` z) = (exp` (i x. z)))
61		fvco3 3761	. . . . . . . . . . . 12 |- ((Fun (L` (exp` (i x. A))) /\ (F o. S):D-->C /\ z e. D) -> (((L` (exp` (i x. A))) o. (F o. S))` z) = ((L` (exp` (i x. A)))` ((F o. S)` z)))
62	61	3expa 831	. . . . . . . . . . 11 |- (((Fun (L` (exp` (i x. A))) /\ (F o. S):D-->C) /\ z e. D) -> (((L` (exp` (i x. A))) o. (F o. S