Metamath Proof Explorer

Theorem efgredlemd

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
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 ) ) )
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 ) ) ) )
efgredlem.2 
|- ( ph -> A e. dom S )
efgredlem.3 
|- ( ph -> B e. dom S )
efgredlem.4 
|- ( ph -> ( S ` A ) = ( S ` B ) )
efgredlem.5 
|- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
efgredlemb.k 
|- K = ( ( ( # ` A ) - 1 ) - 1 )
efgredlemb.l 
|- L = ( ( ( # ` B ) - 1 ) - 1 )
efgredlemb.p 
|- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
efgredlemb.q 
|- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
efgredlemb.u 
|- ( ph -> U e. ( I X. 2o ) )
efgredlemb.v 
|- ( ph -> V e. ( I X. 2o ) )
efgredlemb.6 
|- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
efgredlemb.7 
|- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
efgredlemb.8 
|- ( ph -> -. ( A ` K ) = ( B ` L ) )
efgredlemd.9 
|- ( ph -> P e. ( ZZ>= ` ( Q + 2 ) ) )
efgredlemd.c 
|- ( ph -> C e. dom S )
efgredlemd.sc 
|- ( ph -> ( S ` C ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
Assertion efgredlemd 
|- ( ph -> ( A ` 0 ) = ( B ` 0 ) )

Proof

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 efgredlemb.k 
 |-  K = ( ( ( # ` A ) - 1 ) - 1 )
13 efgredlemb.l 
 |-  L = ( ( ( # ` B ) - 1 ) - 1 )
14 efgredlemb.p 
 |-  ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
15 efgredlemb.q 
 |-  ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
16 efgredlemb.u 
 |-  ( ph -> U e. ( I X. 2o ) )
17 efgredlemb.v 
 |-  ( ph -> V e. ( I X. 2o ) )
18 efgredlemb.6 
 |-  ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
19 efgredlemb.7 
 |-  ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
20 efgredlemb.8 
 |-  ( ph -> -. ( A ` K ) = ( B ` L ) )
21 efgredlemd.9 
 |-  ( ph -> P e. ( ZZ>= ` ( Q + 2 ) ) )
22 efgredlemd.c 
 |-  ( ph -> C e. dom S )
23 efgredlemd.sc 
 |-  ( ph -> ( S ` C ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
24 1 2 3 4 5 6 efgsdm 
 |-  ( C e. dom S <-> ( C e. ( Word W \ { (/) } ) /\ ( C ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` C ) ) ( C ` i ) e. ran ( T ` ( C ` ( i - 1 ) ) ) ) )
25 24 simp1bi 
 |-  ( C e. dom S -> C e. ( Word W \ { (/) } ) )
26 22 25 syl 
 |-  ( ph -> C e. ( Word W \ { (/) } ) )
27 26 eldifad 
 |-  ( ph -> C e. Word W )
28 1 2 3 4 5 6 efgsdm 
 |-  ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` A ) ) ( A ` i ) e. ran ( T ` ( A ` ( i - 1 ) ) ) ) )
29 28 simp1bi 
 |-  ( A e. dom S -> A e. ( Word W \ { (/) } ) )
30 8 29 syl 
 |-  ( ph -> A e. ( Word W \ { (/) } ) )
31 30 eldifad 
 |-  ( ph -> A e. Word W )
32 wrdf 
 |-  ( A e. Word W -> A : ( 0 ..^ ( # ` A ) ) --> W )
33 31 32 syl 
 |-  ( ph -> A : ( 0 ..^ ( # ` A ) ) --> W )
34 fzossfz 
 |-  ( 0 ..^ ( ( # ` A ) - 1 ) ) C_ ( 0 ... ( ( # ` A ) - 1 ) )
35 lencl 
 |-  ( A e. Word W -> ( # ` A ) e. NN0 )
36 31 35 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
37 36 nn0zd 
 |-  ( ph -> ( # ` A ) e. ZZ )
38 fzoval 
 |-  ( ( # ` A ) e. ZZ -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
39 37 38 syl 
 |-  ( ph -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
40 34 39 sseqtrrid 
 |-  ( ph -> ( 0 ..^ ( ( # ` A ) - 1 ) ) C_ ( 0 ..^ ( # ` A ) ) )
41 1 2 3 4 5 6 7 8 9 10 11 efgredlema 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )
42 41 simpld 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. NN )
43 fzo0end 
 |-  ( ( ( # ` A ) - 1 ) e. NN -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
44 42 43 syl 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
45 12 44 eqeltrid 
 |-  ( ph -> K e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
46 40 45 sseldd 
 |-  ( ph -> K e. ( 0 ..^ ( # ` A ) ) )
47 33 46 ffvelrnd 
 |-  ( ph -> ( A ` K ) e. W )
48 47 s1cld 
 |-  ( ph -> <" ( A ` K ) "> e. Word W )
49 eldifsn 
 |-  ( C e. ( Word W \ { (/) } ) <-> ( C e. Word W /\ C =/= (/) ) )
50 lennncl 
 |-  ( ( C e. Word W /\ C =/= (/) ) -> ( # ` C ) e. NN )
51 49 50 sylbi 
 |-  ( C e. ( Word W \ { (/) } ) -> ( # ` C ) e. NN )
52 26 51 syl 
 |-  ( ph -> ( # ` C ) e. NN )
53 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` C ) ) <-> ( # ` C ) e. NN )
54 52 53 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ ( # ` C ) ) )
55 ccatval1 
 |-  ( ( C e. Word W /\ <" ( A ` K ) "> e. Word W /\ 0 e. ( 0 ..^ ( # ` C ) ) ) -> ( ( C ++ <" ( A ` K ) "> ) ` 0 ) = ( C ` 0 ) )
56 27 48 54 55 syl3anc 
 |-  ( ph -> ( ( C ++ <" ( A ` K ) "> ) ` 0 ) = ( C ` 0 ) )
57 1 2 3 4 5 6 efgsdm 
 |-  ( B e. dom S <-> ( B e. ( Word W \ { (/) } ) /\ ( B ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` B ) ) ( B ` i ) e. ran ( T ` ( B ` ( i - 1 ) ) ) ) )
58 57 simp1bi 
 |-  ( B e. dom S -> B e. ( Word W \ { (/) } ) )
59 9 58 syl 
 |-  ( ph -> B e. ( Word W \ { (/) } ) )
60 59 eldifad 
 |-  ( ph -> B e. Word W )
61 wrdf 
 |-  ( B e. Word W -> B : ( 0 ..^ ( # ` B ) ) --> W )
62 60 61 syl 
 |-  ( ph -> B : ( 0 ..^ ( # ` B ) ) --> W )
63 fzossfz 
 |-  ( 0 ..^ ( ( # ` B ) - 1 ) ) C_ ( 0 ... ( ( # ` B ) - 1 ) )
64 lencl 
 |-  ( B e. Word W -> ( # ` B ) e. NN0 )
65 60 64 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
66 65 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
67 fzoval 
 |-  ( ( # ` B ) e. ZZ -> ( 0 ..^ ( # ` B ) ) = ( 0 ... ( ( # ` B ) - 1 ) ) )
68 66 67 syl 
 |-  ( ph -> ( 0 ..^ ( # ` B ) ) = ( 0 ... ( ( # ` B ) - 1 ) ) )
69 63 68 sseqtrrid 
 |-  ( ph -> ( 0 ..^ ( ( # ` B ) - 1 ) ) C_ ( 0 ..^ ( # ` B ) ) )
70 41 simprd 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. NN )
71 fzo0end 
 |-  ( ( ( # ` B ) - 1 ) e. NN -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
72 70 71 syl 
 |-  ( ph -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
73 13 72 eqeltrid 
 |-  ( ph -> L e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
74 69 73 sseldd 
 |-  ( ph -> L e. ( 0 ..^ ( # ` B ) ) )
75 62 74 ffvelrnd 
 |-  ( ph -> ( B ` L ) e. W )
76 75 s1cld 
 |-  ( ph -> <" ( B ` L ) "> e. Word W )
77 ccatval1 
 |-  ( ( C e. Word W /\ <" ( B ` L ) "> e. Word W /\ 0 e. ( 0 ..^ ( # ` C ) ) ) -> ( ( C ++ <" ( B ` L ) "> ) ` 0 ) = ( C ` 0 ) )
78 27 76 54 77 syl3anc 
 |-  ( ph -> ( ( C ++ <" ( B ` L ) "> ) ` 0 ) = ( C ` 0 ) )
79 56 78 eqtr4d 
 |-  ( ph -> ( ( C ++ <" ( A ` K ) "> ) ` 0 ) = ( ( C ++ <" ( B ` L ) "> ) ` 0 ) )
80 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
81 1 80 eqsstri 
 |-  W C_ Word ( I X. 2o )
82 81 47 sseldi 
 |-  ( ph -> ( A ` K ) e. Word ( I X. 2o ) )
83 lencl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( # ` ( A ` K ) ) e. NN0 )
84 82 83 syl 
 |-  ( ph -> ( # ` ( A ` K ) ) e. NN0 )
85 84 nn0red 
 |-  ( ph -> ( # ` ( A ` K ) ) e. RR )
86 2rp 
 |-  2 e. RR+
87 ltaddrp 
 |-  ( ( ( # ` ( A ` K ) ) e. RR /\ 2 e. RR+ ) -> ( # ` ( A ` K ) ) < ( ( # ` ( A ` K ) ) + 2 ) )
88 85 86 87 sylancl 
 |-  ( ph -> ( # ` ( A ` K ) ) < ( ( # ` ( A ` K ) ) + 2 ) )
89 36 nn0red 
 |-  ( ph -> ( # ` A ) e. RR )
90 89 lem1d 
 |-  ( ph -> ( ( # ` A ) - 1 ) <_ ( # ` A ) )
91 fznn 
 |-  ( ( # ` A ) e. ZZ -> ( ( ( # ` A ) - 1 ) e. ( 1 ... ( # ` A ) ) <-> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` A ) - 1 ) <_ ( # ` A ) ) ) )
92 37 91 syl 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) e. ( 1 ... ( # ` A ) ) <-> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` A ) - 1 ) <_ ( # ` A ) ) ) )
93 42 90 92 mpbir2and 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. ( 1 ... ( # ` A ) ) )
94 1 2 3 4 5 6 efgsres 
 |-  ( ( A e. dom S /\ ( ( # ` A ) - 1 ) e. ( 1 ... ( # ` A ) ) ) -> ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) e. dom S )
95 8 93 94 syl2anc 
 |-  ( ph -> ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) e. dom S )
96 1 2 3 4 5 6 efgsval 
 |-  ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) e. dom S -> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) ) )
97 95 96 syl 
 |-  ( ph -> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) ) )
98 fz1ssfz0 
 |-  ( 1 ... ( # ` A ) ) C_ ( 0 ... ( # ` A ) )
99 98 93 sseldi 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. ( 0 ... ( # ` A ) ) )
100 pfxres 
 |-  ( ( A e. Word W /\ ( ( # ` A ) - 1 ) e. ( 0 ... ( # ` A ) ) ) -> ( A prefix ( ( # ` A ) - 1 ) ) = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) )
101 31 99 100 syl2anc 
 |-  ( ph -> ( A prefix ( ( # ` A ) - 1 ) ) = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) )
102 101 fveq2d 
 |-  ( ph -> ( # ` ( A prefix ( ( # ` A ) - 1 ) ) ) = ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) )
103 pfxlen 
 |-  ( ( A e. Word W /\ ( ( # ` A ) - 1 ) e. ( 0 ... ( # ` A ) ) ) -> ( # ` ( A prefix ( ( # ` A ) - 1 ) ) ) = ( ( # ` A ) - 1 ) )
104 31 99 103 syl2anc 
 |-  ( ph -> ( # ` ( A prefix ( ( # ` A ) - 1 ) ) ) = ( ( # ` A ) - 1 ) )
105 102 104 eqtr3d 
 |-  ( ph -> ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( ( # ` A ) - 1 ) )
106 105 oveq1d 
 |-  ( ph -> ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) = ( ( ( # ` A ) - 1 ) - 1 ) )
107 106 12 eqtr4di 
 |-  ( ph -> ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) = K )
108 107 fveq2d 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` ( ( # ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) - 1 ) ) = ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` K ) )
109 45 fvresd 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` K ) = ( A ` K ) )
110 97 108 109 3eqtrd 
 |-  ( ph -> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( A ` K ) )
111 110 fveq2d 
 |-  ( ph -> ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) = ( # ` ( A ` K ) ) )
112 1 2 3 4 5 6 efgsdmi 
 |-  ( ( A e. dom S /\ ( ( # ` A ) - 1 ) e. NN ) -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
113 8 42 112 syl2anc 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
114 12 fveq2i 
 |-  ( A ` K ) = ( A ` ( ( ( # ` A ) - 1 ) - 1 ) )
115 114 fveq2i 
 |-  ( T ` ( A ` K ) ) = ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
116 115 rneqi 
 |-  ran ( T ` ( A ` K ) ) = ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
117 113 116 eleqtrrdi 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( A ` K ) ) )
118 1 2 3 4 efgtlen 
 |-  ( ( ( A ` K ) e. W /\ ( S ` A ) e. ran ( T ` ( A ` K ) ) ) -> ( # ` ( S ` A ) ) = ( ( # ` ( A ` K ) ) + 2 ) )
119 47 117 118 syl2anc 
 |-  ( ph -> ( # ` ( S ` A ) ) = ( ( # ` ( A ` K ) ) + 2 ) )
120 88 111 119 3brtr4d 
 |-  ( ph -> ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) )
121 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 efgredleme 
 |-  ( ph -> ( ( A ` K ) e. ran ( T ` ( S ` C ) ) /\ ( B ` L ) e. ran ( T ` ( S ` C ) ) ) )
122 121 simpld 
 |-  ( ph -> ( A ` K ) e. ran ( T ` ( S ` C ) ) )
123 1 2 3 4 5 6 efgsp1 
 |-  ( ( C e. dom S /\ ( A ` K ) e. ran ( T ` ( S ` C ) ) ) -> ( C ++ <" ( A ` K ) "> ) e. dom S )
124 22 122 123 syl2anc 
 |-  ( ph -> ( C ++ <" ( A ` K ) "> ) e. dom S )
125 1 2 3 4 5 6 efgsval2 
 |-  ( ( C e. Word W /\ ( A ` K ) e. W /\ ( C ++ <" ( A ` K ) "> ) e. dom S ) -> ( S ` ( C ++ <" ( A ` K ) "> ) ) = ( A ` K ) )
126 27 47 124 125 syl3anc 
 |-  ( ph -> ( S ` ( C ++ <" ( A ` K ) "> ) ) = ( A ` K ) )
127 110 126 eqtr4d 
 |-  ( ph -> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( A ` K ) "> ) ) )
128 2fveq3 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( # ` ( S ` a ) ) = ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) )
129 128 breq1d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) <-> ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) ) )
130 fveqeq2 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( S ` a ) = ( S ` b ) <-> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) ) )
131 fveq1 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( a ` 0 ) = ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) )
132 131 eqeq1d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( a ` 0 ) = ( b ` 0 ) <-> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) )
133 130 132 imbi12d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) <-> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) )
134 129 133 imbi12d 
 |-  ( a = ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) ) )
135 fveq2 
 |-  ( b = ( C ++ <" ( A ` K ) "> ) -> ( S ` b ) = ( S ` ( C ++ <" ( A ` K ) "> ) ) )
136 135 eqeq2d 
 |-  ( b = ( C ++ <" ( A ` K ) "> ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) <-> ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( A ` K ) "> ) ) ) )
137 fveq1 
 |-  ( b = ( C ++ <" ( A ` K ) "> ) -> ( b ` 0 ) = ( ( C ++ <" ( A ` K ) "> ) ` 0 ) )
138 137 eqeq2d 
 |-  ( b = ( C ++ <" ( A ` K ) "> ) -> ( ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) <-> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( A ` K ) "> ) ` 0 ) ) )
139 136 138 imbi12d 
 |-  ( b = ( C ++ <" ( A ` K ) "> ) -> ( ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) <-> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( A ` K ) "> ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( A ` K ) "> ) ` 0 ) ) ) )
140 139 imbi2d 
 |-  ( b = ( C ++ <" ( A ` K ) "> ) -> ( ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` b ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( A ` K ) "> ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( A ` K ) "> ) ` 0 ) ) ) ) )
141 134 140 rspc2va 
 |-  ( ( ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) e. dom S /\ ( C ++ <" ( A ` K ) "> ) e. dom S ) /\ A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) -> ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( A ` K ) "> ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( A ` K ) "> ) ` 0 ) ) ) )
142 95 124 7 141 syl21anc 
 |-  ( ph -> ( ( # ` ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( A ` K ) "> ) ) -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( A ` K ) "> ) ` 0 ) ) ) )
143 120 127 142 mp2d 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( A ` K ) "> ) ` 0 ) )
144 81 75 sseldi 
 |-  ( ph -> ( B ` L ) e. Word ( I X. 2o ) )
145 lencl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( # ` ( B ` L ) ) e. NN0 )
146 144 145 syl 
 |-  ( ph -> ( # ` ( B ` L ) ) e. NN0 )
147 146 nn0red 
 |-  ( ph -> ( # ` ( B ` L ) ) e. RR )
148 ltaddrp 
 |-  ( ( ( # ` ( B ` L ) ) e. RR /\ 2 e. RR+ ) -> ( # ` ( B ` L ) ) < ( ( # ` ( B ` L ) ) + 2 ) )
149 147 86 148 sylancl 
 |-  ( ph -> ( # ` ( B ` L ) ) < ( ( # ` ( B ` L ) ) + 2 ) )
150 65 nn0red 
 |-  ( ph -> ( # ` B ) e. RR )
151 150 lem1d 
 |-  ( ph -> ( ( # ` B ) - 1 ) <_ ( # ` B ) )
152 fznn 
 |-  ( ( # ` B ) e. ZZ -> ( ( ( # ` B ) - 1 ) e. ( 1 ... ( # ` B ) ) <-> ( ( ( # ` B ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) <_ ( # ` B ) ) ) )
153 66 152 syl 
 |-  ( ph -> ( ( ( # ` B ) - 1 ) e. ( 1 ... ( # ` B ) ) <-> ( ( ( # ` B ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) <_ ( # ` B ) ) ) )
154 70 151 153 mpbir2and 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. ( 1 ... ( # ` B ) ) )
155 1 2 3 4 5 6 efgsres 
 |-  ( ( B e. dom S /\ ( ( # ` B ) - 1 ) e. ( 1 ... ( # ` B ) ) ) -> ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) e. dom S )
156 9 154 155 syl2anc 
 |-  ( ph -> ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) e. dom S )
157 1 2 3 4 5 6 efgsval 
 |-  ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) e. dom S -> ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) ) )
158 156 157 syl 
 |-  ( ph -> ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) ) )
159 fz1ssfz0 
 |-  ( 1 ... ( # ` B ) ) C_ ( 0 ... ( # ` B ) )
160 159 154 sseldi 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. ( 0 ... ( # ` B ) ) )
161 pfxres 
 |-  ( ( B e. Word W /\ ( ( # ` B ) - 1 ) e. ( 0 ... ( # ` B ) ) ) -> ( B prefix ( ( # ` B ) - 1 ) ) = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) )
162 60 160 161 syl2anc 
 |-  ( ph -> ( B prefix ( ( # ` B ) - 1 ) ) = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) )
163 162 fveq2d 
 |-  ( ph -> ( # ` ( B prefix ( ( # ` B ) - 1 ) ) ) = ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) )
164 pfxlen 
 |-  ( ( B e. Word W /\ ( ( # ` B ) - 1 ) e. ( 0 ... ( # ` B ) ) ) -> ( # ` ( B prefix ( ( # ` B ) - 1 ) ) ) = ( ( # ` B ) - 1 ) )
165 60 160 164 syl2anc 
 |-  ( ph -> ( # ` ( B prefix ( ( # ` B ) - 1 ) ) ) = ( ( # ` B ) - 1 ) )
166 163 165 eqtr3d 
 |-  ( ph -> ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( ( # ` B ) - 1 ) )
167 166 oveq1d 
 |-  ( ph -> ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) = ( ( ( # ` B ) - 1 ) - 1 ) )
168 167 13 eqtr4di 
 |-  ( ph -> ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) = L )
169 168 fveq2d 
 |-  ( ph -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` ( ( # ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) - 1 ) ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` L ) )
170 73 fvresd 
 |-  ( ph -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` L ) = ( B ` L ) )
171 158 169 170 3eqtrd 
 |-  ( ph -> ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( B ` L ) )
172 171 fveq2d 
 |-  ( ph -> ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) = ( # ` ( B ` L ) ) )
173 1 2 3 4 5 6 efgsdmi 
 |-  ( ( B e. dom S /\ ( ( # ` B ) - 1 ) e. NN ) -> ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
174 9 70 173 syl2anc 
 |-  ( ph -> ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
175 10 174 eqeltrd 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
176 13 fveq2i 
 |-  ( B ` L ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) )
177 176 fveq2i 
 |-  ( T ` ( B ` L ) ) = ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
178 177 rneqi 
 |-  ran ( T ` ( B ` L ) ) = ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
179 175 178 eleqtrrdi 
 |-  ( ph -> ( S ` A ) e. ran ( T ` ( B ` L ) ) )
180 1 2 3 4 efgtlen 
 |-  ( ( ( B ` L ) e. W /\ ( S ` A ) e. ran ( T ` ( B ` L ) ) ) -> ( # ` ( S ` A ) ) = ( ( # ` ( B ` L ) ) + 2 ) )
181 75 179 180 syl2anc 
 |-  ( ph -> ( # ` ( S ` A ) ) = ( ( # ` ( B ` L ) ) + 2 ) )
182 149 172 181 3brtr4d 
 |-  ( ph -> ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) )
183 121 simprd 
 |-  ( ph -> ( B ` L ) e. ran ( T ` ( S ` C ) ) )
184 1 2 3 4 5 6 efgsp1 
 |-  ( ( C e. dom S /\ ( B ` L ) e. ran ( T ` ( S ` C ) ) ) -> ( C ++ <" ( B ` L ) "> ) e. dom S )
185 22 183 184 syl2anc 
 |-  ( ph -> ( C ++ <" ( B ` L ) "> ) e. dom S )
186 1 2 3 4 5 6 efgsval2 
 |-  ( ( C e. Word W /\ ( B ` L ) e. W /\ ( C ++ <" ( B ` L ) "> ) e. dom S ) -> ( S ` ( C ++ <" ( B ` L ) "> ) ) = ( B ` L ) )
187 27 75 185 186 syl3anc 
 |-  ( ph -> ( S ` ( C ++ <" ( B ` L ) "> ) ) = ( B ` L ) )
188 171 187 eqtr4d 
 |-  ( ph -> ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( B ` L ) "> ) ) )
189 2fveq3 
 |-  ( a = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( # ` ( S ` a ) ) = ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) )
190 189 breq1d 
 |-  ( a = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) <-> ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) ) )
191 fveqeq2 
 |-  ( a = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( S ` a ) = ( S ` b ) <-> ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` b ) ) )
192 fveq1 
 |-  ( a = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( a ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) )
193 192 eqeq1d 
 |-  ( a = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( a ` 0 ) = ( b ` 0 ) <-> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) )
194 191 193 imbi12d 
 |-  ( a = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) <-> ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` b ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) )
195 190 194 imbi12d 
 |-  ( a = ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) -> ( ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` b ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) ) )
196 fveq2 
 |-  ( b = ( C ++ <" ( B ` L ) "> ) -> ( S ` b ) = ( S ` ( C ++ <" ( B ` L ) "> ) ) )
197 196 eqeq2d 
 |-  ( b = ( C ++ <" ( B ` L ) "> ) -> ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` b ) <-> ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( B ` L ) "> ) ) ) )
198 fveq1 
 |-  ( b = ( C ++ <" ( B ` L ) "> ) -> ( b ` 0 ) = ( ( C ++ <" ( B ` L ) "> ) ` 0 ) )
199 198 eqeq2d 
 |-  ( b = ( C ++ <" ( B ` L ) "> ) -> ( ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) <-> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( B ` L ) "> ) ` 0 ) ) )
200 197 199 imbi12d 
 |-  ( b = ( C ++ <" ( B ` L ) "> ) -> ( ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` b ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) <-> ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( B ` L ) "> ) ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( B ` L ) "> ) ` 0 ) ) ) )
201 200 imbi2d 
 |-  ( b = ( C ++ <" ( B ` L ) "> ) -> ( ( ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` b ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( B ` L ) "> ) ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( B ` L ) "> ) ` 0 ) ) ) ) )
202 195 201 rspc2va 
 |-  ( ( ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) e. dom S /\ ( C ++ <" ( B ` L ) "> ) e. dom S ) /\ A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) -> ( ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( B ` L ) "> ) ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( B ` L ) "> ) ` 0 ) ) ) )
203 156 185 7 202 syl21anc 
 |-  ( ph -> ( ( # ` ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) ) < ( # ` ( S ` A ) ) -> ( ( S ` ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ) = ( S ` ( C ++ <" ( B ` L ) "> ) ) -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( B ` L ) "> ) ` 0 ) ) ) )
204 182 188 203 mp2d 
 |-  ( ph -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( ( C ++ <" ( B ` L ) "> ) ` 0 ) )
205 79 143 204 3eqtr4d 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) )
206 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( ( # ` A ) - 1 ) ) <-> ( ( # ` A ) - 1 ) e. NN )
207 42 206 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
208 207 fvresd 
 |-  ( ph -> ( ( A |` ( 0 ..^ ( ( # ` A ) - 1 ) ) ) ` 0 ) = ( A ` 0 ) )
209 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( ( # ` B ) - 1 ) ) <-> ( ( # ` B ) - 1 ) e. NN )
210 70 209 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
211 210 fvresd 
 |-  ( ph -> ( ( B |` ( 0 ..^ ( ( # ` B ) - 1 ) ) ) ` 0 ) = ( B ` 0 ) )
212 205 208 211 3eqtr3d 
 |-  ( ph -> ( A ` 0 ) = ( B ` 0 ) )