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 ) ) |