Step |
Hyp |
Ref |
Expression |
1 |
|
efgval.w |
|- W = ( _I ` Word ( I X. 2o ) ) |
2 |
|
efgval.r |
|- .~ = ( ~FG ` I ) |
3 |
|
efgval2.m |
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) |
4 |
|
efgval2.t |
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) ) |
5 |
|
efgred.d |
|- D = ( W \ U_ x e. W ran ( T ` x ) ) |
6 |
|
efgred.s |
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) ) |
7 |
|
efgredlem.1 |
|- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) |
8 |
|
efgredlem.2 |
|- ( ph -> A e. dom S ) |
9 |
|
efgredlem.3 |
|- ( ph -> B e. dom S ) |
10 |
|
efgredlem.4 |
|- ( ph -> ( S ` A ) = ( S ` B ) ) |
11 |
|
efgredlem.5 |
|- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) ) |
12 |
1 2 3 4 5 6
|
efgsval |
|- ( B e. dom S -> ( S ` B ) = ( B ` ( ( # ` B ) - 1 ) ) ) |
13 |
9 12
|
syl |
|- ( ph -> ( S ` B ) = ( B ` ( ( # ` B ) - 1 ) ) ) |
14 |
1 2 3 4 5 6
|
efgsval |
|- ( A e. dom S -> ( S ` A ) = ( A ` ( ( # ` A ) - 1 ) ) ) |
15 |
8 14
|
syl |
|- ( ph -> ( S ` A ) = ( A ` ( ( # ` A ) - 1 ) ) ) |
16 |
10 15
|
eqtr3d |
|- ( ph -> ( S ` B ) = ( A ` ( ( # ` A ) - 1 ) ) ) |
17 |
13 16
|
eqtr3d |
|- ( ph -> ( B ` ( ( # ` B ) - 1 ) ) = ( A ` ( ( # ` A ) - 1 ) ) ) |
18 |
|
oveq1 |
|- ( ( # ` A ) = 1 -> ( ( # ` A ) - 1 ) = ( 1 - 1 ) ) |
19 |
|
1m1e0 |
|- ( 1 - 1 ) = 0 |
20 |
18 19
|
eqtrdi |
|- ( ( # ` A ) = 1 -> ( ( # ` A ) - 1 ) = 0 ) |
21 |
20
|
fveq2d |
|- ( ( # ` A ) = 1 -> ( A ` ( ( # ` A ) - 1 ) ) = ( A ` 0 ) ) |
22 |
17 21
|
sylan9eq |
|- ( ( ph /\ ( # ` A ) = 1 ) -> ( B ` ( ( # ` B ) - 1 ) ) = ( A ` 0 ) ) |
23 |
10
|
eleq1d |
|- ( ph -> ( ( S ` A ) e. D <-> ( S ` B ) e. D ) ) |
24 |
1 2 3 4 5 6
|
efgs1b |
|- ( A e. dom S -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) ) |
25 |
8 24
|
syl |
|- ( ph -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) ) |
26 |
1 2 3 4 5 6
|
efgs1b |
|- ( B e. dom S -> ( ( S ` B ) e. D <-> ( # ` B ) = 1 ) ) |
27 |
9 26
|
syl |
|- ( ph -> ( ( S ` B ) e. D <-> ( # ` B ) = 1 ) ) |
28 |
23 25 27
|
3bitr3d |
|- ( ph -> ( ( # ` A ) = 1 <-> ( # ` B ) = 1 ) ) |
29 |
28
|
biimpa |
|- ( ( ph /\ ( # ` A ) = 1 ) -> ( # ` B ) = 1 ) |
30 |
|
oveq1 |
|- ( ( # ` B ) = 1 -> ( ( # ` B ) - 1 ) = ( 1 - 1 ) ) |
31 |
30 19
|
eqtrdi |
|- ( ( # ` B ) = 1 -> ( ( # ` B ) - 1 ) = 0 ) |
32 |
31
|
fveq2d |
|- ( ( # ` B ) = 1 -> ( B ` ( ( # ` B ) - 1 ) ) = ( B ` 0 ) ) |
33 |
29 32
|
syl |
|- ( ( ph /\ ( # ` A ) = 1 ) -> ( B ` ( ( # ` B ) - 1 ) ) = ( B ` 0 ) ) |
34 |
22 33
|
eqtr3d |
|- ( ( ph /\ ( # ` A ) = 1 ) -> ( A ` 0 ) = ( B ` 0 ) ) |
35 |
11 34
|
mtand |
|- ( ph -> -. ( # ` A ) = 1 ) |
36 |
1 2 3 4 5 6
|
efgsdm |
|- ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. u e. ( 1 ..^ ( # ` A ) ) ( A ` u ) e. ran ( T ` ( A ` ( u - 1 ) ) ) ) ) |
37 |
36
|
simp1bi |
|- ( A e. dom S -> A e. ( Word W \ { (/) } ) ) |
38 |
|
eldifsn |
|- ( A e. ( Word W \ { (/) } ) <-> ( A e. Word W /\ A =/= (/) ) ) |
39 |
|
lennncl |
|- ( ( A e. Word W /\ A =/= (/) ) -> ( # ` A ) e. NN ) |
40 |
38 39
|
sylbi |
|- ( A e. ( Word W \ { (/) } ) -> ( # ` A ) e. NN ) |
41 |
8 37 40
|
3syl |
|- ( ph -> ( # ` A ) e. NN ) |
42 |
|
elnn1uz2 |
|- ( ( # ` A ) e. NN <-> ( ( # ` A ) = 1 \/ ( # ` A ) e. ( ZZ>= ` 2 ) ) ) |
43 |
41 42
|
sylib |
|- ( ph -> ( ( # ` A ) = 1 \/ ( # ` A ) e. ( ZZ>= ` 2 ) ) ) |
44 |
43
|
ord |
|- ( ph -> ( -. ( # ` A ) = 1 -> ( # ` A ) e. ( ZZ>= ` 2 ) ) ) |
45 |
35 44
|
mpd |
|- ( ph -> ( # ` A ) e. ( ZZ>= ` 2 ) ) |
46 |
|
uz2m1nn |
|- ( ( # ` A ) e. ( ZZ>= ` 2 ) -> ( ( # ` A ) - 1 ) e. NN ) |
47 |
45 46
|
syl |
|- ( ph -> ( ( # ` A ) - 1 ) e. NN ) |
48 |
35 28
|
mtbid |
|- ( ph -> -. ( # ` B ) = 1 ) |
49 |
1 2 3 4 5 6
|
efgsdm |
|- ( B e. dom S <-> ( B e. ( Word W \ { (/) } ) /\ ( B ` 0 ) e. D /\ A. u e. ( 1 ..^ ( # ` B ) ) ( B ` u ) e. ran ( T ` ( B ` ( u - 1 ) ) ) ) ) |
50 |
49
|
simp1bi |
|- ( B e. dom S -> B e. ( Word W \ { (/) } ) ) |
51 |
|
eldifsn |
|- ( B e. ( Word W \ { (/) } ) <-> ( B e. Word W /\ B =/= (/) ) ) |
52 |
|
lennncl |
|- ( ( B e. Word W /\ B =/= (/) ) -> ( # ` B ) e. NN ) |
53 |
51 52
|
sylbi |
|- ( B e. ( Word W \ { (/) } ) -> ( # ` B ) e. NN ) |
54 |
9 50 53
|
3syl |
|- ( ph -> ( # ` B ) e. NN ) |
55 |
|
elnn1uz2 |
|- ( ( # ` B ) e. NN <-> ( ( # ` B ) = 1 \/ ( # ` B ) e. ( ZZ>= ` 2 ) ) ) |
56 |
54 55
|
sylib |
|- ( ph -> ( ( # ` B ) = 1 \/ ( # ` B ) e. ( ZZ>= ` 2 ) ) ) |
57 |
56
|
ord |
|- ( ph -> ( -. ( # ` B ) = 1 -> ( # ` B ) e. ( ZZ>= ` 2 ) ) ) |
58 |
48 57
|
mpd |
|- ( ph -> ( # ` B ) e. ( ZZ>= ` 2 ) ) |
59 |
|
uz2m1nn |
|- ( ( # ` B ) e. ( ZZ>= ` 2 ) -> ( ( # ` B ) - 1 ) e. NN ) |
60 |
58 59
|
syl |
|- ( ph -> ( ( # ` B ) - 1 ) e. NN ) |
61 |
47 60
|
jca |
|- ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) ) |