Metamath Proof Explorer


Theorem dchrptlem1

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

Ref Expression
Hypotheses dchrpt.g
|- G = ( DChr ` N )
dchrpt.z
|- Z = ( Z/nZ ` N )
dchrpt.d
|- D = ( Base ` G )
dchrpt.b
|- B = ( Base ` Z )
dchrpt.1
|- .1. = ( 1r ` Z )
dchrpt.n
|- ( ph -> N e. NN )
dchrpt.n1
|- ( ph -> A =/= .1. )
dchrpt.u
|- U = ( Unit ` Z )
dchrpt.h
|- H = ( ( mulGrp ` Z ) |`s U )
dchrpt.m
|- .x. = ( .g ` H )
dchrpt.s
|- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )
dchrpt.au
|- ( ph -> A e. U )
dchrpt.w
|- ( ph -> W e. Word U )
dchrpt.2
|- ( ph -> H dom DProd S )
dchrpt.3
|- ( ph -> ( H DProd S ) = U )
dchrpt.p
|- P = ( H dProj S )
dchrpt.o
|- O = ( od ` H )
dchrpt.t
|- T = ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) )
dchrpt.i
|- ( ph -> I e. dom W )
dchrpt.4
|- ( ph -> ( ( P ` I ) ` A ) =/= .1. )
dchrpt.5
|- X = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
Assertion dchrptlem1
|- ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( X ` C ) = ( T ^ M ) )

Proof

Step Hyp Ref Expression
1 dchrpt.g
 |-  G = ( DChr ` N )
2 dchrpt.z
 |-  Z = ( Z/nZ ` N )
3 dchrpt.d
 |-  D = ( Base ` G )
4 dchrpt.b
 |-  B = ( Base ` Z )
5 dchrpt.1
 |-  .1. = ( 1r ` Z )
6 dchrpt.n
 |-  ( ph -> N e. NN )
7 dchrpt.n1
 |-  ( ph -> A =/= .1. )
8 dchrpt.u
 |-  U = ( Unit ` Z )
9 dchrpt.h
 |-  H = ( ( mulGrp ` Z ) |`s U )
10 dchrpt.m
 |-  .x. = ( .g ` H )
11 dchrpt.s
 |-  S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )
12 dchrpt.au
 |-  ( ph -> A e. U )
13 dchrpt.w
 |-  ( ph -> W e. Word U )
14 dchrpt.2
 |-  ( ph -> H dom DProd S )
15 dchrpt.3
 |-  ( ph -> ( H DProd S ) = U )
16 dchrpt.p
 |-  P = ( H dProj S )
17 dchrpt.o
 |-  O = ( od ` H )
18 dchrpt.t
 |-  T = ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) )
19 dchrpt.i
 |-  ( ph -> I e. dom W )
20 dchrpt.4
 |-  ( ph -> ( ( P ` I ) ` A ) =/= .1. )
21 dchrpt.5
 |-  X = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
22 fveqeq2
 |-  ( u = C -> ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) <-> ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) )
23 22 anbi1d
 |-  ( u = C -> ( ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) <-> ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
24 23 rexbidv
 |-  ( u = C -> ( E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) <-> E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
25 24 iotabidv
 |-  ( u = C -> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) = ( iota h E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
26 iotaex
 |-  ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) e. _V
27 25 21 26 fvmpt3i
 |-  ( C e. U -> ( X ` C ) = ( iota h E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
28 27 ad2antlr
 |-  ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( X ` C ) = ( iota h E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
29 ovex
 |-  ( T ^ M ) e. _V
30 simpr
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) )
31 simpllr
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) )
32 31 simprd
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) )
33 30 32 eqtr3d
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ( m .x. ( W ` I ) ) = ( M .x. ( W ` I ) ) )
34 simp-4l
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ph )
35 simplr
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> m e. ZZ )
36 31 simpld
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> M e. ZZ )
37 6 nnnn0d
 |-  ( ph -> N e. NN0 )
38 2 zncrng
 |-  ( N e. NN0 -> Z e. CRing )
39 crngring
 |-  ( Z e. CRing -> Z e. Ring )
40 8 9 unitgrp
 |-  ( Z e. Ring -> H e. Grp )
41 37 38 39 40 4syl
 |-  ( ph -> H e. Grp )
42 41 adantr
 |-  ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) -> H e. Grp )
43 wrdf
 |-  ( W e. Word U -> W : ( 0 ..^ ( # ` W ) ) --> U )
44 13 43 syl
 |-  ( ph -> W : ( 0 ..^ ( # ` W ) ) --> U )
45 44 fdmd
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
46 19 45 eleqtrd
 |-  ( ph -> I e. ( 0 ..^ ( # ` W ) ) )
47 44 46 ffvelrnd
 |-  ( ph -> ( W ` I ) e. U )
48 47 adantr
 |-  ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) -> ( W ` I ) e. U )
49 simprl
 |-  ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) -> m e. ZZ )
50 simprr
 |-  ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) -> M e. ZZ )
51 8 9 unitgrpbas
 |-  U = ( Base ` H )
52 eqid
 |-  ( 0g ` H ) = ( 0g ` H )
53 51 17 10 52 odcong
 |-  ( ( H e. Grp /\ ( W ` I ) e. U /\ ( m e. ZZ /\ M e. ZZ ) ) -> ( ( O ` ( W ` I ) ) || ( m - M ) <-> ( m .x. ( W ` I ) ) = ( M .x. ( W ` I ) ) ) )
54 42 48 49 50 53 syl112anc
 |-  ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) -> ( ( O ` ( W ` I ) ) || ( m - M ) <-> ( m .x. ( W ` I ) ) = ( M .x. ( W ` I ) ) ) )
55 neg1cn
 |-  -u 1 e. CC
56 2re
 |-  2 e. RR
57 2 4 znfi
 |-  ( N e. NN -> B e. Fin )
58 6 57 syl
 |-  ( ph -> B e. Fin )
59 4 8 unitss
 |-  U C_ B
60 ssfi
 |-  ( ( B e. Fin /\ U C_ B ) -> U e. Fin )
61 58 59 60 sylancl
 |-  ( ph -> U e. Fin )
62 51 17 odcl2
 |-  ( ( H e. Grp /\ U e. Fin /\ ( W ` I ) e. U ) -> ( O ` ( W ` I ) ) e. NN )
63 41 61 47 62 syl3anc
 |-  ( ph -> ( O ` ( W ` I ) ) e. NN )
64 63 ad2antrr
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( O ` ( W ` I ) ) e. NN )
65 nndivre
 |-  ( ( 2 e. RR /\ ( O ` ( W ` I ) ) e. NN ) -> ( 2 / ( O ` ( W ` I ) ) ) e. RR )
66 56 64 65 sylancr
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( 2 / ( O ` ( W ` I ) ) ) e. RR )
67 66 recnd
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( 2 / ( O ` ( W ` I ) ) ) e. CC )
68 cxpcl
 |-  ( ( -u 1 e. CC /\ ( 2 / ( O ` ( W ` I ) ) ) e. CC ) -> ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) e. CC )
69 55 67 68 sylancr
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) e. CC )
70 18 69 eqeltrid
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> T e. CC )
71 55 a1i
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> -u 1 e. CC )
72 neg1ne0
 |-  -u 1 =/= 0
73 72 a1i
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> -u 1 =/= 0 )
74 71 73 67 cxpne0d
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) =/= 0 )
75 18 neeq1i
 |-  ( T =/= 0 <-> ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) =/= 0 )
76 74 75 sylibr
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> T =/= 0 )
77 zsubcl
 |-  ( ( m e. ZZ /\ M e. ZZ ) -> ( m - M ) e. ZZ )
78 77 ad2antlr
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( m - M ) e. ZZ )
79 50 adantr
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> M e. ZZ )
80 expaddz
 |-  ( ( ( T e. CC /\ T =/= 0 ) /\ ( ( m - M ) e. ZZ /\ M e. ZZ ) ) -> ( T ^ ( ( m - M ) + M ) ) = ( ( T ^ ( m - M ) ) x. ( T ^ M ) ) )
81 70 76 78 79 80 syl22anc
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( T ^ ( ( m - M ) + M ) ) = ( ( T ^ ( m - M ) ) x. ( T ^ M ) ) )
82 49 adantr
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> m e. ZZ )
83 82 zcnd
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> m e. CC )
84 79 zcnd
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> M e. CC )
85 83 84 npcand
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( ( m - M ) + M ) = m )
86 85 oveq2d
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( T ^ ( ( m - M ) + M ) ) = ( T ^ m ) )
87 18 oveq1i
 |-  ( T ^ ( m - M ) ) = ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ ( m - M ) )
88 root1eq1
 |-  ( ( ( O ` ( W ` I ) ) e. NN /\ ( m - M ) e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ ( m - M ) ) = 1 <-> ( O ` ( W ` I ) ) || ( m - M ) ) )
89 63 77 88 syl2an
 |-  ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) -> ( ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ ( m - M ) ) = 1 <-> ( O ` ( W ` I ) ) || ( m - M ) ) )
90 89 biimpar
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ ( m - M ) ) = 1 )
91 87 90 syl5eq
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( T ^ ( m - M ) ) = 1 )
92 91 oveq1d
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( ( T ^ ( m - M ) ) x. ( T ^ M ) ) = ( 1 x. ( T ^ M ) ) )
93 70 76 79 expclzd
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( T ^ M ) e. CC )
94 93 mulid2d
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( 1 x. ( T ^ M ) ) = ( T ^ M ) )
95 92 94 eqtrd
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( ( T ^ ( m - M ) ) x. ( T ^ M ) ) = ( T ^ M ) )
96 81 86 95 3eqtr3d
 |-  ( ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) /\ ( O ` ( W ` I ) ) || ( m - M ) ) -> ( T ^ m ) = ( T ^ M ) )
97 96 ex
 |-  ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) -> ( ( O ` ( W ` I ) ) || ( m - M ) -> ( T ^ m ) = ( T ^ M ) ) )
98 54 97 sylbird
 |-  ( ( ph /\ ( m e. ZZ /\ M e. ZZ ) ) -> ( ( m .x. ( W ` I ) ) = ( M .x. ( W ` I ) ) -> ( T ^ m ) = ( T ^ M ) ) )
99 34 35 36 98 syl12anc
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ( ( m .x. ( W ` I ) ) = ( M .x. ( W ` I ) ) -> ( T ^ m ) = ( T ^ M ) ) )
100 33 99 mpd
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ( T ^ m ) = ( T ^ M ) )
101 100 eqeq2d
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ( h = ( T ^ m ) <-> h = ( T ^ M ) ) )
102 101 biimpd
 |-  ( ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) /\ ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) ) -> ( h = ( T ^ m ) -> h = ( T ^ M ) ) )
103 102 expimpd
 |-  ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ m e. ZZ ) -> ( ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) -> h = ( T ^ M ) ) )
104 103 rexlimdva
 |-  ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) -> h = ( T ^ M ) ) )
105 oveq1
 |-  ( m = M -> ( m .x. ( W ` I ) ) = ( M .x. ( W ` I ) ) )
106 105 eqeq2d
 |-  ( m = M -> ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) <-> ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) )
107 oveq2
 |-  ( m = M -> ( T ^ m ) = ( T ^ M ) )
108 107 eqeq2d
 |-  ( m = M -> ( h = ( T ^ m ) <-> h = ( T ^ M ) ) )
109 106 108 anbi12d
 |-  ( m = M -> ( ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) <-> ( ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) /\ h = ( T ^ M ) ) ) )
110 109 rspcev
 |-  ( ( M e. ZZ /\ ( ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) /\ h = ( T ^ M ) ) ) -> E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) )
111 110 expr
 |-  ( ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) -> ( h = ( T ^ M ) -> E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
112 111 adantl
 |-  ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( h = ( T ^ M ) -> E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
113 104 112 impbid
 |-  ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) <-> h = ( T ^ M ) ) )
114 113 adantr
 |-  ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ ( T ^ M ) e. _V ) -> ( E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) <-> h = ( T ^ M ) ) )
115 114 iota5
 |-  ( ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) /\ ( T ^ M ) e. _V ) -> ( iota h E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) = ( T ^ M ) )
116 29 115 mpan2
 |-  ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( iota h E. m e. ZZ ( ( ( P ` I ) ` C ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) = ( T ^ M ) )
117 28 116 eqtrd
 |-  ( ( ( ph /\ C e. U ) /\ ( M e. ZZ /\ ( ( P ` I ) ` C ) = ( M .x. ( W ` I ) ) ) ) -> ( X ` C ) = ( T ^ M ) )