Theorem shftefif1olem 10095

Description: Lemma for shftefif1o 10096.

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		shftefif1o.3	. . . . 5 |- C = {w e. CC | (abs` w) = 1}
2	1	efielcirc 10093	. . . 4 |- (A e. RR -> (exp` (_i x. A)) e. C)
3		shftefif1o.6	. . . . . . 7 |- T = ( x. |` (C X. C))
4	1, 3	circgrp 10094	. . . . . 6 |- T e. Abel
5		ablgrp 9410	. . . . . 6 |- (T e. Abel -> T e. Grp)
6	4, 5	ax-mp 7	. . . . 5 |- T e. Grp
7		shftefif1o.7	. . . . . 6 |- L = {<.u, v>. | (u e. C /\ v = {<.x, y>. | (x e. C /\ y = (uTx))})}
8		axmulopr 6418	. . . . . . . 8 |- x. :(CC X. CC)-->CC
9	8	fdmi 4568	. . . . . . 7 |- dom x. = (CC X. CC)
10		ssrab2 2692	. . . . . . . 8 |- {w e. CC | (abs` w) = 1} C_ CC
11	1, 10	eqsstri 2647	. . . . . . 7 |- C C_ CC
12	3	resgrprn 9403	. . . . . . 7 |- ((dom x. = (CC X. CC) /\ T e. Grp /\ C C_ CC) -> C = ran T)
13	9, 6, 11, 12	mp3an 1191	. . . . . 6 |- C = ran T
14	7, 13	grplactf1o 9406	. . . . 5 |- ((T e. Grp /\ (exp` (_i x. A)) e. C) -> (L` (exp` (_i x. A))):C-1-1-onto->C)
15	6, 14	mpan 759	. . . 4 |- ((exp` (_i x. A)) e. C -> (L` (exp` (_i x. A))):C-1-1-onto->C)
16	2, 15	syl 12	. . 3 |- (A e. RR -> (L` (exp` (_i x. A))):C-1-1-onto->C)
17		2re 7163	. . . . . . . 8 |- 2 e. RR
18		pire 10026	. . . . . . . 8 |- pi e. RR
19	17, 18	remulcli 6488	. . . . . . 7 |- (2 x. pi) e. RR
20		readdcl 6455	. . . . . . 7 |- ((A e. RR /\ (2 x. pi) e. RR) -> (A + (2 x. pi)) e. RR)
21	19, 20	mpan2 760	. . . . . 6 |- (A e. RR -> (A + (2 x. pi)) e. RR)
22		renegcl 6600	. . . . . 6 |- (A e. RR -> -uA e. RR)
23		shftefif1o.5	. . . . . . . 8 |- S = {<.x, y>. | (x e. (A[,)(A + (2 x. pi))) /\ y = (x + -uA))}
24	23	icoshftf1o 7580	. . . . . . 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)))
25		shftefif1o.1	. . . . . . . 8 |- D = (A[,)(A + (2 x. pi)))
26		f1oeq2 4631	. . . . . . . 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))))
27	25, 26	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)))
28	24, 27	sylibr 217	. . . . . 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)))
29	21, 22, 28	mpd3an23 1193	. . . . 5 |- (A e. RR -> S:D-1-1-onto->((A + -uA)[,)((A + (2 x. pi)) + -uA)))
30		recn 6466	. . . . . . . 8 |- (A e. RR -> A e. CC)
31		negid 6536	. . . . . . . 8 |- (A e. CC -> (A + -uA) = 0)
32	30, 31	syl 12	. . . . . . 7 |- (A e. RR -> (A + -uA) = 0)
33	21	recnd 6468	. . . . . . . . 9 |- (A e. RR -> (A + (2 x. pi)) e. CC)
34		negsub 6540	. . . . . . . . 9 |- (((A + (2 x. pi)) e. CC /\ A e. CC) -> ((A + (2 x. pi)) + -uA) = ((A + (2 x. pi)) - A))
35	33, 30, 34	syl11anc 524	. . . . . . . 8 |- (A e. RR -> ((A + (2 x. pi)) + -uA) = ((A + (2 x. pi)) - A))
36	19	recni 6467	. . . . . . . . . 10 |- (2 x. pi) e. CC
37		pncan2 6558	. . . . . . . . . 10 |- ((A e. CC /\ (2 x. pi) e. CC) -> ((A + (2 x. pi)) - A) = (2 x. pi))
38	36, 37	mpan2 760	. . . . . . . . 9 |- (A e. CC -> ((A + (2 x. pi)) - A) = (2 x. pi))
39	30, 38	syl 12	. . . . . . . 8 |- (A e. RR -> ((A + (2 x. pi)) - A) = (2 x. pi))
40	35, 39	eqtrd 1925	. . . . . . 7 |- (A e. RR -> ((A + (2 x. pi)) + -uA) = (2 x. pi))
41	32, 40	opreq12d 4900	. . . . . 6 |- (A e. RR -> ((A + -uA)[,)((A + (2 x. pi)) + -uA)) = (0[,)(2 x. pi)))
42		f1oeq3 4632	. . . . . 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))))
43	41, 42	syl 12	. . . . 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))))
44	29, 43	mpbid 212	. . . 4 |- (A e. RR -> S:D-1-1-onto->(0[,)(2 x. pi)))
45		shftefif1o.4	. . . . . 6 |- F = {<.x, y>. | (x e. (0[,)(2 x. pi)) /\ y = (exp` (_i x. x)))}
46	45, 1	efif1o 10092	. . . . 5 |- F:(0[,)(2 x. pi))-1-1-onto->C
47		f1oco 4661	. . . . 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)
48	46, 47	mpan 759	. . . 4 |- (S:D-1-1-onto->(0[,)(2 x. pi)) -> (F o. S):D-1-1-onto->C)
49	44, 48	syl 12	. . 3 |- (A e. RR -> (F o. S):D-1-1-onto->C)
50		f1oco 4661	. . . 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)
51		shftefif1o.8	. . . . 5 |- H = ((L` (exp` (_i x. A))) o. (F o. S))
52		f1oeq1 4630	. . . . 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))
53	51, 52	ax-mp 7	. . . 4 |- (H:D-1-1-onto->C <-> ((L` (exp` (_i x. A))) o. (F o. S)):D-1-1-onto->C)
54	50, 53	sylibr 217	. . 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)
55	16, 49, 54	syl11anc 524	. 2 |- (A e. RR -> H:D-1-1-onto->C)
56		opreq2 4890	. . . . . . . . 9 |- (x = z -> (_i x. x) = (_i x. z))
57	56	fveq2d 4685	. . . . . . . 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 4689	. . . . . . . 8 |- (exp` (_i x. z)) e. _V
60	57, 58, 59	fvopab4 4743	. . . . . . 7 |- (z e. D -> (G` z) = (exp` (_i x. z)))
61	60	adantl 424	. . . . . 6 |- ((A e. RR /\ z e. D) -> (G` z) = (exp` (_i x. z)))
62		fvco3 4739	. . . . . . . . . . . 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 1067	. . . . . . . . . . 11 |- (((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		f1ofun 4637	. . . . . . . . . . . . 13 |- ((L` (exp` (_i x. A))):C-1-1-onto->C -> Fun (L` (exp` (_i x. A))))
65	16, 64	syl 12	. . . . . . . . . . . 12 |- (A e. RR -> Fun (L` (exp` (_i x. A))))
66		f1of 4635	. . . . . . . . . . . . 13 |- ((F o. S):D-1-1-onto->C -> (F o. S):D-->C)
67	49, 66	syl 12	. . . . . . . . . . . 12 |- (A e. RR -> (F o. S):D-->C)
68	65, 67	jca 310	. . . . . . . . . . 11 |- (A e. RR -> (Fun (L` (exp` (_i x. A))) /\ (F o. S):D-->C))
69	63, 68	sylan 497	. . . . . . . . . 10 |- ((A e. RR /\ z e. D) -> (((L` (exp` (_i x. A))) o. (F o. S))` z) = ((L` (exp` (_i x. A)))` ((F o. S)` z)))
70	51	fveq1i 4682	. . . . . . . . . 10 |- (H` z) = (((L` (exp` (_i x. A))) o. (F o. S))` z)
71	69, 70	syl5eq 1940	. . . . . . . . 9 |- ((A e. RR /\ z e. D) -> (H` z) = ((L` (exp` (_i x. A)))` ((F o. S)` z)))
72		f1ofun 4637	. . . . . . . . . . . . 13 |- (F:(0[,)(2 x. pi))-1-1-onto->C -> Fun F)
73	46, 72	ax-mp 7	. . . . . . . . . . . 12 |- Fun F
74		fvco3 4739	. . . . . . . . . . . 12 |- ((Fun F /\ S:D-->(0[,)(2 x. pi)) /\ z e. D) -> ((F o. S)` z) = (F` (S` z)))
75	73, 74	mp3an1 1178	. . . . . . . . . . 11 |- ((S:D-->(0[,)(2 x. pi)) /\ z e. D) -> ((F o. S)` z) = (F` (S` z)))
76		f1of 4635	. . . . . . . . . . . 12 |- (S:D-1-1-onto->(0[,)(2 x. pi)) -> S:D-->(0[,)(2 x. pi)))
77	44, 76	syl 12	. . . . . . . . . . 11 |- (A e. RR -> S:D-->(0[,)(2 x. pi)))
78	75, 77	sylan 497	. . . . . . . . . 10 |- ((A e. RR /\ z e. D) -> ((F o. S)` z) = (F` (S` z)))
79	78	fveq2d 4685	. . . . . . . . 9 |- ((A e. RR /\ z e. D) -> ((L` (exp` (_i x. A)))` ((F o. S)` z)) = ((L` (exp` (_i x. A)))` (F` (S` z))))
80	71, 79	eqtrd 1925	. . . . . . . 8 |- ((A e. RR /\ z e. D) -> (H` z) = ((L` (exp` (_i x. A)))` (F` (S` z))))
81	25	eleq2i 1961	. . . . . . . . . . . . . 14 |- (z e. D <-> z e. (A[,)(A + (2 x. pi))))
82		opreq1 4889	. . . . . . . . . . . . . . 15 |- (x = z -> (x + -uA) = (z + -uA))
83		oprex 4907	. . . . . . . . . . . . . . 15 |- (z + -uA) e. _V
84	82, 23, 83	fvopab4 4743	. . . . . . . . . . . . . 14 |- (z e. (A[,)(A + (2 x. pi))) -> (S` z) = (z + -uA))
85	81, 84	sylbi 216	. . . . . . . . . . . . 13 |- (z e. D -> (S` z) = (z + -uA))
86	85	adantl 424	. . . . . . . . . . . 12 |- ((A e. RR /\ z e. D) -> (S` z) = (z + -uA))
87		elico2 7559	. . . . . . . . . . . . . . . . . 18 |- ((A e. RR /\ (A + (2 x. pi)) e. RR) -> (z e. (A[,)(A + (2 x. pi))) <-> (z e. RR /\ A <_ z /\ z < (A + (2 x. pi)))))
88	21, 87	mpdan 768	. . . . . . . . . . . . . . . . 17 |- (A e. RR -> (z e. (A[,)(A + (2 x. pi))) <-> (z e. RR /\ A <_ z /\ z < (A + (2 x. pi)))))
89	88, 81	syl5bb 591	. . . . . . . . . . . . . . . 16 |- (A e. RR -> (z e. D <-> (z e. RR /\ A <_ z /\ z < (A + (2 x. pi)))))
90	89	biimpa 460	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ z e. D) -> (z e. RR /\ A <_ z /\ z < (A + (2 x. pi))))
91	90	simp1d 888	. . . . . . . . . . . . . 14 |- ((A e. RR /\ z e. D) -> z e. RR)
92	91	recnd 6468	. . . . . . . . . . . . 13 |- ((A e. RR /\ z e. D) -> z e. CC)
93	30	adantr 425	. . . . . . . . . . . . 13 |- ((A e. RR /\ z e. D) -> A e. CC)
94		negsub 6540	. . . . . . . . . . . . 13 |- ((z e. CC /\ A e. CC) -> (z + -uA) = (z - A))
95	92, 93, 94	syl11anc 524	. . . . . . . . . . . 12 |- ((A e. RR /\ z e. D) -> (z + -uA) = (z - A))
96	86, 95	eqtrd 1925	. . . . . . . . . . 11 |- ((A e. RR /\ z e. D) -> (S` z) = (z - A))
97	96	fveq2d 4685	. . . . . . . . . 10 |- ((A e. RR /\ z e. D) -> (F` (S` z)) = (F` (z - A)))
98		icoshft 7577	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ (A + (2 x. pi)) e. RR /\ -uA e. RR) -> (z e. (A[,)(A + (2 x. pi))) -> (z + -uA) e. ((A + -uA)[,)((A + (2 x. pi)) + -uA))))
99	21, 22, 98	mpd3an23 1193	. . . . . . . . . . . . . 14 |- (A e. RR -> (z e. (A[,)(A + (2 x. pi))) -> (z + -uA) e. ((A + -uA)[,)((A + (2 x. pi)) + -uA))))
100	99, 81	syl5ib 223	. . . . . . . . . . . . 13 |- (A e. RR -> (z e. D -> (z + -uA) e. ((A + -uA)[,)((A + (2 x. pi)) + -uA))))
101	100	imp 377	. . . . . . . . . . . 12 |- ((A e. RR /\ z e. D) -> (z + -uA) e. ((A + -uA)[,)((A + (2 x. pi)) + -uA)))
102	41	adantr 425	. . . . . . . . . . . . 13 |- ((A e. RR /\ z e. D) -> ((A + -uA)[,)((A + (2 x. pi)) + -uA)) = (0[,)(2 x. pi)))
103	95, 102	eleq12d 1965	. . . . . . . . . . . 12 |- ((A e. RR /\ z e. D) -> ((z + -uA) e. ((A + -uA)[,)((A + (2 x. pi)) + -uA)) <-> (z - A) e. (0[,)(2 x. pi))))
104	101, 103	mpbid 212	. . . . . . . . . . 11 |- ((A e. RR /\ z e. D) -> (z - A) e. (0[,)(2 x. pi)))
105		opreq2 4890	. . . . . . . . . . . . 13 |- (x = (z - A) -> (_i x. x) = (_i x. (z - A)))
106	105	fveq2d 4685	. . . . . . . . . . . 12 |- (x = (z - A) -> (exp` (_i x. x)) = (exp` (_i x. (z - A))))
107		fvex 4689	. . . . . . . . . . . 12 |- (exp` (_i x. (z - A))) e. _V
108	106, 45, 107	fvopab4 4743	. . . . . . . . . . 11 |- ((z - A) e. (0[,)(2 x. pi)) -> (F` (z - A)) = (exp` (_i x. (z - A))))
109	104, 108	syl 12	. . . . . . . . . 10 |- ((A e. RR /\ z e. D) -> (F` (z - A)) = (exp` (_i x. (z - A))))
110	97, 109	eqtrd 1925	. . . . . . . . 9 |- ((A e. RR /\ z e. D) -> (F` (S` z)) = (exp` (_i x. (z - A))))
111	110	fveq2d 4685	. . . . . . . 8 |- ((A e. RR /\ z e. D) -> ((L` (exp` (_i x. A)))` (F` (S` z))) = ((L` (exp` (_i x. A)))` (exp` (_i x. (z - A)))))
112	2	adantr 425	. . . . . . . . 9 |- ((A e. RR /\ z e. D) -> (exp` (_i x. A)) e. C)
113		simpl 346	. . . . . . . . . . 11 |- ((A e. RR /\ z e. D) -> A e. RR)
114		resubcl 6601	. . . . . . . . . . 11 |- ((z e. RR /\ A e. RR) -> (z - A) e. RR)
115	91, 113, 114	syl11anc 524	. . . . . . . . . 10 |- ((A e. RR /\ z e. D) -> (z - A) e. RR)
116	1	efielcirc 10093	. . . . . . . . . 10 |- ((z - A) e. RR -> (exp` (_i x. (z - A))) e. C)
117	115, 116	syl 12	. . . . . . . . 9 |- ((A e. RR /\ z e. D) -> (exp` (_i x. (z - A))) e. C)
118	7, 13	grplactval 9405	. . . . . . . . . . 11 |- ((T e. Grp /\ (exp` (_i x. A)) e. C /\ (exp` (_i x. (z - A))) e. C) -> ((L` (exp` (_i x. A)))` (exp` (_i x. (z - A)))) = ((exp` (_i x. A))T(exp` (_i x. (z - A)))))
119	6, 118	mp3an1 1178	. . . . . . . . . 10 |- (((exp` (_i x. A)) e. C /\ (exp` (_i x. (z - A))) e. C) -> ((L` (exp` (_i x. A)))` (exp` (_i x. (z - A)))) = ((exp` (_i x. A))T(exp` (_i x. (z - A)))))
120		oprvres 4963	. . . . . . . . . . 11 |- (((exp` (_i x. A)) e. C /\ (exp` (_i x. (z - A))) e. C) -> ((exp` (_i x. A))( x. |` (C X. C))(exp` (_i x. (z - A)))) = ((exp` (_i x. A)) x. (exp` (_i x. (z - A)))))
121	3	opreqi 4896	. . . . . . . . . . 11 |- ((exp` (_i x. A))T(exp` (_i x. (z - A)))) = ((exp` (_i x. A))( x. |` (C X. C))(exp` (_i x. (z - A))))
122	120, 121	syl5eq 1940	. . . . . . . . . 10 |- (((exp` (_i x. A)) e. C /\ (exp` (_i x. (z - A))) e. C) -> ((exp` (_i x. A))T(exp` (_i x. (z - A)))) = ((exp` (_i x. A)) x. (exp` (_i x. (z - A)))))
123	119, 122	eqtrd 1925	. . . . . . . . 9 |- (((exp` (_i x. A)) e. C /\ (exp` (_i x. (z - A))) e. C) -> ((L` (exp` (_i x. A)))` (exp` (_i x. (z - A)))) = ((exp` (_i x. A)) x. (exp` (_i x. (z - A)))))
124	112, 117, 123	syl11anc 524	. . . . . . . 8 |- ((A e. RR /\ z e. D) -> ((L` (exp` (_i x. A)))` (exp` (_i x. (z - A)))) = ((exp` (_i x. A)) x. (exp` (_i x. (z - A)))))
125	80, 111, 124	3eqtrd 1929	. . . . . . 7 |- ((A e. RR /\ z e. D) -> (H` z) = ((exp` (_i x. A)) x. (exp` (_i x. (z - A)))))
126		axicn 6423	. . . . . . . . . . 11 |- _i e. CC
127		mulcl 6456	. . . . . . . . . . 11 |- ((_i e. CC /\ A e. CC) -> (_i x. A) e. CC)
128	126, 127	mpan 759	. . . . . . . . . 10 |- (A e. CC -> (_i x. A) e. CC)
129	30, 128	syl 12	. . . . . . . . 9 |- (A e. RR -> (_i x. A) e. CC)
130	129	adantr 425	. . . . . . . 8 |- ((A e. RR /\ z e. D) -> (_i x. A) e. CC)
131	115	recnd 6468	. . . . . . . . 9 |- ((A e. RR /\ z e. D) -> (z - A) e. CC)
132		mulcl 6456	. . . . . . . . . 10 |- ((_i e. CC /\ (z - A) e. CC) -> (_i x. (z - A)) e. CC)
133	126, 132	mpan 759	. . . . . . . . 9 |- ((z - A) e. CC -> (_i x. (z - A)) e. CC)
134	131, 133	syl 12	. . . . . . . 8 |- ((A e. RR /\ z e. D) -> (_i x. (z - A)) e. CC)
135		efadd 8629	. . . . . . . 8 |- (((_i x. A) e. CC /\ (_i x. (z - A)) e. CC) -> (exp` ((_i x. A) + (_i x. (z - A)))) = ((exp` (_i x. A)) x. (exp` (_i x. (z - A)))))
136	130, 134, 135	syl11anc 524	. . . . . . 7 |- ((A e. RR /\ z e. D) -> (exp` ((_i x. A) + (_i x. (z - A)))) = ((exp` (_i x. A)) x. (exp` (_i x. (z - A)))))
137		adddi 6462	. . . . . . . . . . 11 |- ((_i e. CC /\ A e. CC /\ (z - A) e. CC) -> (_i x. (A + (z - A))) = ((_i x. A) + (_i x. (z - A))))
138	126, 137	mp3an1 1178	. . . . . . . . . 10 |- ((A e. CC /\ (z - A) e. CC) -> (_i x. (A + (z - A))) = ((_i x. A) + (_i x. (z - A))))
139	93, 131, 138	syl11anc 524	. . . . . . . . 9 |- ((A e. RR /\ z e. D) -> (_i x. (A + (z - A))) = ((_i x. A) + (_i x. (z - A))))
140		pncan3 6534	. . . . . . . . . . 11 |- ((A e. CC /\ z e. CC) -> (A + (z - A)) = z)
141	93, 92, 140	syl11anc 524	. . . . . . . . . 10 |- ((A e. RR /\ z e. D) -> (A + (z - A)) = z)
142	141	opreq2d 4898	. . . . . . . . 9 |- ((A e. RR /\ z e. D) -> (_i x. (A + (z - A))) = (_i x. z))
143	139, 142	eqtr3d 1927	. . . . . . . 8 |- ((A e. RR /\ z e. D) -> ((_i x. A) + (_i x. (z - A))) = (_i x. z))
144	143	fveq2d 4685	. . . . . . 7 |- ((A e. RR /\ z e. D) -> (exp` ((_i x. A) + (_i x. (z - A)))) = (exp` (_i x. z)))
145	125, 136, 144	3eqtr2d 1932	. . . . . 6 |- ((A e. RR /\ z e. D) -> (H` z) = (exp` (_i x. z)))
146	61, 145	eqtr4d 1928	. . . . 5 |- ((A e. RR /\ z e. D) -> (G` z) = (H` z))
147	146	r19.21aiva 2176	. . . 4 |- (A e. RR -> A.z e. D (G` z) = (H` z))
148		f1ofn 4636	. . . . . . 7 |- (H:D-1-1-onto->C -> H Fn D)
149	55, 148	syl 12	. . . . . 6 |- (A e. RR -> H Fn D)
150		fvex 4689	. . . . . . . 8 |- (exp` (_i x. x)) e. _V
151	150, 58	fnopab2 4549	. . . . . . 7 |- G Fn D
152		eqfnfv2 4767	. . . . . . 7 |- ((G Fn D /\ H Fn D) -> (G = H <-> A.z e. D (G` z) = (H` z)))
153	151, 152	mpan 759	. . . . . 6 |- (H Fn D -> (G = H <-> A.z e. D (G` z) = (H` z)))
154	149, 153	syl 12	. . . . 5 |- (A e. RR -> (G = H <-> A.z e. D (G` z) = (H` z)))
155	154	biimprd 171	. . . 4 |- (A e. RR -> (A.z e. D (G` z) = (H` z) -> G = H))
156	147, 155	mpd 29	. . 3 |- (A e. RR -> G = H)
157		f1oeq1 4630	. . 3 |- (G = H -> (G:D-1-1-onto->C <-> H:D-1-1-onto->C))
158	156, 157	syl 12	. 2 |- (A e. RR -> (G:D-1-1-onto->C <-> H:D-1-1-onto->C))
159	55, 158	mpbird 213	1 |- (A e. RR -> G:D-1-1-onto->C)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  {crab 2108   C_ wss 2593   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986  ran crn 3987   |` cres 3988   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -1-1-onto->wf1o 3997  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387  _ici 6388   + caddc 6389   x. cmul 6391   - cmin 6445  -ucneg 6446   <_ cle 6448   < clt 6653  2c2 7145  [,)cico 7526  abscabs 8000  expce 8555  picpi 8559  Grpcgr 9311  Abelcabl 9407

This theorem is referenced by:  shftefif1o 10096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731  ax-ac 5906

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-iin 3258  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-r1 5750  df-rank 5751  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-3 7155  df-4 7156  df-5 7157  df-6 7158  df-7 7159  df-8 7160  df-9 7161  df-rp 7232  df-n0 7309  df-z 7345  df-q 7436  df-fl 7463  df-ioo 7528  df-ioc 7529  df-ico 7530  df-icc 7531  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-seq0 7777  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-fac 8184  df-bc 8209  df-clim 8235  df-sum 8240  df-cncf 8525  df-ef 8560  df-sin 8562  df-cos 8563  df-pi 8564  df-top 8861  df-cn 9030  df-cnp 9031  df-met 9070  df-bl 9072  df-opn 9073  df-lm 9200  df-grp 9316  df-gid 9317  df-ginv 9318  df-gdiv 9319  df-abl 9408  df-subg 9424

Copyright terms: Public domain