Theorem shftefif1olem 8725

Description: Lemma for shftefif1o 8726.

Hypotheses

Ref	Expression
shftefif1o.1	⊢ D = (A[,)(A + (2 · π)))
shftefif1o.2	⊢ G = {⟨x, y⟩∣(x ∈ D ⋀ y = (exp ‘(i · x)))}
shftefif1o.3	⊢ C = {w ∈ ℂ∣(abs ‘w) = 1}
shftefif1o.4	⊢ F = {⟨x, y⟩∣(x ∈ (0[,)(2 · π)) ⋀ y = (exp ‘(i · x)))}
shftefif1o.5	⊢ S = {⟨x, y⟩∣(x ∈ (A[,)(A + (2 · π))) ⋀ y = (x + -A))}
shftefif1o.6	⊢ T = ( · ↾ (C × C))
shftefif1o.7	⊢ L = {⟨u, v⟩∣(u ∈ C ⋀ v = {⟨x, y⟩∣(x ∈ C ⋀ y = (uTx))})}
shftefif1o.8	⊢ H = ((L ‘(exp ‘(i · A))) ∘ (F ∘ S))

Assertion

Ref	Expression
shftefif1olem	⊢ (A ∈ ℝ → 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 3704	. . . 4 ⊢ (((L ‘(exp ‘(i · A))):C–1-1-onto→C ⋀ (F ∘ S):D–1-1-onto→C) → ((L ‘(exp ‘(i · A))) ∘ (F ∘ S)):D–1-1-onto→C)
2		shftefif1o.8	. . . . 5 ⊢ H = ((L ‘(exp ‘(i · A))) ∘ (F ∘ S))
3		f1oeq1 3681	. . . . 5 ⊢ (H = ((L ‘(exp ‘(i · A))) ∘ (F ∘ S)) → (H:D–1-1-onto→C ↔ ((L ‘(exp ‘(i · A))) ∘ (F ∘ S)):D–1-1-onto→C))
4	2, 3	ax-mp 7	. . . 4 ⊢ (H:D–1-1-onto→C ↔ ((L ‘(exp ‘(i · A))) ∘ (F ∘ S)):D–1-1-onto→C)
5	1, 4	sylibr 200	. . 3 ⊢ (((L ‘(exp ‘(i · A))):C–1-1-onto→C ⋀ (F ∘ S):D–1-1-onto→C) → H:D–1-1-onto→C)
6		shftefif1o.3	. . . . 5 ⊢ C = {w ∈ ℂ∣(abs ‘w) = 1}
7	6	efielcirc 8723	. . . 4 ⊢ (A ∈ ℝ → (exp ‘(i · A)) ∈ C)
8		shftefif1o.6	. . . . . . 7 ⊢ T = ( · ↾ (C × C))
9	6, 8	circgrp 8724	. . . . . 6 ⊢ T ∈ Abel
10		ablgrp 8086	. . . . . 6 ⊢ (T ∈ Abel → T ∈ Grp)
11	9, 10	ax-mp 7	. . . . 5 ⊢ T ∈ Grp
12		shftefif1o.7	. . . . . 6 ⊢ L = {⟨u, v⟩∣(u ∈ C ⋀ v = {⟨x, y⟩∣(x ∈ C ⋀ y = (uTx))})}
13		axmulopr 5253	. . . . . . . 8 ⊢ · :(ℂ × ℂ)–→ℂ
14		fdm 3628	. . . . . . . 8 ⊢ ( · :(ℂ × ℂ)–→ℂ → dom · = (ℂ × ℂ))
15	13, 14	ax-mp 7	. . . . . . 7 ⊢ dom · = (ℂ × ℂ)
16		ssrab2 2129	. . . . . . . 8 ⊢ {w ∈ ℂ∣(abs ‘w) = 1} ⊆ ℂ
17	6, 16	eqsstr 2089	. . . . . . 7 ⊢ C ⊆ ℂ
18	8	resgrprn 8078	. . . . . . 7 ⊢ ((dom · = (ℂ × ℂ) ⋀ T ∈ Grp ⋀ C ⊆ ℂ) → C = ran T)
19	15, 11, 17, 18	mp3an 915	. . . . . 6 ⊢ C = ran T
20	12, 19	grplactf1o 8082	. . . . 5 ⊢ ((T ∈ Grp ⋀ (exp ‘(i · A)) ∈ C) → (L ‘(exp ‘(i · A))):C–1-1-onto→C)
21	11, 20	mpan 694	. . . 4 ⊢ ((exp ‘(i · A)) ∈ C → (L ‘(exp ‘(i · A))):C–1-1-onto→C)
22	7, 21	syl 10	. . 3 ⊢ (A ∈ ℝ → (L ‘(exp ‘(i · A))):C–1-1-onto→C)
23		2re 5940	. . . . . . . 8 ⊢ 2 ∈ ℝ
24		pire 8660	. . . . . . . 8 ⊢ π ∈ ℝ
25	23, 24	remulcl 5322	. . . . . . 7 ⊢ (2 · π) ∈ ℝ
26		axaddrcl 5259	. . . . . . 7 ⊢ ((A ∈ ℝ ⋀ (2 · π) ∈ ℝ) → (A + (2 · π)) ∈ ℝ)
27	25, 26	mpan2 695	. . . . . 6 ⊢ (A ∈ ℝ → (A + (2 · π)) ∈ ℝ)
28		renegclt 5424	. . . . . 6 ⊢ (A ∈ ℝ → -A ∈ ℝ)
29		shftefif1o.5	. . . . . . . 8 ⊢ S = {⟨x, y⟩∣(x ∈ (A[,)(A + (2 · π))) ⋀ y = (x + -A))}
30	29	icoshftf1o 6362	. . . . . . 7 ⊢ ((A ∈ ℝ ⋀ (A + (2 · π)) ∈ ℝ ⋀ -A ∈ ℝ) → S:(A[,)(A + (2 · π)))–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A)))
31		shftefif1o.1	. . . . . . . 8 ⊢ D = (A[,)(A + (2 · π)))
32		f1oeq2 3682	. . . . . . . 8 ⊢ (D = (A[,)(A + (2 · π))) → (S:D–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A)) ↔ S:(A[,)(A + (2 · π)))–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A))))
33	31, 32	ax-mp 7	. . . . . . 7 ⊢ (S:D–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A)) ↔ S:(A[,)(A + (2 · π)))–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A)))
34	30, 33	sylibr 200	. . . . . 6 ⊢ ((A ∈ ℝ ⋀ (A + (2 · π)) ∈ ℝ ⋀ -A ∈ ℝ) → S:D–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A)))
35	27, 28, 34	mpd3an23 917	. . . . 5 ⊢ (A ∈ ℝ → S:D–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A)))
36		recnt 5300	. . . . . . . 8 ⊢ (A ∈ ℝ → A ∈ ℂ)
37		negidt 5366	. . . . . . . 8 ⊢ (A ∈ ℂ → (A + -A) = 0)
38	36, 37	syl 10	. . . . . . 7 ⊢ (A ∈ ℝ → (A + -A) = 0)
39		negsubt 5369	. . . . . . . . 9 ⊢ (((A + (2 · π)) ∈ ℂ ⋀ A ∈ ℂ) → ((A + (2 · π)) + -A) = ((A + (2 · π)) − A))
40	27	recnd 5302	. . . . . . . . 9 ⊢ (A ∈ ℝ → (A + (2 · π)) ∈ ℂ)
41	39, 40, 36	sylanc 471	. . . . . . . 8 ⊢ (A ∈ ℝ → ((A + (2 · π)) + -A) = ((A + (2 · π)) − A))
42	25	recn 5301	. . . . . . . . . 10 ⊢ (2 · π) ∈ ℂ
43		pncan2t 5385	. . . . . . . . . 10 ⊢ ((A ∈ ℂ ⋀ (2 · π) ∈ ℂ) → ((A + (2 · π)) − A) = (2 · π))
44	42, 43	mpan2 695	. . . . . . . . 9 ⊢ (A ∈ ℂ → ((A + (2 · π)) − A) = (2 · π))
45	36, 44	syl 10	. . . . . . . 8 ⊢ (A ∈ ℝ → ((A + (2 · π)) − A) = (2 · π))
46	41, 45	eqtrd 1506	. . . . . . 7 ⊢ (A ∈ ℝ → ((A + (2 · π)) + -A) = (2 · π))
47	38, 46	opreq12d 3975	. . . . . 6 ⊢ (A ∈ ℝ → ((A + -A)[,)((A + (2 · π)) + -A)) = (0[,)(2 · π)))
48		f1oeq3 3683	. . . . . 6 ⊢ (((A + -A)[,)((A + (2 · π)) + -A)) = (0[,)(2 · π)) → (S:D–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A)) ↔ S:D–1-1-onto→(0[,)(2 · π))))
49	47, 48	syl 10	. . . . 5 ⊢ (A ∈ ℝ → (S:D–1-1-onto→((A + -A)[,)((A + (2 · π)) + -A)) ↔ S:D–1-1-onto→(0[,)(2 · π))))
50	35, 49	mpbid 195	. . . 4 ⊢ (A ∈ ℝ → S:D–1-1-onto→(0[,)(2 · π)))
51		shftefif1o.4	. . . . . 6 ⊢ F = {⟨x, y⟩∣(x ∈ (0[,)(2 · π)) ⋀ y = (exp ‘(i · x)))}
52	51, 6	efif1o 8717	. . . . 5 ⊢ F:(0[,)(2 · π))–1-1-onto→C
53		f1oco 3704	. . . . 5 ⊢ ((F:(0[,)(2 · π))–1-1-onto→C ⋀ S:D–1-1-onto→(0[,)(2 · π))) → (F ∘ S):D–1-1-onto→C)
54	52, 53	mpan 694	. . . 4 ⊢ (S:D–1-1-onto→(0[,)(2 · π)) → (F ∘ S):D–1-1-onto→C)
55	50, 54	syl 10	. . 3 ⊢ (A ∈ ℝ → (F ∘ S):D–1-1-onto→C)
56	5, 22, 55	sylanc 471	. 2 ⊢ (A ∈ ℝ → H:D–1-1-onto→C)
57		opreq2 3966	. . . . . . . . 9 ⊢ (x = z → (i · x) = (i · z))
58	57	fveq2d 3725	. . . . . . . 8 ⊢ (x = z → (exp ‘(i · x)) = (exp ‘(i · z)))
59		shftefif1o.2	. . . . . . . 8 ⊢ G = {⟨x, y⟩∣(x ∈ D ⋀ y = (exp ‘(i · x)))}
60		fvex 3729	. . . . . . . 8 ⊢ (exp ‘(i · z)) ∈ V
61	58, 59, 60	fvopab4 3777	. . . . . . 7 ⊢ (z ∈ D → (G ‘z) = (exp ‘(i · z)))
62	61	adantl 388	. . . . . 6 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (G ‘z) = (exp ‘(i · z)))
63		fvco3 3773	. . . . . . . . . . . 12 ⊢ ((Fun (L ‘(exp ‘(i · A))) ⋀ (F ∘ S):D–→C ⋀ z ∈ D) → (((L ‘(exp ‘(i · A))) ∘ (F ∘ S)) ‘z) = ((L ‘(exp ‘(i · A))) ‘((F ∘ S) ‘z)))
64	63	3expa 832	. . . . . . . . . . 11 ⊢ (((Fun (L ‘(exp ‘(i · A))) ⋀ (F ∘ S):D–→C) ⋀ z ∈ D) → (((L ‘(exp ‘(i · A))) ∘ (F ∘ S)) ‘z) = ((L ‘(exp ‘(i · A))) ‘((F ∘ S) ‘z)))
65		f1ofun 3688	. . . . . . . . . . . . 13 ⊢ ((L ‘(exp ‘(i · A))):C–1-1-onto→C → Fun (L ‘(exp ‘(i · A))))
66	22, 65	syl 10	. . . . . . . . . . . 12 ⊢ (A ∈ ℝ → Fun (L ‘(exp ‘(i · A))))
67		f1of 3686	. . . . . . . . . . . . 13 ⊢ ((F ∘ S):D–1-1-onto→C → (F ∘ S):D–→C)
68	55, 67	syl 10	. . . . . . . . . . . 12 ⊢ (A ∈ ℝ → (F ∘ S):D–→C)
69	66, 68	jca 288	. . . . . . . . . . 11 ⊢ (A ∈ ℝ → (Fun (L ‘(exp ‘(i · A))) ⋀ (F ∘ S):D–→C))
70	64, 69	sylan 448	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (((L ‘(exp ‘(i · A))) ∘ (F ∘ S)) ‘z) = ((L ‘(exp ‘(i · A))) ‘((F ∘ S) ‘z)))
71	2	fveq1i 3722	. . . . . . . . . 10 ⊢ (H ‘z) = (((L ‘(exp ‘(i · A))) ∘ (F ∘ S)) ‘z)
72	70, 71	syl5eq 1518	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (H ‘z) = ((L ‘(exp ‘(i · A))) ‘((F ∘ S) ‘z)))
73		f1ofun 3688	. . . . . . . . . . . . 13 ⊢ (F:(0[,)(2 · π))–1-1-onto→C → Fun F)
74	52, 73	ax-mp 7	. . . . . . . . . . . 12 ⊢ Fun F
75		fvco3 3773	. . . . . . . . . . . 12 ⊢ ((Fun F ⋀ S:D–→(0[,)(2 · π)) ⋀ z ∈ D) → ((F ∘ S) ‘z) = (F ‘(S ‘z)))
76	74, 75	mp3an1 902	. . . . . . . . . . 11 ⊢ ((S:D–→(0[,)(2 · π)) ⋀ z ∈ D) → ((F ∘ S) ‘z) = (F ‘(S ‘z)))
77		f1of 3686	. . . . . . . . . . . 12 ⊢ (S:D–1-1-onto→(0[,)(2 · π)) → S:D–→(0[,)(2 · π)))
78	50, 77	syl 10	. . . . . . . . . . 11 ⊢ (A ∈ ℝ → S:D–→(0[,)(2 · π)))
79	76, 78	sylan 448	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → ((F ∘ S) ‘z) = (F ‘(S ‘z)))
80	79	fveq2d 3725	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → ((L ‘(exp ‘(i · A))) ‘((F ∘ S) ‘z)) = ((L ‘(exp ‘(i · A))) ‘(F ‘(S ‘z))))
81	72, 80	eqtrd 1506	. . . . . . . 8 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (H ‘z) = ((L ‘(exp ‘(i · A))) ‘(F ‘(S ‘z))))
82	31	eleq2i 1537	. . . . . . . . . . . . . 14 ⊢ (z ∈ D ↔ z ∈ (A[,)(A + (2 · π))))
83		opreq1 3965	. . . . . . . . . . . . . . 15 ⊢ (x = z → (x + -A) = (z + -A))
84		oprex 3980	. . . . . . . . . . . . . . 15 ⊢ (z + -A) ∈ V
85	83, 29, 84	fvopab4 3777	. . . . . . . . . . . . . 14 ⊢ (z ∈ (A[,)(A + (2 · π))) → (S ‘z) = (z + -A))
86	82, 85	sylbi 199	. . . . . . . . . . . . 13 ⊢ (z ∈ D → (S ‘z) = (z + -A))
87	86	adantl 388	. . . . . . . . . . . 12 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (S ‘z) = (z + -A))
88		negsubt 5369	. . . . . . . . . . . . 13 ⊢ ((z ∈ ℂ ⋀ A ∈ ℂ) → (z + -A) = (z − A))
89		elico2t 6341	. . . . . . . . . . . . . . . . . 18 ⊢ ((A ∈ ℝ ⋀ (A + (2 · π)) ∈ ℝ) → (z ∈ (A[,)(A + (2 · π))) ↔ (z ∈ ℝ ⋀ A ≤ z ⋀ z < (A + (2 · π)))))
90	27, 89	mpdan 703	. . . . . . . . . . . . . . . . 17 ⊢ (A ∈ ℝ → (z ∈ (A[,)(A + (2 · π))) ↔ (z ∈ ℝ ⋀ A ≤ z ⋀ z < (A + (2 · π)))))
91	90, 82	syl5bb 531	. . . . . . . . . . . . . . . 16 ⊢ (A ∈ ℝ → (z ∈ D ↔ (z ∈ ℝ ⋀ A ≤ z ⋀ z < (A + (2 · π)))))
92	91	biimpa 416	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (z ∈ ℝ ⋀ A ≤ z ⋀ z < (A + (2 · π))))
93	92	3simp1d 793	. . . . . . . . . . . . . 14 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → z ∈ ℝ)
94	93	recnd 5302	. . . . . . . . . . . . 13 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → z ∈ ℂ)
95	36	adantr 389	. . . . . . . . . . . . 13 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → A ∈ ℂ)
96	88, 94, 95	sylanc 471	. . . . . . . . . . . 12 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (z + -A) = (z − A))
97	87, 96	eqtrd 1506	. . . . . . . . . . 11 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (S ‘z) = (z − A))
98	97	fveq2d 3725	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (F ‘(S ‘z)) = (F ‘(z − A)))
99		icoshft 6359	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ ℝ ⋀ (A + (2 · π)) ∈ ℝ ⋀ -A ∈ ℝ) → (z ∈ (A[,)(A + (2 · π))) → (z + -A) ∈ ((A + -A)[,)((A + (2 · π)) + -A))))
100	27, 28, 99	mpd3an23 917	. . . . . . . . . . . . . 14 ⊢ (A ∈ ℝ → (z ∈ (A[,)(A + (2 · π))) → (z + -A) ∈ ((A + -A)[,)((A + (2 · π)) + -A))))
101	100, 82	syl5ib 206	. . . . . . . . . . . . 13 ⊢ (A ∈ ℝ → (z ∈ D → (z + -A) ∈ ((A + -A)[,)((A + (2 · π)) + -A))))
102	101	imp 350	. . . . . . . . . . . 12 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (z + -A) ∈ ((A + -A)[,)((A + (2 · π)) + -A)))
103	47	adantr 389	. . . . . . . . . . . . 13 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → ((A + -A)[,)((A + (2 · π)) + -A)) = (0[,)(2 · π)))
104	96, 103	eleq12d 1541	. . . . . . . . . . . 12 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → ((z + -A) ∈ ((A + -A)[,)((A + (2 · π)) + -A)) ↔ (z − A) ∈ (0[,)(2 · π))))
105	102, 104	mpbid 195	. . . . . . . . . . 11 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (z − A) ∈ (0[,)(2 · π)))
106		opreq2 3966	. . . . . . . . . . . . 13 ⊢ (x = (z − A) → (i · x) = (i · (z − A)))
107	106	fveq2d 3725	. . . . . . . . . . . 12 ⊢ (x = (z − A) → (exp ‘(i · x)) = (exp ‘(i · (z − A))))
108		fvex 3729	. . . . . . . . . . . 12 ⊢ (exp ‘(i · (z − A))) ∈ V
109	107, 51, 108	fvopab4 3777	. . . . . . . . . . 11 ⊢ ((z − A) ∈ (0[,)(2 · π)) → (F ‘(z − A)) = (exp ‘(i · (z − A))))
110	105, 109	syl 10	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (F ‘(z − A)) = (exp ‘(i · (z − A))))
111	98, 110	eqtrd 1506	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (F ‘(S ‘z)) = (exp ‘(i · (z − A))))
112	111	fveq2d 3725	. . . . . . . 8 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → ((L ‘(exp ‘(i · A))) ‘(F ‘(S ‘z))) = ((L ‘(exp ‘(i · A))) ‘(exp ‘(i · (z − A)))))
113	12, 19	grplactval 8081	. . . . . . . . . . 11 ⊢ ((T ∈ Grp ⋀ (exp ‘(i · A)) ∈ C ⋀ (exp ‘(i · (z − A))) ∈ C) → ((L ‘(exp ‘(i · A))) ‘(exp ‘(i · (z − A)))) = ((exp ‘(i · A))T(exp ‘(i · (z − A)))))
114	11, 113	mp3an1 902	. . . . . . . . . 10 ⊢ (((exp ‘(i · A)) ∈ C ⋀ (exp ‘(i · (z − A))) ∈ C) → ((L ‘(exp ‘(i · A))) ‘(exp ‘(i · (z − A)))) = ((exp ‘(i · A))T(exp ‘(i · (z − A)))))
115		oprvalres 4030	. . . . . . . . . . 11 ⊢ (((exp ‘(i · A)) ∈ C ⋀ (exp ‘(i · (z − A))) ∈ C) → ((exp ‘(i · A))( · ↾ (C × C))(exp ‘(i · (z − A)))) = ((exp ‘(i · A)) · (exp ‘(i · (z − A)))))
116	8	opreqi 3971	. . . . . . . . . . 11 ⊢ ((exp ‘(i · A))T(exp ‘(i · (z − A)))) = ((exp ‘(i · A))( · ↾ (C × C))(exp ‘(i · (z − A))))
117	115, 116	syl5eq 1518	. . . . . . . . . 10 ⊢ (((exp ‘(i · A)) ∈ C ⋀ (exp ‘(i · (z − A))) ∈ C) → ((exp ‘(i · A))T(exp ‘(i · (z − A)))) = ((exp ‘(i · A)) · (exp ‘(i · (z − A)))))
118	114, 117	eqtrd 1506	. . . . . . . . 9 ⊢ (((exp ‘(i · A)) ∈ C ⋀ (exp ‘(i · (z − A))) ∈ C) → ((L ‘(exp ‘(i · A))) ‘(exp ‘(i · (z − A)))) = ((exp ‘(i · A)) · (exp ‘(i · (z − A)))))
119	7	adantr 389	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (exp ‘(i · A)) ∈ C)
120		resubclt 5425	. . . . . . . . . . 11 ⊢ ((z ∈ ℝ ⋀ A ∈ ℝ) → (z − A) ∈ ℝ)
121		pm3.26 319	. . . . . . . . . . 11 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → A ∈ ℝ)
122	120, 93, 121	sylanc 471	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (z − A) ∈ ℝ)
123	6	efielcirc 8723	. . . . . . . . . 10 ⊢ ((z − A) ∈ ℝ → (exp ‘(i · (z − A))) ∈ C)
124	122, 123	syl 10	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (exp ‘(i · (z − A))) ∈ C)
125	118, 119, 124	sylanc 471	. . . . . . . 8 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → ((L ‘(exp ‘(i · A))) ‘(exp ‘(i · (z − A)))) = ((exp ‘(i · A)) · (exp ‘(i · (z − A)))))
126	81, 112, 125	3eqtrd 1510	. . . . . . 7 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (H ‘z) = ((exp ‘(i · A)) · (exp ‘(i · (z − A)))))
127		efaddt 7345	. . . . . . . 8 ⊢ (((i · A) ∈ ℂ ⋀ (i · (z − A)) ∈ ℂ) → (exp ‘((i · A) + (i · (z − A)))) = ((exp ‘(i · A)) · (exp ‘(i · (z − A)))))
128		axicn 5257	. . . . . . . . . . 11 ⊢ i ∈ ℂ
129		axmulcl 5260	. . . . . . . . . . 11 ⊢ ((i ∈ ℂ ⋀ A ∈ ℂ) → (i · A) ∈ ℂ)
130	128, 129	mpan 694	. . . . . . . . . 10 ⊢ (A ∈ ℂ → (i · A) ∈ ℂ)
131	36, 130	syl 10	. . . . . . . . 9 ⊢ (A ∈ ℝ → (i · A) ∈ ℂ)
132	131	adantr 389	. . . . . . . 8 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (i · A) ∈ ℂ)
133	122	recnd 5302	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (z − A) ∈ ℂ)
134		axmulcl 5260	. . . . . . . . . 10 ⊢ ((i ∈ ℂ ⋀ (z − A) ∈ ℂ) → (i · (z − A)) ∈ ℂ)
135	128, 134	mpan 694	. . . . . . . . 9 ⊢ ((z − A) ∈ ℂ → (i · (z − A)) ∈ ℂ)
136	133, 135	syl 10	. . . . . . . 8 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (i · (z − A)) ∈ ℂ)
137	127, 132, 136	sylanc 471	. . . . . . 7 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (exp ‘((i · A) + (i · (z − A)))) = ((exp ‘(i · A)) · (exp ‘(i · (z − A)))))
138		axdistr 5266	. . . . . . . . . . 11 ⊢ ((i ∈ ℂ ⋀ A ∈ ℂ ⋀ (z − A) ∈ ℂ) → (i · (A + (z − A))) = ((i · A) + (i · (z − A))))
139	128, 138	mp3an1 902	. . . . . . . . . 10 ⊢ ((A ∈ ℂ ⋀ (z − A) ∈ ℂ) → (i · (A + (z − A))) = ((i · A) + (i · (z − A))))
140	139, 95, 133	sylanc 471	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (i · (A + (z − A))) = ((i · A) + (i · (z − A))))
141		pncan3t 5364	. . . . . . . . . . 11 ⊢ ((A ∈ ℂ ⋀ z ∈ ℂ) → (A + (z − A)) = z)
142	141, 95, 94	sylanc 471	. . . . . . . . . 10 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (A + (z − A)) = z)
143	142	opreq2d 3973	. . . . . . . . 9 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (i · (A + (z − A))) = (i · z))
144	140, 143	eqtr3d 1508	. . . . . . . 8 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → ((i · A) + (i · (z − A))) = (i · z))
145	144	fveq2d 3725	. . . . . . 7 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (exp ‘((i · A) + (i · (z − A)))) = (exp ‘(i · z)))
146	126, 137, 145	3eqtr2d 1512	. . . . . 6 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (H ‘z) = (exp ‘(i · z)))
147	62, 146	eqtr4d 1509	. . . . 5 ⊢ ((A ∈ ℝ ⋀ z ∈ D) → (G ‘z) = (H ‘z))
148	147	r19.21aiva 1713	. . . 4 ⊢ (A ∈ ℝ → ∀z ∈ D (G ‘z) = (H ‘z))
149		eqid 1475	. . . . 5 ⊢ D = D
150		f1ofn 3687	. . . . . . . 8 ⊢ (H:D–1-1-onto→C → H Fn D)
151	56, 150	syl 10	. . . . . . 7 ⊢ (A ∈ ℝ → H Fn D)
152		fvex 3729	. . . . . . . . 9 ⊢ (exp ‘(i · x)) ∈ V
153	152, 59	fnopab2 3615	. . . . . . . 8 ⊢ G Fn D
154		eqfnfv 3794	. . . . . . . 8 ⊢ ((G Fn D ⋀ H Fn D) → (G = H ↔ (D = D ⋀ ∀z ∈ D (G ‘z) = (H ‘z))))
155	153, 154	mpan 694	. . . . . . 7 ⊢ (H Fn D → (G = H ↔ (D = D ⋀ ∀z ∈ D (G ‘z) = (H ‘z))))
156	151, 155	syl 10	. . . . . 6 ⊢ (A ∈ ℝ → (G = H ↔ (D = D ⋀ ∀z ∈ D (G ‘z) = (H ‘z))))
157	156	biimprd 154	. . . . 5 ⊢ (A ∈ ℝ → ((D = D ⋀ ∀z ∈ D (G ‘z) = (H ‘z)) → G = H))
158	149, 157	mpani 697	. . . 4 ⊢ (A ∈ ℝ → (∀z ∈ D (G ‘z) = (H ‘z) → G = H))
159	148, 158	mpd 26	. . 3 ⊢ (A ∈ ℝ → G = H)
160		f1oeq1 3681	. . 3 ⊢ (G = H → (G:D–1-1-onto→C ↔ H:D–1-1-onto→C))
161	159, 160	syl 10	. 2 ⊢ (A ∈ ℝ → (G:D–1-1-onto→C ↔ H:D–1-1-onto→C))
162	56, 161	mpbird 196	1 ⊢ (A ∈ ℝ → G:D–1-1-onto→C)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 774   = wceq 955   ∈ wcel 957  ∀wral 1644  {crab 1647   ⊆ wss 2045   class class class wbr 2616  {copab 2663   × cxp 3165  dom cdm 3167  ran crn 3168   ↾ cres 3169   ∘ ccom 3171  Fun wfun 3173   Fn wfn 3174  –→wf 3175  –1-1-onto→wf1o 3178   ‘cfv 3179  (class class class)co 3960  ℂcc 5219  ℝcr 5220  0cc0 5221  1c1 5222  ici 5223   + caddc 5224   · cmul 5226   − cmin 5279  -cneg 5280   ≤ cle 5282   < clt 5473  2c2 5922  [,)cico 6314  abscabs 6702  expce 7271  πcpi 7275  Grpcgr 8016  Abelcabl 8083

This theorem is referenced by:  shftefif1o 8726

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-reg 4580  ax-inf2 4612  ax-ac 4731

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-nel 1587  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-sbc 1940  df-csb 2000  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-pss 2053  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2501  df-int 2531  df-iun 2565  df-iin 2566  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-id 2832  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949  df-lim 2950  df-suc 2951  df-om 3129  df-xp 3181  df-rel 3182  df-cnv 3183  df-co 3184  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fun 3189  df-fn 3190  df-f 3191  df-f1 3192  df-fo 3193  df-f1o 3194  df-fv 3195  df-rdg 3929  df-opr 3962  df-oprab 3963  df-1st 4076  df-2nd 4077  df-1o 4130  df-oadd 4132  df-omul 4133  df-er 4258  df-ec 4260  df-qs 4263  df-map 4321  df-en 4364  df-dom 4365  df-sdom 4366  df-sup 4561  df-r1 4630  df-rank 4631  df-ni 4987  df-pli 4988  df-mi 4989  df-lti 4990  df-plpq 5022  df-mpq 5023  df-enq 5024  df-nq 5025  df-plq 5026  df-mq 5027  df-rq 5028  df-ltq 5029  df-1q 5030  df-np 5073  df-1p 5074  df-plp 5075  df-mp 5076  df-ltp 5077  df-plpr 5151  df-mpr 5152  df-enr 5153  df-nr 5154  df-plr 5155  df-mr 5156  df-ltr 5157  df-0r 5158  df-1r 5159  df-m1r 5160  df-c 5227  df-0 5228  df-1 5229  df-i 5230  df-r 5231  df-plus 5232  df-mul 5233  df-lt 5234  df-sub 5343  df-neg 5345  df-pnf 5474  df-mnf 5475  df-xr 5476  df-ltxr 5477  df-le 5478  df-div 5686  df-n 5887  df-2 5931  df-3 5932  df-4 5933  df-5 5934  df-6 5935  df-7 5936  df-8 5937  df-9 5938  df-n0 6061  df-z 6097  df-fl 6186  df-q 6211  df-rp 6236  df-seq1 6263  df-shft 6296  df-ioo 6316  df-ioc 6317