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 ( ( ( 𝜑𝐶𝑈 ) ∧ ( 𝑀 ∈ ℤ ∧ ( ( 𝑃𝐼 ) ‘ 𝐶 ) = ( 𝑀 · ( 𝑊𝐼 ) ) ) ) → ( 𝑋𝐶 ) = ( 𝑇𝑀 ) )