efgredlem

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) (Proof shortened by AV, 3-Nov-2022)

	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)$
Assertion	efgredlem	$⊢ \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		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
13	1 12	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
14	1 2 3 4 5 6	efgsdm	$⊢ A \in dom S \leftrightarrow (A \in (Word W ∖ \{\emptyset\}) \land A (0) \in D \land \forall i \in (1 ..^\|A\|) A (i) \in ran T (A (i - 1)))$
15	14	simp1bi	$⊢ A \in dom S \to A \in (Word W ∖ \{\emptyset\})$
16	8 15	syl	$⊢ φ \to A \in (Word W ∖ \{\emptyset\})$
17	16	eldifad	$⊢ φ \to A \in Word W$
18		wrdf	$⊢ A \in Word W \to A : (0 ..^\|A\|) ⟶ W$
19	17 18	syl	$⊢ φ \to A : (0 ..^\|A\|) ⟶ W$
20	1 2 3 4 5 6 7 8 9 10 11	efgredlema	$⊢ φ \to (\|A\| - 1 \in ℕ \land \|B\| - 1 \in ℕ)$
21	20	simpld	$⊢ φ \to \|A\| - 1 \in ℕ$
22		nnm1nn0	$⊢ \|A\| - 1 \in ℕ \to \|A\| - 1 - 1 \in ℕ_{0}$
23	21 22	syl	$⊢ φ \to \|A\| - 1 - 1 \in ℕ_{0}$
24	21	nnred	$⊢ φ \to \|A\| - 1 \in ℝ$
25	24	lem1d	$⊢ φ \to \|A\| - 1 - 1 \leq \|A\| - 1$
26		eldifsni	$⊢ A \in (Word W ∖ \{\emptyset\}) \to A \neq \emptyset$
27	8 15 26	3syl	$⊢ φ \to A \neq \emptyset$
28		wrdfin	$⊢ A \in Word W \to A \in Fin$
29		hashnncl	$⊢ A \in Fin \to (\|A\| \in ℕ \leftrightarrow A \neq \emptyset)$
30	17 28 29	3syl	$⊢ φ \to (\|A\| \in ℕ \leftrightarrow A \neq \emptyset)$
31	27 30	mpbird	$⊢ φ \to \|A\| \in ℕ$
32		nnm1nn0	$⊢ \|A\| \in ℕ \to \|A\| - 1 \in ℕ_{0}$
33		fznn0	$⊢ \|A\| - 1 \in ℕ_{0} \to (\|A\| - 1 - 1 \in (0 \dots \|A\| - 1) \leftrightarrow (\|A\| - 1 - 1 \in ℕ_{0} \land \|A\| - 1 - 1 \leq \|A\| - 1))$
34	31 32 33	3syl	$⊢ φ \to (\|A\| - 1 - 1 \in (0 \dots \|A\| - 1) \leftrightarrow (\|A\| - 1 - 1 \in ℕ_{0} \land \|A\| - 1 - 1 \leq \|A\| - 1))$
35	23 25 34	mpbir2and	$⊢ φ \to \|A\| - 1 - 1 \in (0 \dots \|A\| - 1)$
36		lencl	$⊢ A \in Word W \to \|A\| \in ℕ_{0}$
37	17 36	syl	$⊢ φ \to \|A\| \in ℕ_{0}$
38	37	nn0zd	$⊢ φ \to \|A\| \in ℤ$
39		fzoval	$⊢ \|A\| \in ℤ \to (0 ..^\|A\|) = (0 \dots \|A\| - 1)$
40	38 39	syl	$⊢ φ \to (0 ..^\|A\|) = (0 \dots \|A\| - 1)$
41	35 40	eleqtrrd	$⊢ φ \to \|A\| - 1 - 1 \in (0 ..^\|A\|)$
42	19 41	ffvelrnd	$⊢ φ \to A (\|A\| - 1 - 1) \in W$
43	13 42	sselid	$⊢ φ \to A (\|A\| - 1 - 1) \in Word (I \times 2_{𝑜})$
44		lencl	$⊢ A (\|A\| - 1 - 1) \in Word (I \times 2_{𝑜}) \to \|A (\|A\| - 1 - 1)\| \in ℕ_{0}$
45	43 44	syl	$⊢ φ \to \|A (\|A\| - 1 - 1)\| \in ℕ_{0}$
46	45	nn0red	$⊢ φ \to \|A (\|A\| - 1 - 1)\| \in ℝ$
47		2rp	$⊢ 2 \in ℝ^{+}$
48		ltaddrp	$⊢ (\|A (\|A\| - 1 - 1)\| \in ℝ \land 2 \in ℝ^{+}) \to \|A (\|A\| - 1 - 1)\| < \|A (\|A\| - 1 - 1)\| + 2$
49	46 47 48	sylancl	$⊢ φ \to \|A (\|A\| - 1 - 1)\| < \|A (\|A\| - 1 - 1)\| + 2$
50	37	nn0red	$⊢ φ \to \|A\| \in ℝ$
51	50	lem1d	$⊢ φ \to \|A\| - 1 \leq \|A\|$
52		fznn	$⊢ \|A\| \in ℤ \to (\|A\| - 1 \in (1 \dots \|A\|) \leftrightarrow (\|A\| - 1 \in ℕ \land \|A\| - 1 \leq \|A\|))$
53	38 52	syl	$⊢ φ \to (\|A\| - 1 \in (1 \dots \|A\|) \leftrightarrow (\|A\| - 1 \in ℕ \land \|A\| - 1 \leq \|A\|))$
54	21 51 53	mpbir2and	$⊢ φ \to \|A\| - 1 \in (1 \dots \|A\|)$
55	1 2 3 4 5 6	efgsres	$⊢ (A \in dom S \land \|A\| - 1 \in (1 \dots \|A\|)) \to {A ↾}_{(0 ..^\|A\| - 1)} \in dom S$
56	8 54 55	syl2anc	$⊢ φ \to {A ↾}_{(0 ..^\|A\| - 1)} \in dom S$
57	1 2 3 4 5 6	efgsval	$⊢ {A ↾}_{(0 ..^\|A\| - 1)} \in dom S \to S ({A ↾}_{(0 ..^\|A\| - 1)}) = ({A ↾}_{(0 ..^\|A\| - 1)}) (\|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1)$
58	56 57	syl	$⊢ φ \to S ({A ↾}_{(0 ..^\|A\| - 1)}) = ({A ↾}_{(0 ..^\|A\| - 1)}) (\|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1)$
59		fz1ssfz0	$⊢ (1 \dots \|A\|) \subseteq (0 \dots \|A\|)$
60	59 54	sselid	$⊢ φ \to \|A\| - 1 \in (0 \dots \|A\|)$
61		pfxres	$⊢ (A \in Word W \land \|A\| - 1 \in (0 \dots \|A\|)) \to A prefix (\|A\| - 1) = {A ↾}_{(0 ..^\|A\| - 1)}$
62	17 60 61	syl2anc	$⊢ φ \to A prefix (\|A\| - 1) = {A ↾}_{(0 ..^\|A\| - 1)}$
63	62	fveq2d	$⊢ φ \to \|A prefix (\|A\| - 1)\| = \|{A ↾}_{(0 ..^\|A\| - 1)}\|$
64		pfxlen	$⊢ (A \in Word W \land \|A\| - 1 \in (0 \dots \|A\|)) \to \|A prefix (\|A\| - 1)\| = \|A\| - 1$
65	17 60 64	syl2anc	$⊢ φ \to \|A prefix (\|A\| - 1)\| = \|A\| - 1$
66	63 65	eqtr3d	$⊢ φ \to \|{A ↾}_{(0 ..^\|A\| - 1)}\| = \|A\| - 1$
67	66	fvoveq1d	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (\|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1) = ({A ↾}_{(0 ..^\|A\| - 1)}) (\|A\| - 1 - 1)$
68		fzo0end	$⊢ \|A\| - 1 \in ℕ \to \|A\| - 1 - 1 \in (0 ..^\|A\| - 1)$
69		fvres	$⊢ \|A\| - 1 - 1 \in (0 ..^\|A\| - 1) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (\|A\| - 1 - 1) = A (\|A\| - 1 - 1)$
70	21 68 69	3syl	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (\|A\| - 1 - 1) = A (\|A\| - 1 - 1)$
71	58 67 70	3eqtrd	$⊢ φ \to S ({A ↾}_{(0 ..^\|A\| - 1)}) = A (\|A\| - 1 - 1)$
72	71	fveq2d	$⊢ φ \to \|S ({A ↾}_{(0 ..^\|A\| - 1)})\| = \|A (\|A\| - 1 - 1)\|$
73	1 2 3 4 5 6	efgsdmi	$⊢ (A \in dom S \land \|A\| - 1 \in ℕ) \to S (A) \in ran T (A (\|A\| - 1 - 1))$
74	8 21 73	syl2anc	$⊢ φ \to S (A) \in ran T (A (\|A\| - 1 - 1))$
75	1 2 3 4	efgtlen	$⊢ (A (\|A\| - 1 - 1) \in W \land S (A) \in ran T (A (\|A\| - 1 - 1))) \to \|S (A)\| = \|A (\|A\| - 1 - 1)\| + 2$
76	42 74 75	syl2anc	$⊢ φ \to \|S (A)\| = \|A (\|A\| - 1 - 1)\| + 2$
77	49 72 76	3brtr4d	$⊢ φ \to \|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\|$
78	1 2 3 4	efgtf	$⊢ A (\|A\| - 1 - 1) \in W \to (T (A (\|A\| - 1 - 1)) = (a \in (0 \dots \|A (\|A\| - 1 - 1)\|), b \in (I \times 2_{𝑜}) ⟼ A (\|A\| - 1 - 1) splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (A (\|A\| - 1 - 1)) : (0 \dots \|A (\|A\| - 1 - 1)\|) \times (I \times 2_{𝑜}) ⟶ W)$
79	42 78	syl	$⊢ φ \to (T (A (\|A\| - 1 - 1)) = (a \in (0 \dots \|A (\|A\| - 1 - 1)\|), b \in (I \times 2_{𝑜}) ⟼ A (\|A\| - 1 - 1) splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (A (\|A\| - 1 - 1)) : (0 \dots \|A (\|A\| - 1 - 1)\|) \times (I \times 2_{𝑜}) ⟶ W)$
80	79	simprd	$⊢ φ \to T (A (\|A\| - 1 - 1)) : (0 \dots \|A (\|A\| - 1 - 1)\|) \times (I \times 2_{𝑜}) ⟶ W$
81		ffn	$⊢ T (A (\|A\| - 1 - 1)) : (0 \dots \|A (\|A\| - 1 - 1)\|) \times (I \times 2_{𝑜}) ⟶ W \to T (A (\|A\| - 1 - 1)) Fn ((0 \dots \|A (\|A\| - 1 - 1)\|) \times (I \times 2_{𝑜}))$
82		ovelrn	$⊢ T (A (\|A\| - 1 - 1)) Fn ((0 \dots \|A (\|A\| - 1 - 1)\|) \times (I \times 2_{𝑜})) \to (S (A) \in ran T (A (\|A\| - 1 - 1)) \leftrightarrow \exists i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r)$
83	80 81 82	3syl	$⊢ φ \to (S (A) \in ran T (A (\|A\| - 1 - 1)) \leftrightarrow \exists i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r)$
84	74 83	mpbid	$⊢ φ \to \exists i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r$
85	20	simprd	$⊢ φ \to \|B\| - 1 \in ℕ$
86	1 2 3 4 5 6	efgsdmi	$⊢ (B \in dom S \land \|B\| - 1 \in ℕ) \to S (B) \in ran T (B (\|B\| - 1 - 1))$
87	9 85 86	syl2anc	$⊢ φ \to S (B) \in ran T (B (\|B\| - 1 - 1))$
88	1 2 3 4 5 6	efgsdm	$⊢ B \in dom S \leftrightarrow (B \in (Word W ∖ \{\emptyset\}) \land B (0) \in D \land \forall i \in (1 ..^\|B\|) B (i) \in ran T (B (i - 1)))$
89	88	simp1bi	$⊢ B \in dom S \to B \in (Word W ∖ \{\emptyset\})$
90	9 89	syl	$⊢ φ \to B \in (Word W ∖ \{\emptyset\})$
91	90	eldifad	$⊢ φ \to B \in Word W$
92		wrdf	$⊢ B \in Word W \to B : (0 ..^\|B\|) ⟶ W$
93	91 92	syl	$⊢ φ \to B : (0 ..^\|B\|) ⟶ W$
94		fzo0end	$⊢ \|B\| - 1 \in ℕ \to \|B\| - 1 - 1 \in (0 ..^\|B\| - 1)$
95		elfzofz	$⊢ \|B\| - 1 - 1 \in (0 ..^\|B\| - 1) \to \|B\| - 1 - 1 \in (0 \dots \|B\| - 1)$
96	85 94 95	3syl	$⊢ φ \to \|B\| - 1 - 1 \in (0 \dots \|B\| - 1)$
97		lencl	$⊢ B \in Word W \to \|B\| \in ℕ_{0}$
98	91 97	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
99	98	nn0zd	$⊢ φ \to \|B\| \in ℤ$
100		fzoval	$⊢ \|B\| \in ℤ \to (0 ..^\|B\|) = (0 \dots \|B\| - 1)$
101	99 100	syl	$⊢ φ \to (0 ..^\|B\|) = (0 \dots \|B\| - 1)$
102	96 101	eleqtrrd	$⊢ φ \to \|B\| - 1 - 1 \in (0 ..^\|B\|)$
103	93 102	ffvelrnd	$⊢ φ \to B (\|B\| - 1 - 1) \in W$
104	1 2 3 4	efgtf	$⊢ B (\|B\| - 1 - 1) \in W \to (T (B (\|B\| - 1 - 1)) = (a \in (0 \dots \|B (\|B\| - 1 - 1)\|), b \in (I \times 2_{𝑜}) ⟼ B (\|B\| - 1 - 1) splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (B (\|B\| - 1 - 1)) : (0 \dots \|B (\|B\| - 1 - 1)\|) \times (I \times 2_{𝑜}) ⟶ W)$
105	103 104	syl	$⊢ φ \to (T (B (\|B\| - 1 - 1)) = (a \in (0 \dots \|B (\|B\| - 1 - 1)\|), b \in (I \times 2_{𝑜}) ⟼ B (\|B\| - 1 - 1) splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (B (\|B\| - 1 - 1)) : (0 \dots \|B (\|B\| - 1 - 1)\|) \times (I \times 2_{𝑜}) ⟶ W)$
106	105	simprd	$⊢ φ \to T (B (\|B\| - 1 - 1)) : (0 \dots \|B (\|B\| - 1 - 1)\|) \times (I \times 2_{𝑜}) ⟶ W$
107		ffn	$⊢ T (B (\|B\| - 1 - 1)) : (0 \dots \|B (\|B\| - 1 - 1)\|) \times (I \times 2_{𝑜}) ⟶ W \to T (B (\|B\| - 1 - 1)) Fn ((0 \dots \|B (\|B\| - 1 - 1)\|) \times (I \times 2_{𝑜}))$
108		ovelrn	$⊢ T (B (\|B\| - 1 - 1)) Fn ((0 \dots \|B (\|B\| - 1 - 1)\|) \times (I \times 2_{𝑜})) \to (S (B) \in ran T (B (\|B\| - 1 - 1)) \leftrightarrow \exists j \in (0 \dots \|B (\|B\| - 1 - 1)\|) \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s)$
109	106 107 108	3syl	$⊢ φ \to (S (B) \in ran T (B (\|B\| - 1 - 1)) \leftrightarrow \exists j \in (0 \dots \|B (\|B\| - 1 - 1)\|) \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s)$
110	87 109	mpbid	$⊢ φ \to \exists j \in (0 \dots \|B (\|B\| - 1 - 1)\|) \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s$
111		reeanv	$⊢ \exists i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \exists j \in (0 \dots \|B (\|B\| - 1 - 1)\|) (\exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r \land \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s) \leftrightarrow (\exists i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r \land \exists j \in (0 \dots \|B (\|B\| - 1 - 1)\|) \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s)$
112		reeanv	$⊢ \exists r \in (I \times 2_{𝑜}) \exists s \in (I \times 2_{𝑜}) (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s) \leftrightarrow (\exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r \land \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s)$
113	7	ad3antrrr	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 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)))$
114	8	ad3antrrr	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to A \in dom S$
115	9	ad3antrrr	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to B \in dom S$
116	10	ad3antrrr	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to S (A) = S (B)$
117	11	ad3antrrr	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to \neg A (0) = B (0)$
118		eqid	$⊢ \|A\| - 1 - 1 = \|A\| - 1 - 1$
119		eqid	$⊢ \|B\| - 1 - 1 = \|B\| - 1 - 1$
120		simpllr	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))$
121	120	simpld	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to i \in (0 \dots \|A (\|A\| - 1 - 1)\|)$
122	120	simprd	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to j \in (0 \dots \|B (\|B\| - 1 - 1)\|)$
123		simplrl	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to (r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜}))$
124	123	simpld	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to r \in (I \times 2_{𝑜})$
125	123	simprd	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to s \in (I \times 2_{𝑜})$
126		simplrr	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s)$
127	126	simpld	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to S (A) = i T (A (\|A\| - 1 - 1)) r$
128	126	simprd	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to S (B) = j T (B (\|B\| - 1 - 1)) s$
129		simpr	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \to \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)$
130	1 2 3 4 5 6 113 114 115 116 117 118 119 121 122 124 125 127 128 129	efgredlemb	$⊢ \neg (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1))$
131		iman	$⊢ (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \to A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)) \leftrightarrow \neg (((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \land \neg A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1))$
132	130 131	mpbir	$⊢ ((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land ((r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜})) \land (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s))) \to A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)$
133	132	expr	$⊢ ((φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \land (r \in (I \times 2_{𝑜}) \land s \in (I \times 2_{𝑜}))) \to ((S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s) \to A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1))$
134	133	rexlimdvva	$⊢ (φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \to (\exists r \in (I \times 2_{𝑜}) \exists s \in (I \times 2_{𝑜}) (S (A) = i T (A (\|A\| - 1 - 1)) r \land S (B) = j T (B (\|B\| - 1 - 1)) s) \to A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1))$
135	112 134	syl5bir	$⊢ (φ \land (i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \land j \in (0 \dots \|B (\|B\| - 1 - 1)\|))) \to ((\exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r \land \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s) \to A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1))$
136	135	rexlimdvva	$⊢ φ \to (\exists i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \exists j \in (0 \dots \|B (\|B\| - 1 - 1)\|) (\exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r \land \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s) \to A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1))$
137	111 136	syl5bir	$⊢ φ \to ((\exists i \in (0 \dots \|A (\|A\| - 1 - 1)\|) \exists r \in (I \times 2_{𝑜}) S (A) = i T (A (\|A\| - 1 - 1)) r \land \exists j \in (0 \dots \|B (\|B\| - 1 - 1)\|) \exists s \in (I \times 2_{𝑜}) S (B) = j T (B (\|B\| - 1 - 1)) s) \to A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1))$
138	84 110 137	mp2and	$⊢ φ \to A (\|A\| - 1 - 1) = B (\|B\| - 1 - 1)$
139		fvres	$⊢ \|B\| - 1 - 1 \in (0 ..^\|B\| - 1) \to ({B ↾}_{(0 ..^\|B\| - 1)}) (\|B\| - 1 - 1) = B (\|B\| - 1 - 1)$
140	85 94 139	3syl	$⊢ φ \to ({B ↾}_{(0 ..^\|B\| - 1)}) (\|B\| - 1 - 1) = B (\|B\| - 1 - 1)$
141	138 70 140	3eqtr4d	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (\|A\| - 1 - 1) = ({B ↾}_{(0 ..^\|B\| - 1)}) (\|B\| - 1 - 1)$
142		fz1ssfz0	$⊢ (1 \dots \|B\|) \subseteq (0 \dots \|B\|)$
143	98	nn0red	$⊢ φ \to \|B\| \in ℝ$
144	143	lem1d	$⊢ φ \to \|B\| - 1 \leq \|B\|$
145		fznn	$⊢ \|B\| \in ℤ \to (\|B\| - 1 \in (1 \dots \|B\|) \leftrightarrow (\|B\| - 1 \in ℕ \land \|B\| - 1 \leq \|B\|))$
146	99 145	syl	$⊢ φ \to (\|B\| - 1 \in (1 \dots \|B\|) \leftrightarrow (\|B\| - 1 \in ℕ \land \|B\| - 1 \leq \|B\|))$
147	85 144 146	mpbir2and	$⊢ φ \to \|B\| - 1 \in (1 \dots \|B\|)$
148	142 147	sselid	$⊢ φ \to \|B\| - 1 \in (0 \dots \|B\|)$
149		pfxres	$⊢ (B \in Word W \land \|B\| - 1 \in (0 \dots \|B\|)) \to B prefix (\|B\| - 1) = {B ↾}_{(0 ..^\|B\| - 1)}$
150	91 148 149	syl2anc	$⊢ φ \to B prefix (\|B\| - 1) = {B ↾}_{(0 ..^\|B\| - 1)}$
151	150	fveq2d	$⊢ φ \to \|B prefix (\|B\| - 1)\| = \|{B ↾}_{(0 ..^\|B\| - 1)}\|$
152		pfxlen	$⊢ (B \in Word W \land \|B\| - 1 \in (0 \dots \|B\|)) \to \|B prefix (\|B\| - 1)\| = \|B\| - 1$
153	91 148 152	syl2anc	$⊢ φ \to \|B prefix (\|B\| - 1)\| = \|B\| - 1$
154	151 153	eqtr3d	$⊢ φ \to \|{B ↾}_{(0 ..^\|B\| - 1)}\| = \|B\| - 1$
155	154	fvoveq1d	$⊢ φ \to ({B ↾}_{(0 ..^\|B\| - 1)}) (\|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1) = ({B ↾}_{(0 ..^\|B\| - 1)}) (\|B\| - 1 - 1)$
156	141 67 155	3eqtr4d	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (\|{A ↾}_{(0 ..^\|A\| - 1)}\| - 1) = ({B ↾}_{(0 ..^\|B\| - 1)}) (\|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1)$
157	1 2 3 4 5 6	efgsres	$⊢ (B \in dom S \land \|B\| - 1 \in (1 \dots \|B\|)) \to {B ↾}_{(0 ..^\|B\| - 1)} \in dom S$
158	9 147 157	syl2anc	$⊢ φ \to {B ↾}_{(0 ..^\|B\| - 1)} \in dom S$
159	1 2 3 4 5 6	efgsval	$⊢ {B ↾}_{(0 ..^\|B\| - 1)} \in dom S \to S ({B ↾}_{(0 ..^\|B\| - 1)}) = ({B ↾}_{(0 ..^\|B\| - 1)}) (\|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1)$
160	158 159	syl	$⊢ φ \to S ({B ↾}_{(0 ..^\|B\| - 1)}) = ({B ↾}_{(0 ..^\|B\| - 1)}) (\|{B ↾}_{(0 ..^\|B\| - 1)}\| - 1)$
161	156 58 160	3eqtr4d	$⊢ φ \to S ({A ↾}_{(0 ..^\|A\| - 1)}) = S ({B ↾}_{(0 ..^\|B\| - 1)})$
162		fveq2	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to S (a) = S ({A ↾}_{(0 ..^\|A\| - 1)})$
163	162	fveq2d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to \|S (a)\| = \|S ({A ↾}_{(0 ..^\|A\| - 1)})\|$
164	163	breq1d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to (\|S (a)\| < \|S (A)\| \leftrightarrow \|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\|)$
165	162	eqeq1d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to (S (a) = S (b) \leftrightarrow S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b))$
166		fveq1	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to a (0) = ({A ↾}_{(0 ..^\|A\| - 1)}) (0)$
167	166	eqeq1d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to (a (0) = b (0) \leftrightarrow ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0))$
168	165 167	imbi12d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to ((S (a) = S (b) \to a (0) = b (0)) \leftrightarrow (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0)))$
169	164 168	imbi12d	$⊢ a = {A ↾}_{(0 ..^\|A\| - 1)} \to ((\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0))) \leftrightarrow (\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0))))$
170		fveq2	$⊢ b = {B ↾}_{(0 ..^\|B\| - 1)} \to S (b) = S ({B ↾}_{(0 ..^\|B\| - 1)})$
171	170	eqeq2d	$⊢ b = {B ↾}_{(0 ..^\|B\| - 1)} \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \leftrightarrow S ({A ↾}_{(0 ..^\|A\| - 1)}) = S ({B ↾}_{(0 ..^\|B\| - 1)}))$
172		fveq1	$⊢ b = {B ↾}_{(0 ..^\|B\| - 1)} \to b (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0)$
173	172	eqeq2d	$⊢ b = {B ↾}_{(0 ..^\|B\| - 1)} \to (({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0) \leftrightarrow ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0))$
174	171 173	imbi12d	$⊢ b = {B ↾}_{(0 ..^\|B\| - 1)} \to ((S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0)) \leftrightarrow (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S ({B ↾}_{(0 ..^\|B\| - 1)}) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0)))$
175	174	imbi2d	$⊢ b = {B ↾}_{(0 ..^\|B\| - 1)} \to ((\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S (b) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = b (0))) \leftrightarrow (\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S ({B ↾}_{(0 ..^\|B\| - 1)}) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0))))$
176	169 175	rspc2va	$⊢ (({A ↾}_{(0 ..^\|A\| - 1)} \in dom S \land {B ↾}_{(0 ..^\|B\| - 1)} \in dom S) \land \forall a \in dom S \forall b \in dom S (\|S (a)\| < \|S (A)\| \to (S (a) = S (b) \to a (0) = b (0)))) \to (\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S ({B ↾}_{(0 ..^\|B\| - 1)}) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0)))$
177	56 158 7 176	syl21anc	$⊢ φ \to (\|S ({A ↾}_{(0 ..^\|A\| - 1)})\| < \|S (A)\| \to (S ({A ↾}_{(0 ..^\|A\| - 1)}) = S ({B ↾}_{(0 ..^\|B\| - 1)}) \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0)))$
178	77 161 177	mp2d	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = ({B ↾}_{(0 ..^\|B\| - 1)}) (0)$
179		lbfzo0	$⊢ 0 \in (0 ..^\|A\| - 1) \leftrightarrow \|A\| - 1 \in ℕ$
180	21 179	sylibr	$⊢ φ \to 0 \in (0 ..^\|A\| - 1)$
181	180	fvresd	$⊢ φ \to ({A ↾}_{(0 ..^\|A\| - 1)}) (0) = A (0)$
182		lbfzo0	$⊢ 0 \in (0 ..^\|B\| - 1) \leftrightarrow \|B\| - 1 \in ℕ$
183	85 182	sylibr	$⊢ φ \to 0 \in (0 ..^\|B\| - 1)$
184	183	fvresd	$⊢ φ \to ({B ↾}_{(0 ..^\|B\| - 1)}) (0) = B (0)$
185	178 181 184	3eqtr3d	$⊢ φ \to A (0) = B (0)$
186	185 11	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem efgredlem

Proof