efgredlema

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)

	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 ) )
Assertion	efgredlema	\|- ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )

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	1 2 3 4 5 6	efgsval	\|- ( B e. dom S -> ( S ` B ) = ( B ` ( ( # ` B ) - 1 ) ) )
13	9 12	syl	\|- ( ph -> ( S ` B ) = ( B ` ( ( # ` B ) - 1 ) ) )
14	1 2 3 4 5 6	efgsval	\|- ( A e. dom S -> ( S ` A ) = ( A ` ( ( # ` A ) - 1 ) ) )
15	8 14	syl	\|- ( ph -> ( S ` A ) = ( A ` ( ( # ` A ) - 1 ) ) )
16	10 15	eqtr3d	\|- ( ph -> ( S ` B ) = ( A ` ( ( # ` A ) - 1 ) ) )
17	13 16	eqtr3d	\|- ( ph -> ( B ` ( ( # ` B ) - 1 ) ) = ( A ` ( ( # ` A ) - 1 ) ) )
18		oveq1	\|- ( ( # ` A ) = 1 -> ( ( # ` A ) - 1 ) = ( 1 - 1 ) )
19		1m1e0	\|- ( 1 - 1 ) = 0
20	18 19	eqtrdi	\|- ( ( # ` A ) = 1 -> ( ( # ` A ) - 1 ) = 0 )
21	20	fveq2d	\|- ( ( # ` A ) = 1 -> ( A ` ( ( # ` A ) - 1 ) ) = ( A ` 0 ) )
22	17 21	sylan9eq	\|- ( ( ph /\ ( # ` A ) = 1 ) -> ( B ` ( ( # ` B ) - 1 ) ) = ( A ` 0 ) )
23	10	eleq1d	\|- ( ph -> ( ( S ` A ) e. D <-> ( S ` B ) e. D ) )
24	1 2 3 4 5 6	efgs1b	\|- ( A e. dom S -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) )
25	8 24	syl	\|- ( ph -> ( ( S ` A ) e. D <-> ( # ` A ) = 1 ) )
26	1 2 3 4 5 6	efgs1b	\|- ( B e. dom S -> ( ( S ` B ) e. D <-> ( # ` B ) = 1 ) )
27	9 26	syl	\|- ( ph -> ( ( S ` B ) e. D <-> ( # ` B ) = 1 ) )
28	23 25 27	3bitr3d	\|- ( ph -> ( ( # ` A ) = 1 <-> ( # ` B ) = 1 ) )
29	28	biimpa	\|- ( ( ph /\ ( # ` A ) = 1 ) -> ( # ` B ) = 1 )
30		oveq1	\|- ( ( # ` B ) = 1 -> ( ( # ` B ) - 1 ) = ( 1 - 1 ) )
31	30 19	eqtrdi	\|- ( ( # ` B ) = 1 -> ( ( # ` B ) - 1 ) = 0 )
32	31	fveq2d	\|- ( ( # ` B ) = 1 -> ( B ` ( ( # ` B ) - 1 ) ) = ( B ` 0 ) )
33	29 32	syl	\|- ( ( ph /\ ( # ` A ) = 1 ) -> ( B ` ( ( # ` B ) - 1 ) ) = ( B ` 0 ) )
34	22 33	eqtr3d	\|- ( ( ph /\ ( # ` A ) = 1 ) -> ( A ` 0 ) = ( B ` 0 ) )
35	11 34	mtand	\|- ( ph -> -. ( # ` A ) = 1 )
36	1 2 3 4 5 6	efgsdm	\|- ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. u e. ( 1 ..^ ( # ` A ) ) ( A ` u ) e. ran ( T ` ( A ` ( u - 1 ) ) ) ) )
37	36	simp1bi	\|- ( A e. dom S -> A e. ( Word W \ { (/) } ) )
38		eldifsn	\|- ( A e. ( Word W \ { (/) } ) <-> ( A e. Word W /\ A =/= (/) ) )
39		lennncl	\|- ( ( A e. Word W /\ A =/= (/) ) -> ( # ` A ) e. NN )
40	38 39	sylbi	\|- ( A e. ( Word W \ { (/) } ) -> ( # ` A ) e. NN )
41	8 37 40	3syl	\|- ( ph -> ( # ` A ) e. NN )
42		elnn1uz2	\|- ( ( # ` A ) e. NN <-> ( ( # ` A ) = 1 \/ ( # ` A ) e. ( ZZ>= ` 2 ) ) )
43	41 42	sylib	\|- ( ph -> ( ( # ` A ) = 1 \/ ( # ` A ) e. ( ZZ>= ` 2 ) ) )
44	43	ord	\|- ( ph -> ( -. ( # ` A ) = 1 -> ( # ` A ) e. ( ZZ>= ` 2 ) ) )
45	35 44	mpd	\|- ( ph -> ( # ` A ) e. ( ZZ>= ` 2 ) )
46		uz2m1nn	\|- ( ( # ` A ) e. ( ZZ>= ` 2 ) -> ( ( # ` A ) - 1 ) e. NN )
47	45 46	syl	\|- ( ph -> ( ( # ` A ) - 1 ) e. NN )
48	35 28	mtbid	\|- ( ph -> -. ( # ` B ) = 1 )
49	1 2 3 4 5 6	efgsdm	\|- ( B e. dom S <-> ( B e. ( Word W \ { (/) } ) /\ ( B ` 0 ) e. D /\ A. u e. ( 1 ..^ ( # ` B ) ) ( B ` u ) e. ran ( T ` ( B ` ( u - 1 ) ) ) ) )
50	49	simp1bi	\|- ( B e. dom S -> B e. ( Word W \ { (/) } ) )
51		eldifsn	\|- ( B e. ( Word W \ { (/) } ) <-> ( B e. Word W /\ B =/= (/) ) )
52		lennncl	\|- ( ( B e. Word W /\ B =/= (/) ) -> ( # ` B ) e. NN )
53	51 52	sylbi	\|- ( B e. ( Word W \ { (/) } ) -> ( # ` B ) e. NN )
54	9 50 53	3syl	\|- ( ph -> ( # ` B ) e. NN )
55		elnn1uz2	\|- ( ( # ` B ) e. NN <-> ( ( # ` B ) = 1 \/ ( # ` B ) e. ( ZZ>= ` 2 ) ) )
56	54 55	sylib	\|- ( ph -> ( ( # ` B ) = 1 \/ ( # ` B ) e. ( ZZ>= ` 2 ) ) )
57	56	ord	\|- ( ph -> ( -. ( # ` B ) = 1 -> ( # ` B ) e. ( ZZ>= ` 2 ) ) )
58	48 57	mpd	\|- ( ph -> ( # ` B ) e. ( ZZ>= ` 2 ) )
59		uz2m1nn	\|- ( ( # ` B ) e. ( ZZ>= ` 2 ) -> ( ( # ` B ) - 1 ) e. NN )
60	58 59	syl	\|- ( ph -> ( ( # ` B ) - 1 ) e. NN )
61	47 60	jca	\|- ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )

Metamath Proof Explorer

Theorem efgredlema

Proof