efgredlemb

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (Contributed by Mario Carneiro, 30-Sep-2015)

	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 ) )
Assertion	efgredlemb	\|- -. ph

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		fveq2	\|- ( ( S ` A ) = ( S ` B ) -> ( # ` ( S ` A ) ) = ( # ` ( S ` B ) ) )
22	21	breq2d	\|- ( ( S ` A ) = ( S ` B ) -> ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) <-> ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) ) )
23	22	imbi1d	\|- ( ( S ` A ) = ( S ` B ) -> ( ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
24	23	2ralbidv	\|- ( ( S ` A ) = ( S ` B ) -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
25	10 24	syl	\|- ( ph -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
26	7 25	mpbid	\|- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` B ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
27	10	eqcomd	\|- ( ph -> ( S ` B ) = ( S ` A ) )
28		eqcom	\|- ( ( A ` 0 ) = ( B ` 0 ) <-> ( B ` 0 ) = ( A ` 0 ) )
29	11 28	sylnib	\|- ( ph -> -. ( B ` 0 ) = ( A ` 0 ) )
30		eqcom	\|- ( ( A ` K ) = ( B ` L ) <-> ( B ` L ) = ( A ` K ) )
31	20 30	sylnib	\|- ( ph -> -. ( B ` L ) = ( A ` K ) )
32	1 2 3 4 5 6 26 9 8 27 29 13 12 15 14 17 16 19 18 31	efgredlemc	\|- ( ph -> ( Q e. ( ZZ>= ` P ) -> ( B ` 0 ) = ( A ` 0 ) ) )
33	32 28	imbitrrdi	\|- ( ph -> ( Q e. ( ZZ>= ` P ) -> ( A ` 0 ) = ( B ` 0 ) ) )
34	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	efgredlemc	\|- ( ph -> ( P e. ( ZZ>= ` Q ) -> ( A ` 0 ) = ( B ` 0 ) ) )
35	14	elfzelzd	\|- ( ph -> P e. ZZ )
36	15	elfzelzd	\|- ( ph -> Q e. ZZ )
37		uztric	\|- ( ( P e. ZZ /\ Q e. ZZ ) -> ( Q e. ( ZZ>= ` P ) \/ P e. ( ZZ>= ` Q ) ) )
38	35 36 37	syl2anc	\|- ( ph -> ( Q e. ( ZZ>= ` P ) \/ P e. ( ZZ>= ` Q ) ) )
39	33 34 38	mpjaod	\|- ( ph -> ( A ` 0 ) = ( B ` 0 ) )
40	39 11	pm2.65i	\|- -. ph

Metamath Proof Explorer

Theorem efgredlemb

Proof