Theorem efgsp1 16253

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 16246	. . . . . . 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 1003	. . . . . 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 3359	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> F e. Word W )
11	1, 2, 3, 4, 5, 6	efgsf 16245	. . . . . . . . . . . 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 5583	. . . . . . . . . . . . 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 5571	. . . . . . . . . . . 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 5861	. . . . . . . . . 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 16238	. . . . . . . . 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 5584	. . . . . . 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 3376	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> A e. W )
24	23	s1cld 12313	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> <" A "> e. Word W )
25		ccatcl 12293	. . . 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 12294	. . . . . . 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 12315	. . . . . . 7 |- ( # ` <" A "> ) = 1
30	29	oveq2i 6121	. . . . . 6 |- ( ( # ` F ) + ( # ` <" A "> ) ) = ( ( # ` F ) + 1 )
31	28, 30	syl6eq 2491	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` ( F concat <" A "> ) ) = ( ( # ` F ) + 1 ) )
32		lencl 12268	. . . . . 6 |- ( F e. Word W -> ( # ` F ) e. NN0 )
33		nn0p1nn 10638	. . . . . 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 2517	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` ( F concat <" A "> ) ) e. NN )
36		wrdfin 12267	. . . . 5 |- ( ( F concat <" A "> ) e. Word W -> ( F concat <" A "> ) e. Fin )
37		hashnncl 12153	. . . . 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 4019	. . 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 4020	. . . . . . 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 12267	. . . . . . 7 |- ( F e. Word W -> F e. Fin )
45		hashnncl 12153	. . . . . . 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 11605	. . . . 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 12295	. . . 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 1218	. . 3 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` 0 ) = ( F ` 0 ) )
52	7	simp2bi 1004	. . . 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 2517	. 2 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` 0 ) e. D )
55	7	simp3bi 1005	. . . . . 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 10614	. . . . . . . . . . . . 13 |- 1 e. NN0
58		nn0uz 10914	. . . . . . . . . . . . 13 |- NN0 = ( ZZ>= ` 0 )
59	57, 58	eleqtri 2515	. . . . . . . . . . . 12 |- 1 e. ( ZZ>= ` 0 )
60		fzoss1 11595	. . . . . . . . . . . 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 3371	. . . . . . . . . 10 |- ( i e. ( 1..^ ( # ` F ) ) -> i e. ( 0..^ ( # ` F ) ) )
63		ccatval1 12295	. . . . . . . . . 10 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 0..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` i ) = ( F ` i ) )
64	62, 63	syl3an3 1253	. . . . . . . . 9 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` i ) = ( F ` i ) )
65		elfzoel2 11571	. . . . . . . . . . . . . . . 16 |- ( i e. ( 1..^ ( # ` F ) ) -> ( # ` F ) e. ZZ )
66		peano2zm 10707	. . . . . . . . . . . . . . . 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 10766	. . . . . . . . . . . . . . . 16 |- ( i e. ( 1..^ ( # ` F ) ) -> ( # ` F ) e. RR )
69	68	lem1d 10285	. . . . . . . . . . . . . . 15 |- ( i e. ( 1..^ ( # ` F ) ) -> ( ( # ` F ) - 1 ) <_ ( # ` F ) )
70		eluz2 10886	. . . . . . . . . . . . . . 15 |- ( ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) <-> ( ( ( # ` F ) - 1 ) e. ZZ /\ ( # ` F ) e. ZZ /\ ( ( # ` F ) - 1 ) <_ ( # ` F ) ) )
71	67, 65, 69, 70	syl3anbrc 1172	. . . . . . . . . . . . . 14 |- ( i e. ( 1..^ ( # ` F ) ) -> ( # ` F ) e. ( ZZ>= ` ( ( # ` F ) - 1 ) ) )
72		fzoss2 11596	. . . . . . . . . . . . . 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 11572	. . . . . . . . . . . . . . 15 |- ( i e. ( 1..^ ( # ` F ) ) -> i e. ZZ )
75		elfzom1b 11645	. . . . . . . . . . . . . . 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 3376	. . . . . . . . . . . 12 |- ( i e. ( 1..^ ( # ` F ) ) -> ( i - 1 ) e. ( 0..^ ( # ` F ) ) )
79		ccatval1 12295	. . . . . . . . . . . 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 1253	. . . . . . . . . . 11 |- ( ( F e. Word W /\ <" A "> e. Word W /\ i e. ( 1..^ ( # ` F ) ) ) -> ( ( F concat <" A "> ) ` ( i - 1 ) ) = ( F ` ( i - 1 ) ) )
81	80	fveq2d 5714	. . . . . . . . . 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 5086	. . . . . . . . 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 2511	. . . . . . . 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 1187	. . . . . . 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 2750	. . . . . 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 10657	. . . . . . . . 9 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` F ) e. CC )
90	89	addid2d 9589	. . . . . . . 8 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 0 + ( # ` F ) ) = ( # ` F ) )
91	90	fveq2d 5714	. . . . . . 7 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( ( F concat <" A "> ) ` ( # ` F ) ) )
92		1nn 10352	. . . . . . . . . . 11 |- 1 e. NN
93	29, 92	eqeltri 2513	. . . . . . . . . 10 |- ( # ` <" A "> ) e. NN
94	93	a1i 11	. . . . . . . . 9 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` <" A "> ) e. NN )
95		lbfzo0 11605	. . . . . . . . 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 12297	. . . . . . . 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 1218	. . . . . . 7 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( 0 + ( # ` F ) ) ) = ( <" A "> ` 0 ) )
99	91, 98	eqtr3d 2477	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( # ` F ) ) = ( <" A "> ` 0 ) )
100		s1fv 12317	. . . . . . . 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 11638	. . . . . . . . . . . 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 12295	. . . . . . . . . . 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 1218	. . . . . . . . . 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 16247	. . . . . . . . . . 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 2478	. . . . . . . . 9 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) = ( S ` F ) )
109	108	fveq2d 5714	. . . . . . . 8 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) = ( T ` ( S ` F ) ) )
110	109	rneqd 5086	. . . . . . 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 2524	. . . . . 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 2517	. . . . 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 5720	. . . . . 6 |- ( # ` F ) e. _V
114		fveq2 5710	. . . . . . 7 |- ( i = ( # ` F ) -> ( ( F concat <" A "> ) ` i ) = ( ( F concat <" A "> ) ` ( # ` F ) ) )
115		oveq1 6117	. . . . . . . . . 10 |- ( i = ( # ` F ) -> ( i - 1 ) = ( ( # ` F ) - 1 ) )
116	115	fveq2d 5714	. . . . . . . . 9 |- ( i = ( # ` F ) -> ( ( F concat <" A "> ) ` ( i - 1 ) ) = ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) )
117	116	fveq2d 5714	. . . . . . . 8 |- ( i = ( # ` F ) -> ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) = ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
118	117	rneqd 5086	. . . . . . 7 |- ( i = ( # ` F ) -> ran ( T ` ( ( F concat <" A "> ) ` ( i - 1 ) ) ) = ran ( T ` ( ( F concat <" A "> ) ` ( ( # ` F ) - 1 ) ) ) )
119	114, 118	eleq12d 2511	. . . . . 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 3934	. . . . 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 3556	. . . 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 6126	. . . . 5 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 1..^ ( # ` ( F concat <" A "> ) ) ) = ( 1..^ ( ( # ` F ) + 1 ) ) )
125		nnuz 10915	. . . . . . 7 |- NN = ( ZZ>= ` 1 )
126	47, 125	syl6eleq 2533	. . . . . 6 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( # ` F ) e. ( ZZ>= ` 1 ) )
127		fzosplitsn 11652	. . . . . 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 2475	. . . 4 |- ( ( F e. dom S /\ A e. ran ( T ` ( S ` F ) ) ) -> ( 1..^ ( # ` ( F concat <" A "> ) ) ) = ( ( 1..^ ( # ` F ) ) u. { ( # ` F ) } ) )
130	129	raleqdv 2942	. . 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 16246	. 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 1172	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 965   = wceq 1369   e. wcel 1756   =/= wne 2620   A.wral 2734   {crab 2738   \ cdif 3344   u. cun 3345   C_ wss 3347   (/)c0 3656   {csn 3896   <.cop 3902   <.cotp 3904   U_ciun 4190   class class class wbr 4311   e. cmpt 4369   _I cid 4650   X. cxp 4857   dom cdm 4859   ran crn 4860   -->wf 5433   ` cfv 5437  (class class class)co 6110   e. cmpt2 6112   1oc1o 6932   2oc2o 6933   Fincfn 7329   0cc0 9301   1c1 9302   + caddc 9304   <_ cle 9438   - cmin 9614   NNcn 10341   NN0cn0 10598   ZZcz 10665   ZZ>=cuz 10880   ...cfz 11456  ..^cfzo 11567   #chash 12122  Word cword 12240   concat cconcat 12242   <"cs1 12243   splice csplice 12245   <"cs2 12487   ~_FG cefg 16222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4422  ax-sep 4432  ax-nul 4440  ax-pow 4489  ax-pr 4550  ax-un 6391  ax-cnex 9357  ax-resscn 9358  ax-1cn 9359  ax-icn 9360  ax-addcl 9361  ax-addrcl 9362  ax-mulcl 9363  ax-mulrcl 9364  ax-mulcom 9365  ax-addass 9366  ax-mulass 9367  ax-distr 9368  ax-i2m1 9369  ax-1ne0 9370  ax-1rid 9371  ax-rnegex 9372  ax-rrecex 9373  ax-cnre 9374  ax-pre-lttri 9375  ax-pre-lttrn 9376  ax-pre-ltadd 9377  ax-pre-mulgt0 9378

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2739  df-rex 2740  df-reu 2741  df-rab 2743  df-v 2993  df-sbc 3206  df-csb 3308  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-pss 3363  df-nul 3657  df-if 3811  df-pw 3881  df-sn 3897  df-pr 3899  df-tp 3901  df-op 3903  df-ot 3905  df-uni 4111  df-int 4148  df-iun 4192  df-br 4312  df-opab 4370  df-mpt 4371  df-tr 4405  df-eprel 4651  df-id 4655  df-po 4660  df-so 4661  df-fr 4698  df-we 4700  df-ord 4741  df-on 4742  df-lim 4743  df-suc 4744  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-iota 5400  df-fun 5439  df-fn 5440  df-f 5441  df-f1 5442  df-fo 5443  df-f1o 5444  df-fv 5445  df-riota 6071  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-om 6496  df-1st 6596  df-2nd 6597  df-recs 6851  df-rdg 6885  df-1o 6939  df-2o 6940  df-oadd 6943  df-er 7120  df-map 7235  df-pm 7236  df-en 7330  df-dom 7331  df-sdom 7332  df-fin 7333  df-card 8128  df-pnf 9439  df-mnf 9440  df-xr 9441  df-ltxr 9442  df-le 9443  df-sub 9616  df-neg 9617  df-nn 10342  df-n0 10599  df-z 10666  df-uz 10881  df-fz 11457  df-fzo 11568  df-hash 12123  df-word 12248  df-concat 12250  df-s1 12251  df-substr 12252  df-splice 12253  df-s2 12494

This theorem is referenced by:  efgsfo  16255  efgredlemd  16260  efgrelexlemb  16266