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 ffvelcdmd 
 |-  ( 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 eqtrid 
 |-  ( ( ( 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 mullidd 
 |-  ( ( ( 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 ) )