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 \times 2_{𝑜}))$
	efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
	efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
	efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
	efgredlem.1	$⊢ φ \to \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))$
	efgredlem.2	$⊢ φ \to A \in dom S$
	efgredlem.3	$⊢ φ \to B \in dom S$
	efgredlem.4	$⊢ φ \to S (A) = S (B)$
	efgredlem.5	$⊢ φ \to \neg A (0) = B (0)$
	efgredlemb.k	$⊢ K = \|A\| - 1 - 1$
	efgredlemb.l	$⊢ L = \|B\| - 1 - 1$
	efgredlemb.p	$⊢ φ \to P \in (0 \dots \|A (K)\|)$
	efgredlemb.q	$⊢ φ \to Q \in (0 \dots \|B (L)\|)$
	efgredlemb.u	$⊢ φ \to U \in (I \times 2_{𝑜})$
	efgredlemb.v	$⊢ φ \to V \in (I \times 2_{𝑜})$
	efgredlemb.6	$⊢ φ \to S (A) = P T (A (K)) U$
	efgredlemb.7	$⊢ φ \to S (B) = Q T (B (L)) V$
	efgredlemb.8	$⊢ φ \to \neg A (K) = B (L)$
Assertion	efgredlemb	$⊢ \neg φ$

Proof

Step	Hyp	Ref	Expression
1		efgval.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
2		efgval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
3		efgval2.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
4		efgval2.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
5		efgred.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
6		efgred.s	$⊢ S = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
7		efgredlem.1	$⊢ φ \to \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))$
8		efgredlem.2	$⊢ φ \to A \in dom S$
9		efgredlem.3	$⊢ φ \to B \in dom S$
10		efgredlem.4	$⊢ φ \to S (A) = S (B)$
11		efgredlem.5	$⊢ φ \to \neg A (0) = B (0)$
12		efgredlemb.k	$⊢ K = \|A\| - 1 - 1$
13		efgredlemb.l	$⊢ L = \|B\| - 1 - 1$
14		efgredlemb.p	$⊢ φ \to P \in (0 \dots \|A (K)\|)$
15		efgredlemb.q	$⊢ φ \to Q \in (0 \dots \|B (L)\|)$
16		efgredlemb.u	$⊢ φ \to U \in (I \times 2_{𝑜})$
17		efgredlemb.v	$⊢ φ \to V \in (I \times 2_{𝑜})$
18		efgredlemb.6	$⊢ φ \to S (A) = P T (A (K)) U$
19		efgredlemb.7	$⊢ φ \to S (B) = Q T (B (L)) V$
20		efgredlemb.8	$⊢ φ \to \neg A (K) = B (L)$
21		fveq2	$⊢ S (A) = S (B) \to \|S (A)\| = \|S (B)\|$
22	21	breq2d	$⊢ S (A) = S (B) \to (\|S (a)\| < \|S (A)\| \leftrightarrow \|S (a)\| < \|S (B)\|)$
23	22	imbi1d	$⊢ S (A) = S (B) \to ((\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0))) \leftrightarrow (\|S (a)\| < \|S (B)\| \to (S (a) = S (b) \to a (0) = b (0))))$
24	23	2ralbidv	$⊢ S (A) = S (B) \to (\forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0))) \leftrightarrow \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (B)\| \to (S (a) = S (b) \to a (0) = b (0))))$
25	10 24	syl	$⊢ φ \to (\forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0))) \leftrightarrow \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (B)\| \to (S (a) = S (b) \to a (0) = b (0))))$
26	7 25	mpbid	$⊢ φ \to \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (B)\| \to (S (a) = S (b) \to a (0) = b (0)))$
27	10	eqcomd	$⊢ φ \to S (B) = S (A)$
28		eqcom	$⊢ A (0) = B (0) \leftrightarrow B (0) = A (0)$
29	11 28	sylnib	$⊢ φ \to \neg B (0) = A (0)$
30		eqcom	$⊢ A (K) = B (L) \leftrightarrow B (L) = A (K)$
31	20 30	sylnib	$⊢ φ \to \neg 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	$⊢ φ \to (Q \in ℤ_{\geq P} \to B (0) = A (0))$
33	32 28	syl6ibr	$⊢ φ \to (Q \in ℤ_{\geq P} \to 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	$⊢ φ \to (P \in ℤ_{\geq Q} \to A (0) = B (0))$
35	14	elfzelzd	$⊢ φ \to P \in ℤ$
36	15	elfzelzd	$⊢ φ \to Q \in ℤ$
37		uztric	$⊢ (P \in ℤ \land Q \in ℤ) \to (Q \in ℤ_{\geq P} \lor P \in ℤ_{\geq Q})$
38	35 36 37	syl2anc	$⊢ φ \to (Q \in ℤ_{\geq P} \lor P \in ℤ_{\geq Q})$
39	33 34 38	mpjaod	$⊢ φ \to A (0) = B (0)$
40	39 11	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem efgredlemb

Proof