Step |
Hyp |
Ref |
Expression |
1 |
|
cycpmco2.c |
|- M = ( toCyc ` D ) |
2 |
|
cycpmco2.s |
|- S = ( SymGrp ` D ) |
3 |
|
cycpmco2.d |
|- ( ph -> D e. V ) |
4 |
|
cycpmco2.w |
|- ( ph -> W e. dom M ) |
5 |
|
cycpmco2.i |
|- ( ph -> I e. ( D \ ran W ) ) |
6 |
|
cycpmco2.j |
|- ( ph -> J e. ran W ) |
7 |
|
cycpmco2.e |
|- E = ( ( `' W ` J ) + 1 ) |
8 |
|
cycpmco2.1 |
|- U = ( W splice <. E , E , <" I "> >. ) |
9 |
|
ssrab2 |
|- { w e. Word D | w : dom w -1-1-> D } C_ Word D |
10 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
11 |
1 2 10
|
tocycf |
|- ( D e. V -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) ) |
12 |
3 11
|
syl |
|- ( ph -> M : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` S ) ) |
13 |
12
|
fdmd |
|- ( ph -> dom M = { w e. Word D | w : dom w -1-1-> D } ) |
14 |
4 13
|
eleqtrd |
|- ( ph -> W e. { w e. Word D | w : dom w -1-1-> D } ) |
15 |
9 14
|
sseldi |
|- ( ph -> W e. Word D ) |
16 |
|
pfxcl |
|- ( W e. Word D -> ( W prefix E ) e. Word D ) |
17 |
15 16
|
syl |
|- ( ph -> ( W prefix E ) e. Word D ) |
18 |
5
|
eldifad |
|- ( ph -> I e. D ) |
19 |
18
|
s1cld |
|- ( ph -> <" I "> e. Word D ) |
20 |
|
ccatcl |
|- ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ( ( W prefix E ) ++ <" I "> ) e. Word D ) |
21 |
17 19 20
|
syl2anc |
|- ( ph -> ( ( W prefix E ) ++ <" I "> ) e. Word D ) |
22 |
|
swrdcl |
|- ( W e. Word D -> ( W substr <. E , ( # ` W ) >. ) e. Word D ) |
23 |
15 22
|
syl |
|- ( ph -> ( W substr <. E , ( # ` W ) >. ) e. Word D ) |
24 |
|
id |
|- ( w = W -> w = W ) |
25 |
|
dmeq |
|- ( w = W -> dom w = dom W ) |
26 |
|
eqidd |
|- ( w = W -> D = D ) |
27 |
24 25 26
|
f1eq123d |
|- ( w = W -> ( w : dom w -1-1-> D <-> W : dom W -1-1-> D ) ) |
28 |
27
|
elrab |
|- ( W e. { w e. Word D | w : dom w -1-1-> D } <-> ( W e. Word D /\ W : dom W -1-1-> D ) ) |
29 |
14 28
|
sylib |
|- ( ph -> ( W e. Word D /\ W : dom W -1-1-> D ) ) |
30 |
29
|
simprd |
|- ( ph -> W : dom W -1-1-> D ) |
31 |
|
f1cnv |
|- ( W : dom W -1-1-> D -> `' W : ran W -1-1-onto-> dom W ) |
32 |
|
f1of |
|- ( `' W : ran W -1-1-onto-> dom W -> `' W : ran W --> dom W ) |
33 |
30 31 32
|
3syl |
|- ( ph -> `' W : ran W --> dom W ) |
34 |
33 6
|
ffvelrnd |
|- ( ph -> ( `' W ` J ) e. dom W ) |
35 |
|
wrddm |
|- ( W e. Word D -> dom W = ( 0 ..^ ( # ` W ) ) ) |
36 |
15 35
|
syl |
|- ( ph -> dom W = ( 0 ..^ ( # ` W ) ) ) |
37 |
34 36
|
eleqtrd |
|- ( ph -> ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) ) |
38 |
|
fzofzp1 |
|- ( ( `' W ` J ) e. ( 0 ..^ ( # ` W ) ) -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) ) |
39 |
37 38
|
syl |
|- ( ph -> ( ( `' W ` J ) + 1 ) e. ( 0 ... ( # ` W ) ) ) |
40 |
7 39
|
eqeltrid |
|- ( ph -> E e. ( 0 ... ( # ` W ) ) ) |
41 |
15 30 40
|
pfxf1 |
|- ( ph -> ( W prefix E ) : dom ( W prefix E ) -1-1-> D ) |
42 |
18
|
s1f1 |
|- ( ph -> <" I "> : dom <" I "> -1-1-> D ) |
43 |
|
s1rn |
|- ( I e. D -> ran <" I "> = { I } ) |
44 |
18 43
|
syl |
|- ( ph -> ran <" I "> = { I } ) |
45 |
44
|
ineq2d |
|- ( ph -> ( ran ( W prefix E ) i^i ran <" I "> ) = ( ran ( W prefix E ) i^i { I } ) ) |
46 |
|
pfxrn2 |
|- ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) ) -> ran ( W prefix E ) C_ ran W ) |
47 |
15 40 46
|
syl2anc |
|- ( ph -> ran ( W prefix E ) C_ ran W ) |
48 |
47
|
ssrind |
|- ( ph -> ( ran ( W prefix E ) i^i { I } ) C_ ( ran W i^i { I } ) ) |
49 |
5
|
eldifbd |
|- ( ph -> -. I e. ran W ) |
50 |
|
disjsn |
|- ( ( ran W i^i { I } ) = (/) <-> -. I e. ran W ) |
51 |
49 50
|
sylibr |
|- ( ph -> ( ran W i^i { I } ) = (/) ) |
52 |
48 51
|
sseqtrd |
|- ( ph -> ( ran ( W prefix E ) i^i { I } ) C_ (/) ) |
53 |
|
ss0 |
|- ( ( ran ( W prefix E ) i^i { I } ) C_ (/) -> ( ran ( W prefix E ) i^i { I } ) = (/) ) |
54 |
52 53
|
syl |
|- ( ph -> ( ran ( W prefix E ) i^i { I } ) = (/) ) |
55 |
45 54
|
eqtrd |
|- ( ph -> ( ran ( W prefix E ) i^i ran <" I "> ) = (/) ) |
56 |
3 17 19 41 42 55
|
ccatf1 |
|- ( ph -> ( ( W prefix E ) ++ <" I "> ) : dom ( ( W prefix E ) ++ <" I "> ) -1-1-> D ) |
57 |
|
lencl |
|- ( W e. Word D -> ( # ` W ) e. NN0 ) |
58 |
|
nn0fz0 |
|- ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( 0 ... ( # ` W ) ) ) |
59 |
58
|
biimpi |
|- ( ( # ` W ) e. NN0 -> ( # ` W ) e. ( 0 ... ( # ` W ) ) ) |
60 |
15 57 59
|
3syl |
|- ( ph -> ( # ` W ) e. ( 0 ... ( # ` W ) ) ) |
61 |
15 40 60 30
|
swrdf1 |
|- ( ph -> ( W substr <. E , ( # ` W ) >. ) : dom ( W substr <. E , ( # ` W ) >. ) -1-1-> D ) |
62 |
|
ccatrn |
|- ( ( ( W prefix E ) e. Word D /\ <" I "> e. Word D ) -> ran ( ( W prefix E ) ++ <" I "> ) = ( ran ( W prefix E ) u. ran <" I "> ) ) |
63 |
17 19 62
|
syl2anc |
|- ( ph -> ran ( ( W prefix E ) ++ <" I "> ) = ( ran ( W prefix E ) u. ran <" I "> ) ) |
64 |
63
|
ineq1d |
|- ( ph -> ( ran ( ( W prefix E ) ++ <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ( ran ( W prefix E ) u. ran <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) ) |
65 |
|
indir |
|- ( ( ran ( W prefix E ) u. ran <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) u. ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) ) |
66 |
64 65
|
eqtrdi |
|- ( ph -> ( ran ( ( W prefix E ) ++ <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) u. ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) ) ) |
67 |
|
fz0ssnn0 |
|- ( 0 ... ( # ` W ) ) C_ NN0 |
68 |
67 40
|
sseldi |
|- ( ph -> E e. NN0 ) |
69 |
|
pfxval |
|- ( ( W e. Word D /\ E e. NN0 ) -> ( W prefix E ) = ( W substr <. 0 , E >. ) ) |
70 |
15 68 69
|
syl2anc |
|- ( ph -> ( W prefix E ) = ( W substr <. 0 , E >. ) ) |
71 |
70
|
rneqd |
|- ( ph -> ran ( W prefix E ) = ran ( W substr <. 0 , E >. ) ) |
72 |
71
|
ineq1d |
|- ( ph -> ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ran ( W substr <. 0 , E >. ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) ) |
73 |
|
0elfz |
|- ( E e. NN0 -> 0 e. ( 0 ... E ) ) |
74 |
68 73
|
syl |
|- ( ph -> 0 e. ( 0 ... E ) ) |
75 |
|
elfzuz3 |
|- ( E e. ( 0 ... ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` E ) ) |
76 |
|
eluzfz1 |
|- ( ( # ` W ) e. ( ZZ>= ` E ) -> E e. ( E ... ( # ` W ) ) ) |
77 |
40 75 76
|
3syl |
|- ( ph -> E e. ( E ... ( # ` W ) ) ) |
78 |
|
eluzfz2 |
|- ( ( # ` W ) e. ( ZZ>= ` E ) -> ( # ` W ) e. ( E ... ( # ` W ) ) ) |
79 |
40 75 78
|
3syl |
|- ( ph -> ( # ` W ) e. ( E ... ( # ` W ) ) ) |
80 |
15 74 40 30 77 79
|
swrdrndisj |
|- ( ph -> ( ran ( W substr <. 0 , E >. ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = (/) ) |
81 |
72 80
|
eqtrd |
|- ( ph -> ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = (/) ) |
82 |
|
incom |
|- ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) = ( ran ( W substr <. E , ( # ` W ) >. ) i^i ran <" I "> ) |
83 |
44
|
ineq2d |
|- ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i ran <" I "> ) = ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) ) |
84 |
|
swrdrn2 |
|- ( ( W e. Word D /\ E e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ran ( W substr <. E , ( # ` W ) >. ) C_ ran W ) |
85 |
15 40 60 84
|
syl3anc |
|- ( ph -> ran ( W substr <. E , ( # ` W ) >. ) C_ ran W ) |
86 |
85
|
ssrind |
|- ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) C_ ( ran W i^i { I } ) ) |
87 |
86 51
|
sseqtrd |
|- ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) C_ (/) ) |
88 |
|
ss0 |
|- ( ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) C_ (/) -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) = (/) ) |
89 |
87 88
|
syl |
|- ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i { I } ) = (/) ) |
90 |
83 89
|
eqtrd |
|- ( ph -> ( ran ( W substr <. E , ( # ` W ) >. ) i^i ran <" I "> ) = (/) ) |
91 |
82 90
|
syl5eq |
|- ( ph -> ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) = (/) ) |
92 |
81 91
|
uneq12d |
|- ( ph -> ( ( ran ( W prefix E ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) u. ( ran <" I "> i^i ran ( W substr <. E , ( # ` W ) >. ) ) ) = ( (/) u. (/) ) ) |
93 |
|
unidm |
|- ( (/) u. (/) ) = (/) |
94 |
93
|
a1i |
|- ( ph -> ( (/) u. (/) ) = (/) ) |
95 |
66 92 94
|
3eqtrd |
|- ( ph -> ( ran ( ( W prefix E ) ++ <" I "> ) i^i ran ( W substr <. E , ( # ` W ) >. ) ) = (/) ) |
96 |
3 21 23 56 61 95
|
ccatf1 |
|- ( ph -> ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) : dom ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) -1-1-> D ) |
97 |
|
ovexd |
|- ( ph -> ( ( `' W ` J ) + 1 ) e. _V ) |
98 |
7 97
|
eqeltrid |
|- ( ph -> E e. _V ) |
99 |
|
splval |
|- ( ( W e. dom M /\ ( E e. _V /\ E e. _V /\ <" I "> e. Word D ) ) -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) |
100 |
4 98 98 19 99
|
syl13anc |
|- ( ph -> ( W splice <. E , E , <" I "> >. ) = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) |
101 |
8 100
|
syl5eq |
|- ( ph -> U = ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) |
102 |
101
|
dmeqd |
|- ( ph -> dom U = dom ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) ) |
103 |
|
eqidd |
|- ( ph -> D = D ) |
104 |
101 102 103
|
f1eq123d |
|- ( ph -> ( U : dom U -1-1-> D <-> ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) : dom ( ( ( W prefix E ) ++ <" I "> ) ++ ( W substr <. E , ( # ` W ) >. ) ) -1-1-> D ) ) |
105 |
96 104
|
mpbird |
|- ( ph -> U : dom U -1-1-> D ) |