Metamath Proof Explorer

Theorem dchrptlem1

Description: Lemma for dchrpt . (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrpt.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrpt.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrpt.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrpt.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchrpt.1 ⊢ 1 = ( 1r ‘ 𝑍 )
dchrpt.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
dchrpt.n1 ⊢ ( 𝜑 → 𝐴 ≠ 1 )
dchrpt.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchrpt.h ⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
dchrpt.m ⊢ · = ( .g ‘ 𝐻 )
dchrpt.s ⊢ 𝑆 = ( 𝑘 ∈ dom 𝑊 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) )
dchrpt.au ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
dchrpt.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑈 )
dchrpt.2 ⊢ ( 𝜑 → 𝐻 dom DProd 𝑆 )
dchrpt.3 ⊢ ( 𝜑 → ( 𝐻 DProd 𝑆 ) = 𝑈 )
dchrpt.p ⊢ 𝑃 = ( 𝐻 dProj 𝑆 )
dchrpt.o ⊢ 𝑂 = ( od ‘ 𝐻 )
dchrpt.t ⊢ 𝑇 = ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) )
dchrpt.i ⊢ ( 𝜑 → 𝐼 ∈ dom 𝑊 )
dchrpt.4 ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) ≠ 1 )
dchrpt.5 ⊢ 𝑋 = ( 𝑢 ∈ 𝑈 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
Assertion dchrptlem1 ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝐶 ) = ( 𝑇 ↑ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 dchrpt.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrpt.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrpt.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrpt.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
5 dchrpt.1 ⊢ 1 = ( 1r ‘ 𝑍 )
6 dchrpt.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 dchrpt.n1 ⊢ ( 𝜑 → 𝐴 ≠ 1 )
8 dchrpt.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
9 dchrpt.h ⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾s 𝑈 )
10 dchrpt.m ⊢ · = ( .g ‘ 𝐻 )
11 dchrpt.s ⊢ 𝑆 = ( 𝑘 ∈ dom 𝑊 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑊 ‘ 𝑘 ) ) ) )
12 dchrpt.au ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
13 dchrpt.w ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑈 )
14 dchrpt.2 ⊢ ( 𝜑 → 𝐻 dom DProd 𝑆 )
15 dchrpt.3 ⊢ ( 𝜑 → ( 𝐻 DProd 𝑆 ) = 𝑈 )
16 dchrpt.p ⊢ 𝑃 = ( 𝐻 dProj 𝑆 )
17 dchrpt.o ⊢ 𝑂 = ( od ‘ 𝐻 )
18 dchrpt.t ⊢ 𝑇 = ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) )
19 dchrpt.i ⊢ ( 𝜑 → 𝐼 ∈ dom 𝑊 )
20 dchrpt.4 ⊢ ( 𝜑 → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐴 ) ≠ 1 )
21 dchrpt.5 ⊢ 𝑋 = ( 𝑢 ∈ 𝑈 ↦ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
22 fveqeq2 ⊢ ( 𝑢 = 𝐶 → ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ↔ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) )
23 22 anbi1d ⊢ ( 𝑢 = 𝐶 → ( ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ↔ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
24 23 rexbidv ⊢ ( 𝑢 = 𝐶 → ( ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
25 24 iotabidv ⊢ ( 𝑢 = 𝐶 → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
26 iotaex ⊢ ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝑢 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) ∈ V
27 25 21 26 fvmpt3i ⊢ ( 𝐶 ∈ 𝑈 → ( 𝑋 ‘ 𝐶 ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
28 27 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝐶 ) = ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
29 ovex ⊢ ( 𝑇 ↑ 𝑀 ) ∈ V
30 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) )
31 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) )
32 31 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) )
33 30 32 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) )
34 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → 𝜑 )
35 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → 𝑚 ∈ ℤ )
36 31 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → 𝑀 ∈ ℤ )
37 6 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
38 2 zncrng ⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
39 crngring ⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
40 8 9 unitgrp ⊢ ( 𝑍 ∈ Ring → 𝐻 ∈ Grp )
41 37 38 39 40 4syl ⊢ ( 𝜑 → 𝐻 ∈ Grp )
42 41 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝐻 ∈ Grp )
43 wrdf ⊢ ( 𝑊 ∈ Word 𝑈 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑈 )
44 13 43 syl ⊢ ( 𝜑 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝑈 )
45 44 fdmd ⊢ ( 𝜑 → dom 𝑊 = ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
46 19 45 eleqtrd ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
47 44 46 ffvelrnd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 )
48 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 )
49 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑚 ∈ ℤ )
50 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
51 8 9 unitgrpbas ⊢ 𝑈 = ( Base ‘ 𝐻 )
52 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
53 51 17 10 52 odcong ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ↔ ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) )
54 42 48 49 50 53 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ↔ ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) )
55 neg1cn ⊢ - 1 ∈ ℂ
56 2re ⊢ 2 ∈ ℝ
57 2 4 znfi ⊢ ( 𝑁 ∈ ℕ → 𝐵 ∈ Fin )
58 6 57 syl ⊢ ( 𝜑 → 𝐵 ∈ Fin )
59 4 8 unitss ⊢ 𝑈 ⊆ 𝐵
60 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ 𝑈 ⊆ 𝐵 ) → 𝑈 ∈ Fin )
61 58 59 60 sylancl ⊢ ( 𝜑 → 𝑈 ∈ Fin )
62 51 17 odcl2 ⊢ ( ( 𝐻 ∈ Grp ∧ 𝑈 ∈ Fin ∧ ( 𝑊 ‘ 𝐼 ) ∈ 𝑈 ) → ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ )
63 41 61 47 62 syl3anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ )
64 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ )
65 nndivre ⊢ ( ( 2 ∈ ℝ ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ ) → ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ∈ ℝ )
66 56 64 65 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ∈ ℝ )
67 66 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ∈ ℂ )
68 cxpcl ⊢ ( ( - 1 ∈ ℂ ∧ ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ∈ ℂ ) → ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ∈ ℂ )
69 55 67 68 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ∈ ℂ )
70 18 69 eqeltrid ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → 𝑇 ∈ ℂ )
71 55 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → - 1 ∈ ℂ )
72 neg1ne0 ⊢ - 1 ≠ 0
73 72 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → - 1 ≠ 0 )
74 71 73 67 cxpne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ≠ 0 )
75 18 neeq1i ⊢ ( 𝑇 ≠ 0 ↔ ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ≠ 0 )
76 74 75 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → 𝑇 ≠ 0 )
77 zsubcl ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑚 − 𝑀 ) ∈ ℤ )
78 77 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 𝑚 − 𝑀 ) ∈ ℤ )
79 50 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → 𝑀 ∈ ℤ )
80 expaddz ⊢ ( ( ( 𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ) ∧ ( ( 𝑚 − 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑇 ↑ ( ( 𝑚 − 𝑀 ) + 𝑀 ) ) = ( ( 𝑇 ↑ ( 𝑚 − 𝑀 ) ) · ( 𝑇 ↑ 𝑀 ) ) )
81 70 76 78 79 80 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 𝑇 ↑ ( ( 𝑚 − 𝑀 ) + 𝑀 ) ) = ( ( 𝑇 ↑ ( 𝑚 − 𝑀 ) ) · ( 𝑇 ↑ 𝑀 ) ) )
82 49 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → 𝑚 ∈ ℤ )
83 82 zcnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → 𝑚 ∈ ℂ )
84 79 zcnd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → 𝑀 ∈ ℂ )
85 83 84 npcand ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( ( 𝑚 − 𝑀 ) + 𝑀 ) = 𝑚 )
86 85 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 𝑇 ↑ ( ( 𝑚 − 𝑀 ) + 𝑀 ) ) = ( 𝑇 ↑ 𝑚 ) )
87 18 oveq1i ⊢ ( 𝑇 ↑ ( 𝑚 − 𝑀 ) ) = ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ ( 𝑚 − 𝑀 ) )
88 root1eq1 ⊢ ( ( ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∈ ℕ ∧ ( 𝑚 − 𝑀 ) ∈ ℤ ) → ( ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ ( 𝑚 − 𝑀 ) ) = 1 ↔ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) )
89 63 77 88 syl2an ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ ( 𝑚 − 𝑀 ) ) = 1 ↔ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) )
90 89 biimpar ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( ( - 1 ↑𝑐 ( 2 / ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ) ) ↑ ( 𝑚 − 𝑀 ) ) = 1 )
91 87 90 syl5eq ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 𝑇 ↑ ( 𝑚 − 𝑀 ) ) = 1 )
92 91 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( ( 𝑇 ↑ ( 𝑚 − 𝑀 ) ) · ( 𝑇 ↑ 𝑀 ) ) = ( 1 · ( 𝑇 ↑ 𝑀 ) ) )
93 70 76 79 expclzd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 𝑇 ↑ 𝑀 ) ∈ ℂ )
94 93 mulid2d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 1 · ( 𝑇 ↑ 𝑀 ) ) = ( 𝑇 ↑ 𝑀 ) )
95 92 94 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( ( 𝑇 ↑ ( 𝑚 − 𝑀 ) ) · ( 𝑇 ↑ 𝑀 ) ) = ( 𝑇 ↑ 𝑀 ) )
96 81 86 95 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) ∧ ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) ) → ( 𝑇 ↑ 𝑚 ) = ( 𝑇 ↑ 𝑀 ) )
97 96 ex ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑂 ‘ ( 𝑊 ‘ 𝐼 ) ) ∥ ( 𝑚 − 𝑀 ) → ( 𝑇 ↑ 𝑚 ) = ( 𝑇 ↑ 𝑀 ) ) )
98 54 97 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) → ( 𝑇 ↑ 𝑚 ) = ( 𝑇 ↑ 𝑀 ) ) )
99 34 35 36 98 syl12anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → ( ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) → ( 𝑇 ↑ 𝑚 ) = ( 𝑇 ↑ 𝑀 ) ) )
100 33 99 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → ( 𝑇 ↑ 𝑚 ) = ( 𝑇 ↑ 𝑀 ) )
101 100 eqeq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → ( ℎ = ( 𝑇 ↑ 𝑚 ) ↔ ℎ = ( 𝑇 ↑ 𝑀 ) ) )
102 101 biimpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ) → ( ℎ = ( 𝑇 ↑ 𝑚 ) → ℎ = ( 𝑇 ↑ 𝑀 ) ) )
103 102 expimpd ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ 𝑚 ∈ ℤ ) → ( ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) → ℎ = ( 𝑇 ↑ 𝑀 ) ) )
104 103 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) → ℎ = ( 𝑇 ↑ 𝑀 ) ) )
105 oveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) )
106 105 eqeq2d ⊢ ( 𝑚 = 𝑀 → ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ↔ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) )
107 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 𝑇 ↑ 𝑚 ) = ( 𝑇 ↑ 𝑀 ) )
108 107 eqeq2d ⊢ ( 𝑚 = 𝑀 → ( ℎ = ( 𝑇 ↑ 𝑚 ) ↔ ℎ = ( 𝑇 ↑ 𝑀 ) ) )
109 106 108 anbi12d ⊢ ( 𝑚 = 𝑀 → ( ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ↔ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑀 ) ) ) )
110 109 rspcev ⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑀 ) ) ) → ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) )
111 110 expr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) → ( ℎ = ( 𝑇 ↑ 𝑀 ) → ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
112 111 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ℎ = ( 𝑇 ↑ 𝑀 ) → ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) )
113 104 112 impbid ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ↔ ℎ = ( 𝑇 ↑ 𝑀 ) ) )
114 113 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ ( 𝑇 ↑ 𝑀 ) ∈ V ) → ( ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ↔ ℎ = ( 𝑇 ↑ 𝑀 ) ) )
115 114 iota5 ⊢ ( ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) ∧ ( 𝑇 ↑ 𝑀 ) ∈ V ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) = ( 𝑇 ↑ 𝑀 ) )
116 29 115 mpan2 ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( ℩ ℎ ∃ 𝑚 ∈ ℤ ( ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑚 · ( 𝑊 ‘ 𝐼 ) ) ∧ ℎ = ( 𝑇 ↑ 𝑚 ) ) ) = ( 𝑇 ↑ 𝑀 ) )
117 28 116 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ 𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃 ‘ 𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊 ‘ 𝐼 ) ) ) ) → ( 𝑋 ‘ 𝐶 ) = ( 𝑇 ↑ 𝑀 ) )