Theorem efgsp1 16561

Description: If F is an extension sequence and A is an extension of the last element of F, then F + <" A "> is an extension sequence. (Contributed by Mario Carneiro, 1-Oct-2015.)

Hypotheses

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

Assertion

Ref	Expression
efgsp1	|- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F concat <" A "> ) e. dom S )

Distinct variable groups:   y, z   t, n, v, w, y, z, m, x   m, M   x, n, M, t, v, w   k, m, t, x, T   k, n, v, w, y, z, W, m, t, x   .~ , m, t, x, y, z   m, I, n, t, v, w, x, y, z   D, m, t

Allowed substitution hints:   A( x, y, z, w, v, t, k, m, n)   D( x, y, z, w, v, k, n)   .~ ( w, v, k, n)   S( x, y, z, w, v, t, k, m, n)   T( y, z, w, v, n)   F( x, y, z, w, v, t, k, m, n)   I( k)   M( y, z, k)

Proof of Theorem efgsp1

Dummy variables a i are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		efgval.w	. . . . . . . 8 |- W = ( _I ` Word ( I X. 2o ) )
2		efgval.r	. . . . . . . 8 |- .~ = ( ~FG ` I )
3		efgval2.m	. . . . . . . 8 |- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4		efgval2.t	. . . . . . . 8 |- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5		efgred.d	. . . . . . . 8 |- D = ( W \ U_ x e. W ran ( T ` x ) )
6		efgred.s	. . . . . . . 8 |- 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	1, 2, 3, 4, 5, 6	efgsdm 16554	. . . . . . 7 |- ( F e. dom S <-> ( F e. (Word W \ { (/) } ) /\ ( F ` 0 ) e. D /\ A. i e. ( 1..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
8	7	simp1bi 1011	. . . . . 6 |- ( F e. dom S -> F e. (Word W \ { (/) } ) )
9	8	adantr 465	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> F e. (Word W \ { (/) } ) )
10	9	eldifad 3488	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> F e. Word W )
11	1, 2, 3, 4, 5, 6	efgsf 16553	. . . . . . . . . . . 12 |- S : { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W
12	11	fdmi 5736	. . . . . . . . . . . . 13 |- dom S = { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) }
13	12	feq2i 5724	. . . . . . . . . . . 12 |- ( S : dom S --> W <-> S : { t e. (Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W )
14	11, 13	mpbir 209	. . . . . . . . . . 11 |- S : dom S --> W
15	14	ffvelrni 6020	. . . . . . . . . 10 |- ( F e. dom S -> ( S ` F ) e. W )
16	15	adantr 465	. . . . . . . . 9 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( S ` F ) e. W )
17	1, 2, 3, 4	efgtf 16546	. . . . . . . . 9 |- ( ( S ` F ) e. W -> ( ( T ` ( S ` F ) ) = ( a e. ( 0 ... ( # ` ( S ` F ) ) ) , i e. ( I X. 2o ) |-> ( ( S ` F ) splice <. a , a , <" i ( M ` i ) "> >. ) ) /\ ( T ` ( S ` F ) ) : ( ( 0 ... ( # ` ( S ` F ) ) ) X. ( I X. 2o ) ) --> W ) )
18	16, 17	syl 16	. . . . . . . 8 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( T ` ( S ` F ) ) = ( a e. ( 0 ... ( # ` ( S ` F ) ) ) , i e. ( I X. 2o ) |-> ( ( S ` F ) splice <. a , a , <" i ( M ` i ) "> >. ) ) /\ ( T ` ( S ` F ) ) : ( ( 0 ... ( # ` ( S ` F ) ) ) X. ( I X. 2o ) ) --> W ) )
19	18	simprd 463	. . . . . . 7 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( T ` ( S ` F ) ) : ( ( 0 ... ( # ` ( S ` F ) ) ) X. ( I X. 2o ) ) --> W )
20		frn 5737	. . . . . . 7 |- ( ( T ` ( S ` F ) ) : ( ( 0 ... ( # ` ( S ` F ) ) ) X. ( I X. 2o ) ) --> W -> ran ( T ` ( S ` F ) ) C_ W )
21	19, 20	syl 16	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ran ( T ` ( S ` F ) ) C_ W )
22		simpr 461	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A e. ran ( T ` ( S ` F ) ) )
23	21, 22	sseldd 3505	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A e. W )
24	23	s1cld 12578	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> <" A "> e. Word W )
25		ccatcl 12558	. . . 4 |- ( ( F e. Word W /\ <" A "> e. Word W ) -> ( F concat <" A "> ) e. Word W )
26	10, 24, 25	syl2anc 661	. . 3 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F concat <" A "> ) e. Word W )
27		ccatlen 12559	. . . . . . 7 |- ( ( F e. Word W /\ <" A "> e. Word W ) -> ( # ` ( F concat <" A "> ) ) = ( ( # ` F ) + ( # ` <" A "> ) ) )
28	10, 24, 27	syl2anc 661	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` ( F concat <" A "> ) ) = ( ( # ` F ) + ( # ` <" A "> ) ) )
29		s1len 12580	. . . . . . 7 |- ( # ` <" A "> ) = 1
30	29	oveq2i 6295	. . . . . 6 |- ( ( # ` F ) + ( # ` <" A "> ) ) = ( ( # ` F ) + 1 )
31	28, 30	syl6eq 2524	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` ( F concat <" A "> ) ) = ( ( # ` F ) + 1 ) )
32		lencl 12528	. . . . . 6 |- ( F e. Word W -> ( # ` F ) e. NN0 )
33		nn0p1nn 10835	. . . . . 6 |- ( ( # ` F ) e. NN0 -> ( ( # ` F ) + 1 ) e. NN )
34	10, 32, 33	3syl 20	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( # ` F ) + 1 ) e. NN )
35	31, 34	eqeltrd 2555	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` ( F concat <" A "> ) ) e. NN )
36		wrdfin 12527	. . . . 5 |- ( ( F concat <" A "> ) e. Word W -> ( F concat <" A "> ) e. Fin )
37		hashnncl 12404	. . . . 5 |- ( ( F concat <" A "> ) e. Fin -> ( ( # ` ( F concat <" A "> ) ) e. NN <-> ( F concat <" A "> ) =/= (/) ) )
38	26, 36, 37	3syl 20	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( # ` ( F concat <" A "> ) ) e. NN <-> ( F concat <" A "> ) =/= (/) ) )
39	35, 38	mpbid 210	. . 3 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F concat <" A "> ) =/= (/) )
40		eldifsn 4152	. . 3 |- ( ( F concat <" A "> ) e. (Word W \ { (/) } ) <-> ( ( F concat <" A "> ) e. Word W /\ ( F concat <" A "> ) =/= (/) ) )
41	26, 39, 40	sylanbrc 664	. 2 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F concat <" A "> ) e. (Word W \ { (/) } ) )
42		eldifsni 4153	. . . . . . 7 |- ( F e. (Word W \ { (/) } ) -> F =/= (/) )
43	9, 42	syl 16	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> F =/= (/) )
44		wrdfin 12527	. . . . . . 7 |- ( F e. Word W -> F e. Fin )
45		hashnncl 12404	. . . . . . 7 |- ( F e. Fin -> ( ( # ` F ) e. NN <-> F =/= (/) ) )
46	10, 44, 45	3syl 20	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( # ` F ) e. NN <-> F =/= (/) ) )
47	43, 46	mpbird 232	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` F ) e. NN )
48		lbfzo0 11830	. . . . 5 |- ( 0 e. ( 0..^ ( # ` F ) ) <-> ( # ` F ) e. NN )
49	47, 48	sylibr 212	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> 0 e. ( 0..^ ( # ` F ) ) )
50		ccatval1 12560	. . . 4 |- ( ( F e. Word W /\ <" A "> e. Word W /\ 0 e. ( 0..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` 0 ) = ( F ` 0 ) )
51	10, 24, 49, 50	syl3anc 1228	. . 3 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` 0 ) = ( F ` 0 ) )
52	7	simp2bi 1012	. . . 4 |- ( F e. dom S -> ( F ` 0 ) e. D )
53	52	adantr 465	. . 3 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F ` 0 ) e. D )
54	51, 53	eqeltrd 2555	. 2 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` 0 ) e. D )
55	7	simp3bi 1013	. . . . . 6 |- ( F e. dom S -> A. i e. ( 1..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
56	55	adantr 465	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. ( 1..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) )
57		1nn0 10811	. . . . . . . . . . . . 13 |- 1 e. NN0
58		nn0uz 11116	. . . . . . . . . . . . 13 |- NN0 = ( ZZ>= ` 0 )
59	57, 58	eleqtri 2553	. . . . . . . . . . . 12 |- 1 e. ( ZZ>= ` 0 )
60		fzoss1 11820	. . . . . . . . . . . 12 |- ( 1 e. ( ZZ>= ` 0 ) -> ( 1..^ ( # ` F ) ) C_ ( 0..^ ( # ` F ) ) )
61	59, 60	ax-mp 5	. . . . . . . . . . 11 |- ( 1..^ ( # ` F ) ) C_ ( 0..^ ( # ` F ) )
62	61	sseli 3500	. . . . . . . . . 10 |- ( i e. ( 1..^ ( # ` F ) ) -> i e. ( 0..^ ( # ` F ) ) )
63		ccatval1 12560	. . . . . . . . . 10 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 0..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` i ) = ( F ` i ) )
64	62, 63	syl3an3 1263	. . . . . . . . 9 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` i ) = ( F ` i ) )
65		elfzoel2 11796	. . . . . . . . . . . . . . . 16 |- ( i e. ( 1..^ ( # ` F ) ) -> ( # ` F ) e. ZZ )
66		peano2zm 10906	. . . . . . . . . . . . . . . 16 |- ( ( # ` F ) e. ZZ -> ( ( # ` F ) - 1 ) e. ZZ )
67	65, 66	syl 16	. . . . . . . . . . . . . . 15 |- ( i e. ( 1..^ ( # ` F ) ) -> ( ( # ` F ) - 1 ) e. ZZ )
68	65	zred 10966	. . . . . . . . . . . . . . . 16 |- ( i e. ( 1..^ ( # ` F ) ) -> ( # ` F ) e. RR )
69	68	lem1d 10479	. . . . . . . . . . . . . . 15 |- ( i e. ( 1..^ ( # ` F ) ) -> ( ( # ` F ) - 1 ) <_ ( # ` F ) )
70		eluz2 11088	. . . . . . . . . . . . . . 15 |- ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) <-> ( ( ( # ` F ) - 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( ( # ` F ) - 1 ) <_ ( # ` F ) ) )
71	67, 65, 69, 70	syl3anbrc 1180	. . . . . . . . . . . . . 14 |- ( i e. ( 1..^ ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
72		fzoss2 11821	. . . . . . . . . . . . . 14 |- ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) -> ( 0..^ ( ( # ` F ) - 1 ) ) C_ ( 0..^ ( # ` F ) ) )
73	71, 72	syl 16	. . . . . . . . . . . . 13 |- ( i e. ( 1..^ ( # ` F ) ) -> ( 0..^ ( ( # ` F ) - 1 ) ) C_ ( 0..^ ( # ` F ) ) )
74		elfzoelz 11797	. . . . . . . . . . . . . . 15 |- ( i e. ( 1..^ ( # ` F ) ) -> i e. ZZ )
75		elfzom1b 11879	. . . . . . . . . . . . . . 15 |- ( ( i e. ZZ /\ ( # ` F ) e. ZZ ) -> ( i e. ( 1..^ ( # ` F ) ) <-> ( i - 1 ) e. ( 0..^ ( ( # ` F ) - 1 ) ) ) )
76	74, 65, 75	syl2anc 661	. . . . . . . . . . . . . 14 |- ( i e. ( 1..^ ( # ` F ) ) -> ( i e. ( 1..^ ( # ` F ) ) <-> ( i - 1 ) e. ( 0..^ ( ( # ` F ) - 1 ) ) ) )
77	76	ibi 241	. . . . . . . . . . . . 13 |- ( i e. ( 1..^ ( # ` F ) ) -> ( i - 1 ) e. ( 0..^ ( ( # ` F ) - 1 ) ) )
78	73, 77	sseldd 3505	. . . . . . . . . . . 12 |- ( i e. ( 1..^ ( # ` F ) ) -> ( i - 1 ) e. ( 0..^ ( # ` F ) ) )
79		ccatval1 12560	. . . . . . . . . . . 12 |- ( ( F e. Word W /\ <" A "> e. Word W /\ ( i - 1 ) e. ( 0..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` ( i - 1 ) ) = ( F ` ( i - 1 ) ) )
80	78, 79	syl3an3 1263	. . . . . . . . . . 11 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` ( i - 1 ) ) = ( F ` ( i - 1 ) ) )
81	80	fveq2d 5870	. . . . . . . . . 10 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1..^ ( # ` F ) ) ) -> ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) = ( T ` ( F ` ( i - 1 ) ) ) )
82	81	rneqd 5230	. . . . . . . . 9 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1..^ ( # ` F ) ) ) -> ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) = ran ( T ` ( F ` ( i - 1 ) ) ) )
83	64, 82	eleq12d 2549	. . . . . . . 8 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1..^ ( # ` F ) ) ) -> ( ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) <-> ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
84	83	3expa 1196	. . . . . . 7 |- ( ( ( F e. Word W /\ <" A "> e. Word W ) /\ i e. ( 1..^ ( # ` F ) ) ) -> ( ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) <-> ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
85	84	ralbidva 2900	. . . . . 6 |- ( ( F e. Word W /\ <" A "> e. Word W ) -> ( A. i e. ( 1..^ ( # ` F ) ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) <-> A. i e. ( 1..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
86	10, 24, 85	syl2anc 661	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( A. i e. ( 1..^ ( # ` F ) ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) <-> A. i e. ( 1..^ ( # ` F ) ) ( F ` i ) e. ran ( T ` ( F ` ( i - 1 ) ) ) ) )
87	56, 86	mpbird 232	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. ( 1..^ ( # ` F ) ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) )
88	10, 32	syl 16	. . . . . . . . . 10 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` F ) e. NN0 )
89	88	nn0cnd 10854	. . . . . . . . 9 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` F ) e. CC )
90	89	addid2d 9780	. . . . . . . 8 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 0 + ( # ` F ) ) = ( # ` F ) )
91	90	fveq2d 5870	. . . . . . 7 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( ( F concat <" A "> ) ` ( # ` F ) ) )
92		1nn 10547	. . . . . . . . . . 11 |- 1 e. NN
93	29, 92	eqeltri 2551	. . . . . . . . . 10 |- ( # ` <" A "> ) e. NN
94	93	a1i 11	. . . . . . . . 9 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` <" A "> ) e. NN )
95		lbfzo0 11830	. . . . . . . . 9 |- ( 0 e. ( 0..^ ( # ` <" A "> ) ) <-> ( # ` <" A "> ) e. NN )
96	94, 95	sylibr 212	. . . . . . . 8 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> 0 e. ( 0..^ ( # ` <" A "> ) ) )
97		ccatval3 12562	. . . . . . . 8 |- ( ( F e. Word W /\ <" A "> e. Word W /\ 0 e. ( 0..^ ( # ` <" A "> ) ) ) -> ( ( F concat <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( <" A "> ` 0 ) )
98	10, 24, 96, 97	syl3anc 1228	. . . . . . 7 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( <" A "> ` 0 ) )
99	91, 98	eqtr3d 2510	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( # ` F ) ) = ( <" A "> ` 0 ) )
100		s1fv 12582	. . . . . . . 8 |- ( A e. ran ( T ` ( S ` F ) ) -> ( <" A "> ` 0 ) = A )
101	100	adantl 466	. . . . . . 7 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( <" A "> ` 0 ) = A )
102		fzo0end 11872	. . . . . . . . . . . 12 |- ( ( # ` F ) e. NN -> ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) )
103	47, 102	syl 16	. . . . . . . . . . 11 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) )
104		ccatval1 12560	. . . . . . . . . . 11 |- ( ( F e. Word W /\ <" A "> e. Word W /\ ( ( # ` F ) - 1 ) e. ( 0..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) = ( F ` ( ( # ` F ) - 1 ) ) )
105	10, 24, 103, 104	syl3anc 1228	. . . . . . . . . 10 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) = ( F ` ( ( # ` F ) - 1 ) ) )
106	1, 2, 3, 4, 5, 6	efgsval 16555	. . . . . . . . . . 11 |- ( F e. dom S -> ( S ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
107	106	adantr 465	. . . . . . . . . 10 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( S ` F ) = ( F ` ( ( # ` F ) - 1 ) ) )
108	105, 107	eqtr4d 2511	. . . . . . . . 9 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) = ( S ` F ) )
109	108	fveq2d 5870	. . . . . . . 8 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) = ( T ` ( S ` F ) ) )
110	109	rneqd 5230	. . . . . . 7 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ran ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) = ran ( T ` ( S ` F ) ) )
111	22, 101, 110	3eltr4d 2570	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( <" A "> ` 0 ) e. ran ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
112	99, 111	eqeltrd 2555	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( # ` F ) ) e. ran ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
113		fvex 5876	. . . . . 6 |- ( # ` F ) e. _V
114		fveq2 5866	. . . . . . 7 |- ( i = ( # ` F ) -> ( ( F concat <" A "> ) ` i ) = ( ( F concat <" A "> ) ` ( # ` F ) ) )
115		oveq1 6291	. . . . . . . . . 10 |- ( i = ( # ` F ) -> ( i - 1 ) = ( ( # ` F ) - 1 ) )
116	115	fveq2d 5870	. . . . . . . . 9 |- ( i = ( # ` F ) -> ( ( F concat <" A "> ) ` ( i - 1 ) ) = ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) )
117	116	fveq2d 5870	. . . . . . . 8 |- ( i = ( # ` F ) -> ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) = ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
118	117	rneqd 5230	. . . . . . 7 |- ( i = ( # ` F ) -> ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) = ran ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
119	114, 118	eleq12d 2549	. . . . . 6 |- ( i = ( # ` F ) -> ( ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) <-> ( ( F concat <" A "> ) ` ( # ` F ) ) e. ran ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) ) )
120	113, 119	ralsn 4066	. . . . 5 |- ( A. i e. { ( # ` F ) } ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) <-> ( ( F concat <" A "> ) ` ( # ` F ) ) e. ran ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
121	112, 120	sylibr 212	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. { ( # ` F ) } ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) )
122		ralunb 3685	. . . 4 |- ( A. i e. ( ( 1..^ ( # ` F ) ) u. { ( # ` F ) } ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) <-> ( A. i e. ( 1..^ ( # ` F ) ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) /\ A. i e. { ( # ` F ) } ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) ) )
123	87, 121, 122	sylanbrc 664	. . 3 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. ( ( 1..^ ( # ` F ) ) u. { ( # ` F ) } ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) )
124	31	oveq2d 6300	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 1..^ ( # ` ( F concat <" A "> ) ) ) = ( 1..^ ( ( # ` F ) + 1 ) ) )
125		nnuz 11117	. . . . . . 7 |- NN = ( ZZ>= ` 1 )
126	47, 125	syl6eleq 2565	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` F ) e. ( ZZ>= ` 1 ) )
127		fzosplitsn 11886	. . . . . 6 |- ( ( # ` F ) e. ( ZZ>= ` 1 ) -> ( 1..^ ( ( # ` F ) + 1 ) ) = ( ( 1..^ ( # ` F ) ) u. { ( # ` F ) } ) )
128	126, 127	syl 16	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 1..^ ( ( # ` F ) + 1 ) ) = ( ( 1..^ ( # ` F ) ) u. { ( # ` F ) } ) )
129	124, 128	eqtrd 2508	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 1..^ ( # ` ( F concat <" A "> ) ) ) = ( ( 1..^ ( # ` F ) ) u. { ( # ` F ) } ) )
130	129	raleqdv 3064	. . 3 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( A. i e. ( 1..^ ( # ` ( F concat <" A "> ) ) ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) <-> A. i e. ( ( 1..^ ( # ` F ) ) u. { ( # ` F ) } ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) ) )
131	123, 130	mpbird 232	. 2 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A. i e. ( 1..^ ( # ` ( F concat <" A "> ) ) ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) )
132	1, 2, 3, 4, 5, 6	efgsdm 16554	. 2 |- ( ( F concat <" A "> ) e. dom S <-> ( ( F concat <" A "> ) e. (Word W \ { (/) } ) /\ ( ( F concat <" A "> ) ` 0 ) e. D /\ A. i e. ( 1..^ ( # ` ( F concat <" A "> ) ) ) ( ( F concat <" A "> ) ` i ) e. ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) ) )
133	41, 54, 131, 132	syl3anbrc 1180	1 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( F concat <" A "> ) e. dom S )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2814   {crab 2818   \ cdif 3473   u. cun 3474   C_ wss 3476   (/)c0 3785   {csn 4027   <.cop 4033   <.cotp 4035   U_ciun 4325   class class class wbr 4447   |-> cmpt 4505   _I cid 4790   X. cxp 4997   dom cdm 4999   ran crn 5000   -->wf 5584   ` cfv 5588  (class class class)co 6284   |-> cmpt2 6286   1oc1o 7123   2oc2o 7124   Fincfn 7516   0cc0 9492   1c1 9493   + caddc 9495   <_ cle 9629   - cmin 9805   NNcn 10536   NN0cn0 10795   ZZcz 10864   ZZ>=cuz 11082   ...cfz 11672  ..^cfzo 11792   #chash 12373  Word cword 12500   concat cconcat 12502   <"cs1 12503   splice csplice 12505   <"cs2 12769   ~_FG cefg 16530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-ot 4036  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-card 8320  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-n0 10796  df-z 10865  df-uz 11083  df-fz 11673  df-fzo 11793  df-hash 12374  df-word 12508  df-concat 12510  df-s1 12511  df-substr 12512  df-splice 12513  df-s2 12776

This theorem is referenced by:  efgsfo  16563  efgredlemd  16568  efgrelexlemb  16574