efgredlemc

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) (Proof shortened by AV, 15-Oct-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)$
	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	efgredlemc	$⊢ φ \to (P \in ℤ_{\geq Q} \to A (0) = B (0))$

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		uzp1	$⊢ P \in ℤ_{\geq Q} \to (P = Q \lor P \in ℤ_{\geq (Q + 1)})$
22		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
23	1 22	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
24	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)))$
25	24	simp1bi	$⊢ A \in dom S \to A \in (Word W ∖ \{\emptyset\})$
26	8 25	syl	$⊢ φ \to A \in (Word W ∖ \{\emptyset\})$
27	26	eldifad	$⊢ φ \to A \in Word W$
28		wrdf	$⊢ A \in Word W \to A : (0 ..^\|A\|) ⟶ W$
29	27 28	syl	$⊢ φ \to A : (0 ..^\|A\|) ⟶ W$
30		fzossfz	$⊢ (0 ..^\|A\| - 1) \subseteq (0 \dots \|A\| - 1)$
31	1 2 3 4 5 6 7 8 9 10 11	efgredlema	$⊢ φ \to (\|A\| - 1 \in ℕ \land \|B\| - 1 \in ℕ)$
32	31	simpld	$⊢ φ \to \|A\| - 1 \in ℕ$
33		fzo0end	$⊢ \|A\| - 1 \in ℕ \to \|A\| - 1 - 1 \in (0 ..^\|A\| - 1)$
34	32 33	syl	$⊢ φ \to \|A\| - 1 - 1 \in (0 ..^\|A\| - 1)$
35	12 34	eqeltrid	$⊢ φ \to K \in (0 ..^\|A\| - 1)$
36	30 35	sselid	$⊢ φ \to K \in (0 \dots \|A\| - 1)$
37		lencl	$⊢ A \in Word W \to \|A\| \in ℕ_{0}$
38	27 37	syl	$⊢ φ \to \|A\| \in ℕ_{0}$
39	38	nn0zd	$⊢ φ \to \|A\| \in ℤ$
40		fzoval	$⊢ \|A\| \in ℤ \to (0 ..^\|A\|) = (0 \dots \|A\| - 1)$
41	39 40	syl	$⊢ φ \to (0 ..^\|A\|) = (0 \dots \|A\| - 1)$
42	36 41	eleqtrrd	$⊢ φ \to K \in (0 ..^\|A\|)$
43	29 42	ffvelcdmd	$⊢ φ \to A (K) \in W$
44	23 43	sselid	$⊢ φ \to A (K) \in Word (I \times 2_{𝑜})$
45		lencl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to \|A (K)\| \in ℕ_{0}$
46	44 45	syl	$⊢ φ \to \|A (K)\| \in ℕ_{0}$
47		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
48	46 47	eleqtrdi	$⊢ φ \to \|A (K)\| \in ℤ_{\geq 0}$
49		eluzfz2	$⊢ \|A (K)\| \in ℤ_{\geq 0} \to \|A (K)\| \in (0 \dots \|A (K)\|)$
50	48 49	syl	$⊢ φ \to \|A (K)\| \in (0 \dots \|A (K)\|)$
51		ccatpfx	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land P \in (0 \dots \|A (K)\|) \land \|A (K)\| \in (0 \dots \|A (K)\|)) \to (A (K) prefix P) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = A (K) prefix \|A (K)\|$
52	44 14 50 51	syl3anc	$⊢ φ \to (A (K) prefix P) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = A (K) prefix \|A (K)\|$
53		pfxid	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) prefix \|A (K)\| = A (K)$
54	44 53	syl	$⊢ φ \to A (K) prefix \|A (K)\| = A (K)$
55	52 54	eqtrd	$⊢ φ \to (A (K) prefix P) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = A (K)$
56	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)))$
57	56	simp1bi	$⊢ B \in dom S \to B \in (Word W ∖ \{\emptyset\})$
58	9 57	syl	$⊢ φ \to B \in (Word W ∖ \{\emptyset\})$
59	58	eldifad	$⊢ φ \to B \in Word W$
60		wrdf	$⊢ B \in Word W \to B : (0 ..^\|B\|) ⟶ W$
61	59 60	syl	$⊢ φ \to B : (0 ..^\|B\|) ⟶ W$
62		fzossfz	$⊢ (0 ..^\|B\| - 1) \subseteq (0 \dots \|B\| - 1)$
63	31	simprd	$⊢ φ \to \|B\| - 1 \in ℕ$
64		fzo0end	$⊢ \|B\| - 1 \in ℕ \to \|B\| - 1 - 1 \in (0 ..^\|B\| - 1)$
65	63 64	syl	$⊢ φ \to \|B\| - 1 - 1 \in (0 ..^\|B\| - 1)$
66	13 65	eqeltrid	$⊢ φ \to L \in (0 ..^\|B\| - 1)$
67	62 66	sselid	$⊢ φ \to L \in (0 \dots \|B\| - 1)$
68		lencl	$⊢ B \in Word W \to \|B\| \in ℕ_{0}$
69	59 68	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
70	69	nn0zd	$⊢ φ \to \|B\| \in ℤ$
71		fzoval	$⊢ \|B\| \in ℤ \to (0 ..^\|B\|) = (0 \dots \|B\| - 1)$
72	70 71	syl	$⊢ φ \to (0 ..^\|B\|) = (0 \dots \|B\| - 1)$
73	67 72	eleqtrrd	$⊢ φ \to L \in (0 ..^\|B\|)$
74	61 73	ffvelcdmd	$⊢ φ \to B (L) \in W$
75	23 74	sselid	$⊢ φ \to B (L) \in Word (I \times 2_{𝑜})$
76		lencl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to \|B (L)\| \in ℕ_{0}$
77	75 76	syl	$⊢ φ \to \|B (L)\| \in ℕ_{0}$
78	77 47	eleqtrdi	$⊢ φ \to \|B (L)\| \in ℤ_{\geq 0}$
79		eluzfz2	$⊢ \|B (L)\| \in ℤ_{\geq 0} \to \|B (L)\| \in (0 \dots \|B (L)\|)$
80	78 79	syl	$⊢ φ \to \|B (L)\| \in (0 \dots \|B (L)\|)$
81		ccatpfx	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots \|B (L)\|) \land \|B (L)\| \in (0 \dots \|B (L)\|)) \to (B (L) prefix Q) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) = B (L) prefix \|B (L)\|$
82	75 15 80 81	syl3anc	$⊢ φ \to (B (L) prefix Q) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) = B (L) prefix \|B (L)\|$
83		pfxid	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) prefix \|B (L)\| = B (L)$
84	75 83	syl	$⊢ φ \to B (L) prefix \|B (L)\| = B (L)$
85	82 84	eqtrd	$⊢ φ \to (B (L) prefix Q) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) = B (L)$
86	55 85	eqeq12d	$⊢ φ \to ((A (K) prefix P) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) prefix Q) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \leftrightarrow A (K) = B (L))$
87	20 86	mtbird	$⊢ φ \to \neg (A (K) prefix P) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) prefix Q) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
88	1 2 3 4	efgtval	$⊢ (A (K) \in W \land P \in (0 \dots \|A (K)\|) \land U \in (I \times 2_{𝑜})) \to P T (A (K)) U = A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩$
89	43 14 16 88	syl3anc	$⊢ φ \to P T (A (K)) U = A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩$
90	3	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
91	90	ffvelcdmi	$⊢ U \in (I \times 2_{𝑜}) \to M (U) \in (I \times 2_{𝑜})$
92	16 91	syl	$⊢ φ \to M (U) \in (I \times 2_{𝑜})$
93	16 92	s2cld	$⊢ φ \to ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})$
94		splval	$⊢ (A (K) \in W \land (P \in (0 \dots \|A (K)\|) \land P \in (0 \dots \|A (K)\|) \land ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜}))) \to A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩ = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
95	43 14 14 93 94	syl13anc	$⊢ φ \to A (K) splice ⟨P, P, ⟨“ U M (U) ”⟩⟩ = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
96	18 89 95	3eqtrd	$⊢ φ \to S (A) = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
97	1 2 3 4	efgtval	$⊢ (B (L) \in W \land Q \in (0 \dots \|B (L)\|) \land V \in (I \times 2_{𝑜})) \to Q T (B (L)) V = B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩$
98	74 15 17 97	syl3anc	$⊢ φ \to Q T (B (L)) V = B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩$
99	90	ffvelcdmi	$⊢ V \in (I \times 2_{𝑜}) \to M (V) \in (I \times 2_{𝑜})$
100	17 99	syl	$⊢ φ \to M (V) \in (I \times 2_{𝑜})$
101	17 100	s2cld	$⊢ φ \to ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})$
102		splval	$⊢ (B (L) \in W \land (Q \in (0 \dots \|B (L)\|) \land Q \in (0 \dots \|B (L)\|) \land ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜}))) \to B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩ = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
103	74 15 15 101 102	syl13anc	$⊢ φ \to B (L) splice ⟨Q, Q, ⟨“ V M (V) ”⟩⟩ = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
104	19 98 103	3eqtrd	$⊢ φ \to S (B) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
105	10 96 104	3eqtr3d	$⊢ φ \to ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
106	105	adantr	$⊢ (φ \land P = Q) \to ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
107		pfxcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) prefix P \in Word (I \times 2_{𝑜})$
108	44 107	syl	$⊢ φ \to A (K) prefix P \in Word (I \times 2_{𝑜})$
109	108	adantr	$⊢ (φ \land P = Q) \to A (K) prefix P \in Word (I \times 2_{𝑜})$
110	93	adantr	$⊢ (φ \land P = Q) \to ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})$
111		ccatcl	$⊢ (A (K) prefix P \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})) \to (A (K) prefix P) ++ ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})$
112	109 110 111	syl2anc	$⊢ (φ \land P = Q) \to (A (K) prefix P) ++ ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})$
113		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
114	44 113	syl	$⊢ φ \to A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
115	114	adantr	$⊢ (φ \land P = Q) \to A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
116		pfxcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) prefix Q \in Word (I \times 2_{𝑜})$
117	75 116	syl	$⊢ φ \to B (L) prefix Q \in Word (I \times 2_{𝑜})$
118	117	adantr	$⊢ (φ \land P = Q) \to B (L) prefix Q \in Word (I \times 2_{𝑜})$
119	101	adantr	$⊢ (φ \land P = Q) \to ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})$
120		ccatcl	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})) \to (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})$
121	118 119 120	syl2anc	$⊢ (φ \land P = Q) \to (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})$
122		swrdcl	$⊢ B (L) \in Word (I \times 2_{𝑜}) \to B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
123	75 122	syl	$⊢ φ \to B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
124	123	adantr	$⊢ (φ \land P = Q) \to B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
125		pfxlen	$⊢ (A (K) \in Word (I \times 2_{𝑜}) \land P \in (0 \dots \|A (K)\|)) \to \|A (K) prefix P\| = P$
126	44 14 125	syl2anc	$⊢ φ \to \|A (K) prefix P\| = P$
127		pfxlen	$⊢ (B (L) \in Word (I \times 2_{𝑜}) \land Q \in (0 \dots \|B (L)\|)) \to \|B (L) prefix Q\| = Q$
128	75 15 127	syl2anc	$⊢ φ \to \|B (L) prefix Q\| = Q$
129	126 128	eqeq12d	$⊢ φ \to (\|A (K) prefix P\| = \|B (L) prefix Q\| \leftrightarrow P = Q)$
130	129	biimpar	$⊢ (φ \land P = Q) \to \|A (K) prefix P\| = \|B (L) prefix Q\|$
131		s2len	$⊢ \|⟨“ U M (U) ”⟩\| = 2$
132		s2len	$⊢ \|⟨“ V M (V) ”⟩\| = 2$
133	131 132	eqtr4i	$⊢ \|⟨“ U M (U) ”⟩\| = \|⟨“ V M (V) ”⟩\|$
134	133	a1i	$⊢ (φ \land P = Q) \to \|⟨“ U M (U) ”⟩\| = \|⟨“ V M (V) ”⟩\|$
135	130 134	oveq12d	$⊢ (φ \land P = Q) \to \|A (K) prefix P\| + \|⟨“ U M (U) ”⟩\| = \|B (L) prefix Q\| + \|⟨“ V M (V) ”⟩\|$
136		ccatlen	$⊢ (A (K) prefix P \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})) \to \|(A (K) prefix P) ++ ⟨“ U M (U) ”⟩\| = \|A (K) prefix P\| + \|⟨“ U M (U) ”⟩\|$
137	109 110 136	syl2anc	$⊢ (φ \land P = Q) \to \|(A (K) prefix P) ++ ⟨“ U M (U) ”⟩\| = \|A (K) prefix P\| + \|⟨“ U M (U) ”⟩\|$
138		ccatlen	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})) \to \|(B (L) prefix Q) ++ ⟨“ V M (V) ”⟩\| = \|B (L) prefix Q\| + \|⟨“ V M (V) ”⟩\|$
139	118 119 138	syl2anc	$⊢ (φ \land P = Q) \to \|(B (L) prefix Q) ++ ⟨“ V M (V) ”⟩\| = \|B (L) prefix Q\| + \|⟨“ V M (V) ”⟩\|$
140	135 137 139	3eqtr4d	$⊢ (φ \land P = Q) \to \|(A (K) prefix P) ++ ⟨“ U M (U) ”⟩\| = \|(B (L) prefix Q) ++ ⟨“ V M (V) ”⟩\|$
141		ccatopth	$⊢ (((A (K) prefix P) ++ ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \land ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})) \land \|(A (K) prefix P) ++ ⟨“ U M (U) ”⟩\| = \|(B (L) prefix Q) ++ ⟨“ V M (V) ”⟩\|) \to (((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \leftrightarrow ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩ = (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ \land A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨Q, \|B (L)\|⟩))$
142	112 115 121 124 140 141	syl221anc	$⊢ (φ \land P = Q) \to (((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \leftrightarrow ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩ = (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ \land A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨Q, \|B (L)\|⟩))$
143	106 142	mpbid	$⊢ (φ \land P = Q) \to ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩ = (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ \land A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨Q, \|B (L)\|⟩)$
144	143	simpld	$⊢ (φ \land P = Q) \to (A (K) prefix P) ++ ⟨“ U M (U) ”⟩ = (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩$
145		ccatopth	$⊢ ((A (K) prefix P \in Word (I \times 2_{𝑜}) \land ⟨“ U M (U) ”⟩ \in Word (I \times 2_{𝑜})) \land (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V M (V) ”⟩ \in Word (I \times 2_{𝑜})) \land \|A (K) prefix P\| = \|B (L) prefix Q\|) \to ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩ = (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ \leftrightarrow (A (K) prefix P = B (L) prefix Q \land ⟨“ U M (U) ”⟩ = ⟨“ V M (V) ”⟩))$
146	109 110 118 119 130 145	syl221anc	$⊢ (φ \land P = Q) \to ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩ = (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ \leftrightarrow (A (K) prefix P = B (L) prefix Q \land ⟨“ U M (U) ”⟩ = ⟨“ V M (V) ”⟩))$
147	144 146	mpbid	$⊢ (φ \land P = Q) \to (A (K) prefix P = B (L) prefix Q \land ⟨“ U M (U) ”⟩ = ⟨“ V M (V) ”⟩)$
148	147	simpld	$⊢ (φ \land P = Q) \to A (K) prefix P = B (L) prefix Q$
149	143	simprd	$⊢ (φ \land P = Q) \to A (K) substr ⟨P, \|A (K)\|⟩ = B (L) substr ⟨Q, \|B (L)\|⟩$
150	148 149	oveq12d	$⊢ (φ \land P = Q) \to (A (K) prefix P) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) prefix Q) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
151	87 150	mtand	$⊢ φ \to \neg P = Q$
152	151	pm2.21d	$⊢ φ \to (P = Q \to A (0) = B (0))$
153		uzp1	$⊢ P \in ℤ_{\geq (Q + 1)} \to (P = Q + 1 \lor P \in ℤ_{\geq (Q + 1 + 1)})$
154	16	s1cld	$⊢ φ \to ⟨“ U ”⟩ \in Word (I \times 2_{𝑜})$
155		ccatcl	$⊢ (A (K) prefix P \in Word (I \times 2_{𝑜}) \land ⟨“ U ”⟩ \in Word (I \times 2_{𝑜})) \to (A (K) prefix P) ++ ⟨“ U ”⟩ \in Word (I \times 2_{𝑜})$
156	108 154 155	syl2anc	$⊢ φ \to (A (K) prefix P) ++ ⟨“ U ”⟩ \in Word (I \times 2_{𝑜})$
157	92	s1cld	$⊢ φ \to ⟨“ M (U) ”⟩ \in Word (I \times 2_{𝑜})$
158		ccatass	$⊢ ((A (K) prefix P) ++ ⟨“ U ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (U) ”⟩ \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \to (((A (K) prefix P) ++ ⟨“ U ”⟩) ++ ⟨“ M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((A (K) prefix P) ++ ⟨“ U ”⟩) ++ (⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))$
159	156 157 114 158	syl3anc	$⊢ φ \to (((A (K) prefix P) ++ ⟨“ U ”⟩) ++ ⟨“ M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((A (K) prefix P) ++ ⟨“ U ”⟩) ++ (⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))$
160		ccatass	$⊢ (A (K) prefix P \in Word (I \times 2_{𝑜}) \land ⟨“ U ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (U) ”⟩ \in Word (I \times 2_{𝑜})) \to ((A (K) prefix P) ++ ⟨“ U ”⟩) ++ ⟨“ M (U) ”⟩ = (A (K) prefix P) ++ (⟨“ U ”⟩ ++ ⟨“ M (U) ”⟩)$
161	108 154 157 160	syl3anc	$⊢ φ \to ((A (K) prefix P) ++ ⟨“ U ”⟩) ++ ⟨“ M (U) ”⟩ = (A (K) prefix P) ++ (⟨“ U ”⟩ ++ ⟨“ M (U) ”⟩)$
162		df-s2	$⊢ ⟨“ U M (U) ”⟩ = ⟨“ U ”⟩ ++ ⟨“ M (U) ”⟩$
163	162	oveq2i	$⊢ (A (K) prefix P) ++ ⟨“ U M (U) ”⟩ = (A (K) prefix P) ++ (⟨“ U ”⟩ ++ ⟨“ M (U) ”⟩)$
164	161 163	eqtr4di	$⊢ φ \to ((A (K) prefix P) ++ ⟨“ U ”⟩) ++ ⟨“ M (U) ”⟩ = (A (K) prefix P) ++ ⟨“ U M (U) ”⟩$
165	164	oveq1d	$⊢ φ \to (((A (K) prefix P) ++ ⟨“ U ”⟩) ++ ⟨“ M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((A (K) prefix P) ++ ⟨“ U M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
166	17	s1cld	$⊢ φ \to ⟨“ V ”⟩ \in Word (I \times 2_{𝑜})$
167	100	s1cld	$⊢ φ \to ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜})$
168		ccatass	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜})) \to ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ = (B (L) prefix Q) ++ (⟨“ V ”⟩ ++ ⟨“ M (V) ”⟩)$
169	117 166 167 168	syl3anc	$⊢ φ \to ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ = (B (L) prefix Q) ++ (⟨“ V ”⟩ ++ ⟨“ M (V) ”⟩)$
170		df-s2	$⊢ ⟨“ V M (V) ”⟩ = ⟨“ V ”⟩ ++ ⟨“ M (V) ”⟩$
171	170	oveq2i	$⊢ (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩ = (B (L) prefix Q) ++ (⟨“ V ”⟩ ++ ⟨“ M (V) ”⟩)$
172	169 171	eqtr4di	$⊢ φ \to ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ = (B (L) prefix Q) ++ ⟨“ V M (V) ”⟩$
173	172	oveq1d	$⊢ φ \to (((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) = ((B (L) prefix Q) ++ ⟨“ V M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
174	105 165 173	3eqtr4d	$⊢ φ \to (((A (K) prefix P) ++ ⟨“ U ”⟩) ++ ⟨“ M (U) ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
175	159 174	eqtr3d	$⊢ φ \to ((A (K) prefix P) ++ ⟨“ U ”⟩) ++ (⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
176	175	adantr	$⊢ (φ \land P = Q + 1) \to ((A (K) prefix P) ++ ⟨“ U ”⟩) ++ (⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
177	156	adantr	$⊢ (φ \land P = Q + 1) \to (A (K) prefix P) ++ ⟨“ U ”⟩ \in Word (I \times 2_{𝑜})$
178	157	adantr	$⊢ (φ \land P = Q + 1) \to ⟨“ M (U) ”⟩ \in Word (I \times 2_{𝑜})$
179	114	adantr	$⊢ (φ \land P = Q + 1) \to A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
180		ccatcl	$⊢ (⟨“ M (U) ”⟩ \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \to ⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})$
181	178 179 180	syl2anc	$⊢ (φ \land P = Q + 1) \to ⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})$
182		ccatcl	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V ”⟩ \in Word (I \times 2_{𝑜})) \to (B (L) prefix Q) ++ ⟨“ V ”⟩ \in Word (I \times 2_{𝑜})$
183	117 166 182	syl2anc	$⊢ φ \to (B (L) prefix Q) ++ ⟨“ V ”⟩ \in Word (I \times 2_{𝑜})$
184	183	adantr	$⊢ (φ \land P = Q + 1) \to (B (L) prefix Q) ++ ⟨“ V ”⟩ \in Word (I \times 2_{𝑜})$
185	167	adantr	$⊢ (φ \land P = Q + 1) \to ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜})$
186		ccatcl	$⊢ ((B (L) prefix Q) ++ ⟨“ V ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜})) \to ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜})$
187	184 185 186	syl2anc	$⊢ (φ \land P = Q + 1) \to ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜})$
188	123	adantr	$⊢ (φ \land P = Q + 1) \to B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})$
189		ccatlen	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V ”⟩ \in Word (I \times 2_{𝑜})) \to \|(B (L) prefix Q) ++ ⟨“ V ”⟩\| = \|B (L) prefix Q\| + \|⟨“ V ”⟩\|$
190	117 166 189	syl2anc	$⊢ φ \to \|(B (L) prefix Q) ++ ⟨“ V ”⟩\| = \|B (L) prefix Q\| + \|⟨“ V ”⟩\|$
191		s1len	$⊢ \|⟨“ V ”⟩\| = 1$
192	191	a1i	$⊢ φ \to \|⟨“ V ”⟩\| = 1$
193	128 192	oveq12d	$⊢ φ \to \|B (L) prefix Q\| + \|⟨“ V ”⟩\| = Q + 1$
194	190 193	eqtrd	$⊢ φ \to \|(B (L) prefix Q) ++ ⟨“ V ”⟩\| = Q + 1$
195	126 194	eqeq12d	$⊢ φ \to (\|A (K) prefix P\| = \|(B (L) prefix Q) ++ ⟨“ V ”⟩\| \leftrightarrow P = Q + 1)$
196	195	biimpar	$⊢ (φ \land P = Q + 1) \to \|A (K) prefix P\| = \|(B (L) prefix Q) ++ ⟨“ V ”⟩\|$
197		s1len	$⊢ \|⟨“ U ”⟩\| = 1$
198		s1len	$⊢ \|⟨“ M (V) ”⟩\| = 1$
199	197 198	eqtr4i	$⊢ \|⟨“ U ”⟩\| = \|⟨“ M (V) ”⟩\|$
200	199	a1i	$⊢ (φ \land P = Q + 1) \to \|⟨“ U ”⟩\| = \|⟨“ M (V) ”⟩\|$
201	196 200	oveq12d	$⊢ (φ \land P = Q + 1) \to \|A (K) prefix P\| + \|⟨“ U ”⟩\| = \|(B (L) prefix Q) ++ ⟨“ V ”⟩\| + \|⟨“ M (V) ”⟩\|$
202	108	adantr	$⊢ (φ \land P = Q + 1) \to A (K) prefix P \in Word (I \times 2_{𝑜})$
203	154	adantr	$⊢ (φ \land P = Q + 1) \to ⟨“ U ”⟩ \in Word (I \times 2_{𝑜})$
204		ccatlen	$⊢ (A (K) prefix P \in Word (I \times 2_{𝑜}) \land ⟨“ U ”⟩ \in Word (I \times 2_{𝑜})) \to \|(A (K) prefix P) ++ ⟨“ U ”⟩\| = \|A (K) prefix P\| + \|⟨“ U ”⟩\|$
205	202 203 204	syl2anc	$⊢ (φ \land P = Q + 1) \to \|(A (K) prefix P) ++ ⟨“ U ”⟩\| = \|A (K) prefix P\| + \|⟨“ U ”⟩\|$
206		ccatlen	$⊢ ((B (L) prefix Q) ++ ⟨“ V ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜})) \to \|((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩\| = \|(B (L) prefix Q) ++ ⟨“ V ”⟩\| + \|⟨“ M (V) ”⟩\|$
207	184 185 206	syl2anc	$⊢ (φ \land P = Q + 1) \to \|((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩\| = \|(B (L) prefix Q) ++ ⟨“ V ”⟩\| + \|⟨“ M (V) ”⟩\|$
208	201 205 207	3eqtr4d	$⊢ (φ \land P = Q + 1) \to \|(A (K) prefix P) ++ ⟨“ U ”⟩\| = \|((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩\|$
209		ccatopth	$⊢ (((A (K) prefix P) ++ ⟨“ U ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})) \land (((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜}) \land B (L) substr ⟨Q, \|B (L)\|⟩ \in Word (I \times 2_{𝑜})) \land \|(A (K) prefix P) ++ ⟨“ U ”⟩\| = \|((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩\|) \to (((A (K) prefix P) ++ ⟨“ U ”⟩) ++ (⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \leftrightarrow ((A (K) prefix P) ++ ⟨“ U ”⟩ = ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ \land ⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨Q, \|B (L)\|⟩))$
210	177 181 187 188 208 209	syl221anc	$⊢ (φ \land P = Q + 1) \to (((A (K) prefix P) ++ ⟨“ U ”⟩) ++ (⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩) ++ (B (L) substr ⟨Q, \|B (L)\|⟩) \leftrightarrow ((A (K) prefix P) ++ ⟨“ U ”⟩ = ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ \land ⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨Q, \|B (L)\|⟩))$
211	176 210	mpbid	$⊢ (φ \land P = Q + 1) \to ((A (K) prefix P) ++ ⟨“ U ”⟩ = ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ \land ⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨Q, \|B (L)\|⟩)$
212	211	simpld	$⊢ (φ \land P = Q + 1) \to (A (K) prefix P) ++ ⟨“ U ”⟩ = ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩$
213		ccatopth	$⊢ ((A (K) prefix P \in Word (I \times 2_{𝑜}) \land ⟨“ U ”⟩ \in Word (I \times 2_{𝑜})) \land ((B (L) prefix Q) ++ ⟨“ V ”⟩ \in Word (I \times 2_{𝑜}) \land ⟨“ M (V) ”⟩ \in Word (I \times 2_{𝑜})) \land \|A (K) prefix P\| = \|(B (L) prefix Q) ++ ⟨“ V ”⟩\|) \to ((A (K) prefix P) ++ ⟨“ U ”⟩ = ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ \leftrightarrow (A (K) prefix P = (B (L) prefix Q) ++ ⟨“ V ”⟩ \land ⟨“ U ”⟩ = ⟨“ M (V) ”⟩))$
214	202 203 184 185 196 213	syl221anc	$⊢ (φ \land P = Q + 1) \to ((A (K) prefix P) ++ ⟨“ U ”⟩ = ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ ⟨“ M (V) ”⟩ \leftrightarrow (A (K) prefix P = (B (L) prefix Q) ++ ⟨“ V ”⟩ \land ⟨“ U ”⟩ = ⟨“ M (V) ”⟩))$
215	212 214	mpbid	$⊢ (φ \land P = Q + 1) \to (A (K) prefix P = (B (L) prefix Q) ++ ⟨“ V ”⟩ \land ⟨“ U ”⟩ = ⟨“ M (V) ”⟩)$
216	215	simpld	$⊢ (φ \land P = Q + 1) \to A (K) prefix P = (B (L) prefix Q) ++ ⟨“ V ”⟩$
217	216	oveq1d	$⊢ (φ \land P = Q + 1) \to (A (K) prefix P) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
218	117	adantr	$⊢ (φ \land P = Q + 1) \to B (L) prefix Q \in Word (I \times 2_{𝑜})$
219	166	adantr	$⊢ (φ \land P = Q + 1) \to ⟨“ V ”⟩ \in Word (I \times 2_{𝑜})$
220		ccatass	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land ⟨“ V ”⟩ \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨P, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \to ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) prefix Q) ++ (⟨“ V ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))$
221	218 219 179 220	syl3anc	$⊢ (φ \land P = Q + 1) \to ((B (L) prefix Q) ++ ⟨“ V ”⟩) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) prefix Q) ++ (⟨“ V ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩))$
222	215	simprd	$⊢ (φ \land P = Q + 1) \to ⟨“ U ”⟩ = ⟨“ M (V) ”⟩$
223		s111	$⊢ (U \in (I \times 2_{𝑜}) \land M (V) \in (I \times 2_{𝑜})) \to (⟨“ U ”⟩ = ⟨“ M (V) ”⟩ \leftrightarrow U = M (V))$
224	16 100 223	syl2anc	$⊢ φ \to (⟨“ U ”⟩ = ⟨“ M (V) ”⟩ \leftrightarrow U = M (V))$
225	224	adantr	$⊢ (φ \land P = Q + 1) \to (⟨“ U ”⟩ = ⟨“ M (V) ”⟩ \leftrightarrow U = M (V))$
226	222 225	mpbid	$⊢ (φ \land P = Q + 1) \to U = M (V)$
227	226	fveq2d	$⊢ (φ \land P = Q + 1) \to M (U) = M (M (V))$
228	3	efgmnvl	$⊢ V \in (I \times 2_{𝑜}) \to M (M (V)) = V$
229	17 228	syl	$⊢ φ \to M (M (V)) = V$
230	229	adantr	$⊢ (φ \land P = Q + 1) \to M (M (V)) = V$
231	227 230	eqtrd	$⊢ (φ \land P = Q + 1) \to M (U) = V$
232	231	s1eqd	$⊢ (φ \land P = Q + 1) \to ⟨“ M (U) ”⟩ = ⟨“ V ”⟩$
233	232	oveq1d	$⊢ (φ \land P = Q + 1) \to ⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = ⟨“ V ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)$
234	211	simprd	$⊢ (φ \land P = Q + 1) \to ⟨“ M (U) ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨Q, \|B (L)\|⟩$
235	233 234	eqtr3d	$⊢ (φ \land P = Q + 1) \to ⟨“ V ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩) = B (L) substr ⟨Q, \|B (L)\|⟩$
236	235	oveq2d	$⊢ (φ \land P = Q + 1) \to (B (L) prefix Q) ++ (⟨“ V ”⟩ ++ (A (K) substr ⟨P, \|A (K)\|⟩)) = (B (L) prefix Q) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
237	217 221 236	3eqtrd	$⊢ (φ \land P = Q + 1) \to (A (K) prefix P) ++ (A (K) substr ⟨P, \|A (K)\|⟩) = (B (L) prefix Q) ++ (B (L) substr ⟨Q, \|B (L)\|⟩)$
238	87 237	mtand	$⊢ φ \to \neg P = Q + 1$
239	238	pm2.21d	$⊢ φ \to (P = Q + 1 \to A (0) = B (0))$
240	15	elfzelzd	$⊢ φ \to Q \in ℤ$
241	240	zcnd	$⊢ φ \to Q \in ℂ$
242		1cnd	$⊢ φ \to 1 \in ℂ$
243	241 242 242	addassd	$⊢ φ \to Q + 1 + 1 = Q + 1 + 1$
244		df-2	$⊢ 2 = 1 + 1$
245	244	oveq2i	$⊢ Q + 2 = Q + 1 + 1$
246	243 245	eqtr4di	$⊢ φ \to Q + 1 + 1 = Q + 2$
247	246	fveq2d	$⊢ φ \to ℤ_{\geq (Q + 1 + 1)} = ℤ_{\geq (Q + 2)}$
248	247	eleq2d	$⊢ φ \to (P \in ℤ_{\geq (Q + 1 + 1)} \leftrightarrow P \in ℤ_{\geq (Q + 2)})$
249	1 2 3 4 5 6	efgsfo	$⊢ S : dom S \underset{onto}{⟶} W$
250		swrdcl	$⊢ A (K) \in Word (I \times 2_{𝑜}) \to A (K) substr ⟨Q + 2, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
251	44 250	syl	$⊢ φ \to A (K) substr ⟨Q + 2, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})$
252		ccatcl	$⊢ (B (L) prefix Q \in Word (I \times 2_{𝑜}) \land A (K) substr ⟨Q + 2, \|A (K)\|⟩ \in Word (I \times 2_{𝑜})) \to (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})$
253	117 251 252	syl2anc	$⊢ φ \to (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) \in Word (I \times 2_{𝑜})$
254	1	efgrcl	$⊢ A (K) \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
255	43 254	syl	$⊢ φ \to (I \in V \land W = Word (I \times 2_{𝑜}))$
256	255	simprd	$⊢ φ \to W = Word (I \times 2_{𝑜})$
257	253 256	eleqtrrd	$⊢ φ \to (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) \in W$
258		foelrn	$⊢ (S : dom S \underset{onto}{⟶} W \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) \in W) \to \exists c \in dom S (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c)$
259	249 257 258	sylancr	$⊢ φ \to \exists c \in dom S (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c)$
260	259	adantr	$⊢ (φ \land P \in ℤ_{\geq (Q + 2)}) \to \exists c \in dom S (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c)$
261	7	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \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)))$
262	8	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to A \in dom S$
263	9	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to B \in dom S$
264	10	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to S (A) = S (B)$
265	11	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to \neg A (0) = B (0)$
266	14	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to P \in (0 \dots \|A (K)\|)$
267	15	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to Q \in (0 \dots \|B (L)\|)$
268	16	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to U \in (I \times 2_{𝑜})$
269	17	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to V \in (I \times 2_{𝑜})$
270	18	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to S (A) = P T (A (K)) U$
271	19	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to S (B) = Q T (B (L)) V$
272	20	ad2antrr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to \neg A (K) = B (L)$
273		simplr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to P \in ℤ_{\geq (Q + 2)}$
274		simprl	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to c \in dom S$
275		simprr	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c)$
276	275	eqcomd	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to S (c) = (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩)$
277	1 2 3 4 5 6 261 262 263 264 265 12 13 266 267 268 269 270 271 272 273 274 276	efgredlemd	$⊢ ((φ \land P \in ℤ_{\geq (Q + 2)}) \land (c \in dom S \land (B (L) prefix Q) ++ (A (K) substr ⟨Q + 2, \|A (K)\|⟩) = S (c))) \to A (0) = B (0)$
278	260 277	rexlimddv	$⊢ (φ \land P \in ℤ_{\geq (Q + 2)}) \to A (0) = B (0)$
279	278	ex	$⊢ φ \to (P \in ℤ_{\geq (Q + 2)} \to A (0) = B (0))$
280	248 279	sylbid	$⊢ φ \to (P \in ℤ_{\geq (Q + 1 + 1)} \to A (0) = B (0))$
281	239 280	jaod	$⊢ φ \to ((P = Q + 1 \lor P \in ℤ_{\geq (Q + 1 + 1)}) \to A (0) = B (0))$
282	153 281	syl5	$⊢ φ \to (P \in ℤ_{\geq (Q + 1)} \to A (0) = B (0))$
283	152 282	jaod	$⊢ φ \to ((P = Q \lor P \in ℤ_{\geq (Q + 1)}) \to A (0) = B (0))$
284	21 283	syl5	$⊢ φ \to (P \in ℤ_{\geq Q} \to A (0) = B (0))$

Metamath Proof Explorer

Theorem efgredlemc

Proof