Theorem shftefif1olem 8680

Description: Lemma for shftefif1o 8681.

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 3698	. . . 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 3675	. . . . 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 8678	. . . 4 |- (A e. RR -> (exp` (i x. A)) e. C)
8		shftefif1o.6	. . . . . . 7 |- T = ( x. |` (C X. C))
9	6, 8	circgrp 8679	. . . . . 6 |- T e. Abel
10		ablgrp 8053	. . . . . 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 5246	. . . . . . . 8 |- x. :(CC X. CC)-->CC
14		fdm 3623	. . . . . . . 8 |- ( x. :(CC X. CC)-->CC -> dom x. = (CC X. CC))
15	13, 14	ax-mp 7	. . . . . . 7 |- dom x. = (CC X. CC)
16		ssrab2 2127	. . . . . . . 8 |- {w e. CC | (abs` w) = 1} (_ CC
17	6, 16	eqsstr 2087	. . . . . . 7 |- C (_ CC
18	8	resgrprn 8045	. . . . . . 7 |- ((dom x. = (CC X. CC) /\ T e. Grp /\ C (_ CC) -> C = ran T)
19	15, 11, 17, 18	mp3an 914	. . . . . 6 |- C = ran T
20	12, 19	grplactf1o 8049	. . . . 5 |- ((T e. Grp /\ (exp` (i x. A)) e. C) -> (L` (exp` (i x. A))):C-1-1-onto->C)
21	11, 20	mpan 694	. . . 4 |- ((exp` (i x. A)) e. C -> (L` (exp` (i x. A))):C-1-1-onto->C)
22	7, 21	syl 10	. . 3 |- (A e. RR -> (L` (exp` (i x. A))):C-1-1-onto->C)
23		2re 5934	. . . . . . . 8 |- 2 e. RR
24		pire 8615	. . . . . . . 8 |- pi e. RR
25	23, 24	remulcl 5315	. . . . . . 7 |- (2 x. pi) e. RR
26		axaddrcl 5252	. . . . . . 7 |- ((A e. RR /\ (2 x. pi) e. RR) -> (A + (2 x. pi)) e. RR)
27	25, 26	mpan2 695	. . . . . 6 |- (A e. RR -> (A + (2 x. pi)) e. RR)
28		renegclt 5417	. . . . . 6 |- (A e. RR -> -uA e. RR)
29		shftefif1o.5	. . . . . . . 8 |- S = {<.x, y>. | (x e. (A[,)(A + (2 x. pi))) /\ y = (x + -uA))}
30	29	icoshftf1o 6352	. . . . . . 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)))
31		shftefif1o.1	. . . . . . . 8 |- D = (A[,)(A + (2 x. pi)))
32		f1oeq2 3676	. . . . . . . 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))))
33	31, 32	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)))
34	30, 33	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)))
35	27, 28, 34	mpd3an23 916	. . . . 5 |- (A e. RR -> S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)))
36		recnt 5293	. . . . . . . 8 |- (A e. RR -> A e. CC)
37		negidt 5359	. . . . . . . 8 |- (A e. CC -> (A + -uA) = 0)
38	36, 37	syl 10	. . . . . . 7 |- (A e. RR -> (A + -uA) = 0)
39		negsubt 5362	. . . . . . . . 9 |- (((A + (2 x. pi)) e. CC /\ A e. CC) -> ((A + (2 x. pi)) + -uA) = ((A + (2 x. pi)) - A))
40	27	recnd 5295	. . . . . . . . 9 |- (A e. RR -> (A + (2 x. pi)) e. CC)
41	39, 40, 36	sylanc 471	. . . . . . . 8 |- (A e. RR -> ((A + (2 x. pi)) + -uA) = ((A + (2 x. pi)) - A))
42	25	recn 5294	. . . . . . . . . 10 |- (2 x. pi) e. CC
43		pncan2t 5378	. . . . . . . . . 10 |- ((A e. CC /\ (2 x. pi) e. CC) -> ((A + (2 x. pi)) - A) = (2 x. pi))
44	42, 43	mpan2 695	. . . . . . . . 9 |- (A e. CC -> ((A + (2 x. pi)) - A) = (2 x. pi))
45	36, 44	syl 10	. . . . . . . 8 |- (A e. RR -> ((A + (2 x. pi)) - A) = (2 x. pi))
46	41, 45	eqtrd 1504	. . . . . . 7 |- (A e. RR -> ((A + (2 x. pi)) + -uA) = (2 x. pi))
47	38, 46	opreq12d 3969	. . . . . 6 |- (A e. RR -> ((A + -uA)[,)((A + (2 x. pi)) + -uA)) = (0[,)(2 x. pi)))
48		f1oeq3 3677	. . . . . 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))))
49	47, 48	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))))
50	35, 49	mpbid 195	. . . 4 |- (A e. RR -> S:D-1-1-onto->(0[,)(2 x. pi)))
51		shftefif1o.4	. . . . . 6 |- F = {<.x, y>. | (x e. (0[,)(2 x. pi)) /\ y = (exp` (i x. x)))}
52	51, 6	efif1o 8672	. . . . 5 |- F:(0[,)(2 x. pi))-1-1-onto->C
53		f1oco 3698	. . . . 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)
54	52, 53	mpan 694	. . . 4 |- (S:D-1-1-onto->(0[,)(2 x. pi)) -> (F o. S):D-1-1-onto->C)
55	50, 54	syl 10	. . 3 |- (A e. RR -> (F o. S):D-1-1-onto->C)
56	5, 22, 55	sylanc 471	. 2 |- (A e. RR -> H:D-1-1-onto->C)
57		opreq2 3960	. . . . . . . . 9 |- (x = z -> (i x. x) = (i x. z))
58	57	fveq2d 3719	. . . . . . . 8 |- (x = z -> (exp` (i x. x)) = (exp` (i x. z)))
59		shftefif1o.2	. . . . . . . 8 |- G = {<.x, y>. | (x e. D /\ y = (exp` (i x. x)))}
60		fvex 3723	. . . . . . . 8 |- (exp` (i x. z)) e. V
61	58, 59, 60	fvopab4 3771	. . . . . . 7 |- (z e. D -> (G` z) = (exp` (i x. z)))
62	61	adantl 388	. . . . . 6 |- ((A e. RR /\ z e. D) -> (G` z) = (exp` (i x. z)))
63		fvco3 3767	. . . . . . . . . . . 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)))
64	63	3expa 832	. . . . . . . . . . 11 |- (((Fun (L` (exp` (i x. A)))