Theorem shftefif1olem 8741

Description: Lemma for shftefif1o 8742.

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
shftefif1olem	|- (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 shftefif1olem

Step	Hyp	Ref	Expression
1		f1oco 3707	. . . 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 3684	. . . . 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	efielcirc 8739	. . . 4 |- (A e. RR -> (exp` (i x. A)) e. C)
8		shftefif1o.6	. . . . . . 7 |- T = ( x. |` (C X. C))
9	6, 8	circgrp 8740	. . . . . 6 |- T e. Abel
10		ablgrp 8102	. . . . . 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 5266	. . . . . . . 8 |- x. :(CC X. CC)-->CC
14	13	fdmi 3632	. . . . . . 7 |- dom x. = (CC X. CC)
15		ssrab2 2131	. . . . . . . 8 |- {w e. CC | (abs` w) = 1} (_ CC
16	6, 15	eqsstr 2091	. . . . . . 7 |- C (_ CC
17	8	resgrprn 8095	. . . . . . 7 |- ((dom x. = (CC X. CC) /\ T e. Grp /\ C (_ CC) -> C = ran T)
18	14, 11, 16, 17	mp3an 916	. . . . . 6 |- C = ran T
19	12, 18	grplactf1o 8098	. . . . 5 |- ((T e. Grp /\ (exp` (i x. A)) e. C) -> (L` (exp` (i x. A))):C-1-1-onto->C)
20	11, 19	mpan 695	. . . 4 |- ((exp` (i x. A)) e. C -> (L` (exp` (i x. A))):C-1-1-onto->C)
21	7, 20	syl 10	. . 3 |- (A e. RR -> (L` (exp` (i x. A))):C-1-1-onto->C)
22		2re 5979	. . . . . . . 8 |- 2 e. RR
23		pire 8677	. . . . . . . 8 |- pi e. RR
24	22, 23	remulcl 5335	. . . . . . 7 |- (2 x. pi) e. RR
25		axaddrcl 5272	. . . . . . 7 |- ((A e. RR /\ (2 x. pi) e. RR) -> (A + (2 x. pi)) e. RR)
26	24, 25	mpan2 696	. . . . . 6 |- (A e. RR -> (A + (2 x. pi)) e. RR)
27		renegclt 5437	. . . . . 6 |- (A e. RR -> -uA e. RR)
28		shftefif1o.5	. . . . . . . 8 |- S = {<.x, y>. | (x e. (A[,)(A + (2 x. pi))) /\ y = (x + -uA))}
29	28	icoshftf1o 6411	. . . . . . 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)))
30		shftefif1o.1	. . . . . . . 8 |- D = (A[,)(A + (2 x. pi)))
31		f1oeq2 3685	. . . . . . . 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))))
32	30, 31	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)))
33	29, 32	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)))
34	26, 27, 33	mpd3an23 918	. . . . 5 |- (A e. RR -> S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)))
35		recnt 5313	. . . . . . . 8 |- (A e. RR -> A e. CC)
36		negidt 5379	. . . . . . . 8 |- (A e. CC -> (A + -uA) = 0)
37	35, 36	syl 10	. . . . . . 7 |- (A e. RR -> (A + -uA) = 0)
38		negsubt 5382	. . . . . . . . 9 |- (((A + (2 x. pi)) e. CC /\ A e. CC) -> ((A + (2 x. pi)) + -uA) = ((A + (2 x. pi)) - A))
39	26	recnd 5315	. . . . . . . . 9 |- (A e. RR -> (A + (2 x. pi)) e. CC)
40	38, 39, 35	sylanc 471	. . . . . . . 8 |- (A e. RR -> ((A + (2 x. pi)) + -uA) = ((A + (2 x. pi)) - A))
41	24	recn 5314	. . . . . . . . . 10 |- (2 x. pi) e. CC
42		pncan2t 5398	. . . . . . . . . 10 |- ((A e. CC /\ (2 x. pi) e. CC) -> ((A + (2 x. pi)) - A) = (2 x. pi))
43	41, 42	mpan2 696	. . . . . . . . 9 |- (A e. CC -> ((A + (2 x. pi)) - A) = (2 x. pi))
44	35, 43	syl 10	. . . . . . . 8 |- (A e. RR -> ((A + (2 x. pi)) - A) = (2 x. pi))
45	40, 44	eqtrd 1507	. . . . . . 7 |- (A e. RR -> ((A + (2 x. pi)) + -uA) = (2 x. pi))
46	37, 45	opreq12d 3978	. . . . . 6 |- (A e. RR -> ((A + -uA)[,)((A + (2 x. pi)) + -uA)) = (0[,)(2 x. pi)))
47		f1oeq3 3686	. . . . . 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))))
48	46, 47	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))))
49	34, 48	mpbid 195	. . . 4 |- (A e. RR -> S:D-1-1-onto->(0[,)(2 x. pi)))
50		shftefif1o.4	. . . . . 6 |- F = {<.x, y>. | (x e. (0[,)(2 x. pi)) /\ y = (exp` (i x. x)))}
51	50, 6	efif1o 8738	. . . . 5 |- F:(0[,)(2 x. pi))-1-1-onto->C
52		f1oco 3707	. . . . 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)
53	51, 52	mpan 695	. . . 4 |- (S:D-1-1-onto->(0[,)(2 x. pi)) -> (F o. S):D-1-1-onto->C)
54	49, 53	syl 10	. . 3 |- (A e. RR -> (F o. S):D-1-1-onto->C)
55	5, 21, 54	sylanc 471	. 2 |- (A e. RR -> H:D-1-1-onto->C)
56		opreq2 3969	. . . . . . . . 9 |- (x = z -> (i x. x) = (i x. z))
57	56	fveq2d 3728	. . . . . . . 8 |- (x = z -> (exp` (i x. x)) = (exp` (i x. z)))
58		shftefif1o.2	. . . . . . . 8 |- G = {<.x, y>. | (x e. D /\ y = (exp` (i x. x)))}
59		fvex 3732	. . . . . . . 8 |- (exp` (i x. z)) e. V
60	57, 58, 59	fvopab4 3780	. . . . . . 7 |- (z e. D -> (G` z) = (exp` (i x. z)))
61	60	adantl 388	. . . . . 6 |- ((A e. RR /\ z e. D) -> (G` z) = (exp` (i x. z)))
62		fvco3 3776	. . . . . . . . . . . 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)))
63	62	3expa 833	. . . . . . . . . . 11 |- (((Fun (L` (exp` (i x. A))) /\ (F o. S):D-->C) /\ z e. D) -> (((L` (exp