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	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
	efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
	efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
	efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
	efgred.d	⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
	efgred.s	⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
	efgredlem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
	efgredlem.2	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑆 )
	efgredlem.3	⊢ ( 𝜑 → 𝐵 ∈ dom 𝑆 )
	efgredlem.4	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) )
	efgredlem.5	⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
	efgredlemb.k	⊢ 𝐾 = ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 )
	efgredlemb.l	⊢ 𝐿 = ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 )
	efgredlemb.p	⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
	efgredlemb.q	⊢ ( 𝜑 → 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
	efgredlemb.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐼 × 2_o ) )
	efgredlemb.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐼 × 2_o ) )
	efgredlemb.6	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑃 ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) 𝑈 ) )
	efgredlemb.7	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( 𝑄 ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) 𝑉 ) )
	efgredlemb.8	⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) )
Assertion	efgredlemb	⊢ ¬ 𝜑

Proof

Step	Hyp	Ref	Expression
1		efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2_o ) )
2		efgval.r	⊢ ∼ = ( ~_FG ‘ 𝐼 )
3		efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2_o ↦ ⟨ 𝑦 , ( 1_o ∖ 𝑧 ) ⟩ )
4		efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2_o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5		efgred.d	⊢ 𝐷 = ( 𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran ( 𝑇 ‘ 𝑥 ) )
6		efgred.s	⊢ 𝑆 = ( 𝑚 ∈ { 𝑡 ∈ ( Word 𝑊 ∖ { ∅ } ) ∣ ( ( 𝑡 ‘ 0 ) ∈ 𝐷 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑡 ) ) ( 𝑡 ‘ 𝑘 ) ∈ ran ( 𝑇 ‘ ( 𝑡 ‘ ( 𝑘 − 1 ) ) ) ) } ↦ ( 𝑚 ‘ ( ( ♯ ‘ 𝑚 ) − 1 ) ) )
7		efgredlem.1	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
8		efgredlem.2	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑆 )
9		efgredlem.3	⊢ ( 𝜑 → 𝐵 ∈ dom 𝑆 )
10		efgredlem.4	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) )
11		efgredlem.5	⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
12		efgredlemb.k	⊢ 𝐾 = ( ( ( ♯ ‘ 𝐴 ) − 1 ) − 1 )
13		efgredlemb.l	⊢ 𝐿 = ( ( ( ♯ ‘ 𝐵 ) − 1 ) − 1 )
14		efgredlemb.p	⊢ ( 𝜑 → 𝑃 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ‘ 𝐾 ) ) ) )
15		efgredlemb.q	⊢ ( 𝜑 → 𝑄 ∈ ( 0 ... ( ♯ ‘ ( 𝐵 ‘ 𝐿 ) ) ) )
16		efgredlemb.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐼 × 2_o ) )
17		efgredlemb.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐼 × 2_o ) )
18		efgredlemb.6	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐴 ) = ( 𝑃 ( 𝑇 ‘ ( 𝐴 ‘ 𝐾 ) ) 𝑈 ) )
19		efgredlemb.7	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( 𝑄 ( 𝑇 ‘ ( 𝐵 ‘ 𝐿 ) ) 𝑉 ) )
20		efgredlemb.8	⊢ ( 𝜑 → ¬ ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) )
21		fveq2	⊢ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) → ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) = ( ♯ ‘ ( 𝑆 ‘ 𝐵 ) ) )
22	21	breq2d	⊢ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) → ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) ↔ ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐵 ) ) ) )
23	22	imbi1d	⊢ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) → ( ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
24	23	2ralbidv	⊢ ( ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐵 ) → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
25	10 24	syl	⊢ ( 𝜑 → ( ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ↔ ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) ) )
26	7 25	mpbid	⊢ ( 𝜑 → ∀ 𝑎 ∈ dom 𝑆 ∀ 𝑏 ∈ dom 𝑆 ( ( ♯ ‘ ( 𝑆 ‘ 𝑎 ) ) < ( ♯ ‘ ( 𝑆 ‘ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑎 ) = ( 𝑆 ‘ 𝑏 ) → ( 𝑎 ‘ 0 ) = ( 𝑏 ‘ 0 ) ) ) )
27	10	eqcomd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐵 ) = ( 𝑆 ‘ 𝐴 ) )
28		eqcom	⊢ ( ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ↔ ( 𝐵 ‘ 0 ) = ( 𝐴 ‘ 0 ) )
29	11 28	sylnib	⊢ ( 𝜑 → ¬ ( 𝐵 ‘ 0 ) = ( 𝐴 ‘ 0 ) )
30		eqcom	⊢ ( ( 𝐴 ‘ 𝐾 ) = ( 𝐵 ‘ 𝐿 ) ↔ ( 𝐵 ‘ 𝐿 ) = ( 𝐴 ‘ 𝐾 ) )
31	20 30	sylnib	⊢ ( 𝜑 → ¬ ( 𝐵 ‘ 𝐿 ) = ( 𝐴 ‘ 𝐾 ) )
32	1 2 3 4 5 6 26 9 8 27 29 13 12 15 14 17 16 19 18 31	efgredlemc	⊢ ( 𝜑 → ( 𝑄 ∈ ( ℤ_≥ ‘ 𝑃 ) → ( 𝐵 ‘ 0 ) = ( 𝐴 ‘ 0 ) ) )
33	32 28	imbitrrdi	⊢ ( 𝜑 → ( 𝑄 ∈ ( ℤ_≥ ‘ 𝑃 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
34	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	efgredlemc	⊢ ( 𝜑 → ( 𝑃 ∈ ( ℤ_≥ ‘ 𝑄 ) → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) ) )
35	14	elfzelzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
36	15	elfzelzd	⊢ ( 𝜑 → 𝑄 ∈ ℤ )
37		uztric	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑄 ∈ ℤ ) → ( 𝑄 ∈ ( ℤ_≥ ‘ 𝑃 ) ∨ 𝑃 ∈ ( ℤ_≥ ‘ 𝑄 ) ) )
38	35 36 37	syl2anc	⊢ ( 𝜑 → ( 𝑄 ∈ ( ℤ_≥ ‘ 𝑃 ) ∨ 𝑃 ∈ ( ℤ_≥ ‘ 𝑄 ) ) )
39	33 34 38	mpjaod	⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) = ( 𝐵 ‘ 0 ) )
40	39 11	pm2.65i	⊢ ¬ 𝜑

Metamath Proof Explorer

Theorem efgredlemb

Proof