efgredlemg

	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 ) )
Assertion	efgredlemg	\|- ( ph -> ( # ` ( A ` K ) ) = ( # ` ( B ` L ) ) )

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		fviss	\|- ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
21	1 20	eqsstri	\|- W C_ Word ( I X. 2o )
22	1 2 3 4 5 6 7 8 9 10 11 12 13	efgredlemf	\|- ( ph -> ( ( A ` K ) e. W /\ ( B ` L ) e. W ) )
23	22	simpld	\|- ( ph -> ( A ` K ) e. W )
24	21 23	sselid	\|- ( ph -> ( A ` K ) e. Word ( I X. 2o ) )
25		lencl	\|- ( ( A ` K ) e. Word ( I X. 2o ) -> ( # ` ( A ` K ) ) e. NN0 )
26	24 25	syl	\|- ( ph -> ( # ` ( A ` K ) ) e. NN0 )
27	26	nn0cnd	\|- ( ph -> ( # ` ( A ` K ) ) e. CC )
28	22	simprd	\|- ( ph -> ( B ` L ) e. W )
29	21 28	sselid	\|- ( ph -> ( B ` L ) e. Word ( I X. 2o ) )
30		lencl	\|- ( ( B ` L ) e. Word ( I X. 2o ) -> ( # ` ( B ` L ) ) e. NN0 )
31	29 30	syl	\|- ( ph -> ( # ` ( B ` L ) ) e. NN0 )
32	31	nn0cnd	\|- ( ph -> ( # ` ( B ` L ) ) e. CC )
33		2cnd	\|- ( ph -> 2 e. CC )
34	1 2 3 4 5 6 7 8 9 10 11	efgredlema	\|- ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )
35	34	simpld	\|- ( ph -> ( ( # ` A ) - 1 ) e. NN )
36	1 2 3 4 5 6	efgsdmi	\|- ( ( A e. dom S /\ ( ( # ` A ) - 1 ) e. NN ) -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
37	8 35 36	syl2anc	\|- ( ph -> ( S ` A ) e. ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) ) )
38	12	fveq2i	\|- ( A ` K ) = ( A ` ( ( ( # ` A ) - 1 ) - 1 ) )
39	38	fveq2i	\|- ( T ` ( A ` K ) ) = ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
40	39	rneqi	\|- ran ( T ` ( A ` K ) ) = ran ( T ` ( A ` ( ( ( # ` A ) - 1 ) - 1 ) ) )
41	37 40	eleqtrrdi	\|- ( ph -> ( S ` A ) e. ran ( T ` ( A ` K ) ) )
42	1 2 3 4	efgtlen	\|- ( ( ( A ` K ) e. W /\ ( S ` A ) e. ran ( T ` ( A ` K ) ) ) -> ( # ` ( S ` A ) ) = ( ( # ` ( A ` K ) ) + 2 ) )
43	23 41 42	syl2anc	\|- ( ph -> ( # ` ( S ` A ) ) = ( ( # ` ( A ` K ) ) + 2 ) )
44	34	simprd	\|- ( ph -> ( ( # ` B ) - 1 ) e. NN )
45	1 2 3 4 5 6	efgsdmi	\|- ( ( B e. dom S /\ ( ( # ` B ) - 1 ) e. NN ) -> ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
46	9 44 45	syl2anc	\|- ( ph -> ( S ` B ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
47	10 46	eqeltrd	\|- ( ph -> ( S ` A ) e. ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) ) )
48	13	fveq2i	\|- ( B ` L ) = ( B ` ( ( ( # ` B ) - 1 ) - 1 ) )
49	48	fveq2i	\|- ( T ` ( B ` L ) ) = ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
50	49	rneqi	\|- ran ( T ` ( B ` L ) ) = ran ( T ` ( B ` ( ( ( # ` B ) - 1 ) - 1 ) ) )
51	47 50	eleqtrrdi	\|- ( ph -> ( S ` A ) e. ran ( T ` ( B ` L ) ) )
52	1 2 3 4	efgtlen	\|- ( ( ( B ` L ) e. W /\ ( S ` A ) e. ran ( T ` ( B ` L ) ) ) -> ( # ` ( S ` A ) ) = ( ( # ` ( B ` L ) ) + 2 ) )
53	28 51 52	syl2anc	\|- ( ph -> ( # ` ( S ` A ) ) = ( ( # ` ( B ` L ) ) + 2 ) )
54	43 53	eqtr3d	\|- ( ph -> ( ( # ` ( A ` K ) ) + 2 ) = ( ( # ` ( B ` L ) ) + 2 ) )
55	27 32 33 54	addcan2ad	\|- ( ph -> ( # ` ( A ` K ) ) = ( # ` ( B ` L ) ) )

Metamath Proof Explorer

Theorem efgredlemg

Proof