efgcpbllemb

Description: Lemma for efgrelex . Show that L is an equivalence relation containing all direct extensions of a word, so is closed under .~ . (Contributed by Mario Carneiro, 1-Oct-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))$
	efgcpbllem.1	$⊢ L = \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\}$
Assertion	efgcpbllemb	$⊢ (A \in W \land B \in W) \to \underset{˙}{\sim} \subseteq L$

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		efgcpbllem.1	$⊢ L = \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\}$
8	1 2 3 4	efgval2	$⊢ \underset{˙}{\sim} = ⋂ \{r \| (r Er W \land \forall f \in W ran T (f) \subseteq [f] r)\}$
9	7	relopabiv	$⊢ Rel L$
10	9	a1i	$⊢ (A \in W \land B \in W) \to Rel L$
11	1 2 3 4 5 6 7	efgcpbllema	$⊢ f L g \leftrightarrow (f \in W \land g \in W \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ g) ++ B))$
12	11	simp2bi	$⊢ f L g \to g \in W$
13	12	adantl	$⊢ ((A \in W \land B \in W) \land f L g) \to g \in W$
14	11	simp1bi	$⊢ f L g \to f \in W$
15	14	adantl	$⊢ ((A \in W \land B \in W) \land f L g) \to f \in W$
16	1 2	efger	$⊢ \underset{˙}{\sim} Er W$
17	16	a1i	$⊢ ((A \in W \land B \in W) \land f L g) \to \underset{˙}{\sim} Er W$
18	11	simp3bi	$⊢ f L g \to ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ g) ++ B)$
19	18	adantl	$⊢ ((A \in W \land B \in W) \land f L g) \to ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ g) ++ B)$
20	17 19	ersym	$⊢ ((A \in W \land B \in W) \land f L g) \to ((A ++ g) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B)$
21	1 2 3 4 5 6 7	efgcpbllema	$⊢ g L f \leftrightarrow (g \in W \land f \in W \land ((A ++ g) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B))$
22	13 15 20 21	syl3anbrc	$⊢ ((A \in W \land B \in W) \land f L g) \to g L f$
23	14	ad2antrl	$⊢ ((A \in W \land B \in W) \land (f L g \land g L h)) \to f \in W$
24	1 2 3 4 5 6 7	efgcpbllema	$⊢ g L h \leftrightarrow (g \in W \land h \in W \land ((A ++ g) ++ B) \underset{˙}{\sim} ((A ++ h) ++ B))$
25	24	simp2bi	$⊢ g L h \to h \in W$
26	25	ad2antll	$⊢ ((A \in W \land B \in W) \land (f L g \land g L h)) \to h \in W$
27	16	a1i	$⊢ ((A \in W \land B \in W) \land (f L g \land g L h)) \to \underset{˙}{\sim} Er W$
28	18	ad2antrl	$⊢ ((A \in W \land B \in W) \land (f L g \land g L h)) \to ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ g) ++ B)$
29	24	simp3bi	$⊢ g L h \to ((A ++ g) ++ B) \underset{˙}{\sim} ((A ++ h) ++ B)$
30	29	ad2antll	$⊢ ((A \in W \land B \in W) \land (f L g \land g L h)) \to ((A ++ g) ++ B) \underset{˙}{\sim} ((A ++ h) ++ B)$
31	27 28 30	ertrd	$⊢ ((A \in W \land B \in W) \land (f L g \land g L h)) \to ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ h) ++ B)$
32	1 2 3 4 5 6 7	efgcpbllema	$⊢ f L h \leftrightarrow (f \in W \land h \in W \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ h) ++ B))$
33	23 26 31 32	syl3anbrc	$⊢ ((A \in W \land B \in W) \land (f L g \land g L h)) \to f L h$
34	16	a1i	$⊢ ((A \in W \land B \in W) \land f \in W) \to \underset{˙}{\sim} Er W$
35		fviss	$⊢ I (Word (I \times 2_{𝑜})) \subseteq Word (I \times 2_{𝑜})$
36	1 35	eqsstri	$⊢ W \subseteq Word (I \times 2_{𝑜})$
37		simpll	$⊢ ((A \in W \land B \in W) \land f \in W) \to A \in W$
38	36 37	sselid	$⊢ ((A \in W \land B \in W) \land f \in W) \to A \in Word (I \times 2_{𝑜})$
39		simpr	$⊢ ((A \in W \land B \in W) \land f \in W) \to f \in W$
40	36 39	sselid	$⊢ ((A \in W \land B \in W) \land f \in W) \to f \in Word (I \times 2_{𝑜})$
41		ccatcl	$⊢ (A \in Word (I \times 2_{𝑜}) \land f \in Word (I \times 2_{𝑜})) \to A ++ f \in Word (I \times 2_{𝑜})$
42	38 40 41	syl2anc	$⊢ ((A \in W \land B \in W) \land f \in W) \to A ++ f \in Word (I \times 2_{𝑜})$
43		simplr	$⊢ ((A \in W \land B \in W) \land f \in W) \to B \in W$
44	36 43	sselid	$⊢ ((A \in W \land B \in W) \land f \in W) \to B \in Word (I \times 2_{𝑜})$
45		ccatcl	$⊢ (A ++ f \in Word (I \times 2_{𝑜}) \land B \in Word (I \times 2_{𝑜})) \to (A ++ f) ++ B \in Word (I \times 2_{𝑜})$
46	42 44 45	syl2anc	$⊢ ((A \in W \land B \in W) \land f \in W) \to (A ++ f) ++ B \in Word (I \times 2_{𝑜})$
47	1	efgrcl	$⊢ A \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
48	47	simprd	$⊢ A \in W \to W = Word (I \times 2_{𝑜})$
49	48	ad2antrr	$⊢ ((A \in W \land B \in W) \land f \in W) \to W = Word (I \times 2_{𝑜})$
50	46 49	eleqtrrd	$⊢ ((A \in W \land B \in W) \land f \in W) \to (A ++ f) ++ B \in W$
51	34 50	erref	$⊢ ((A \in W \land B \in W) \land f \in W) \to ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B)$
52	51	ex	$⊢ (A \in W \land B \in W) \to (f \in W \to ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B))$
53	52	pm4.71d	$⊢ (A \in W \land B \in W) \to (f \in W \leftrightarrow (f \in W \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B)))$
54	1 2 3 4 5 6 7	efgcpbllema	$⊢ f L f \leftrightarrow (f \in W \land f \in W \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B))$
55		df-3an	$⊢ (f \in W \land f \in W \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B)) \leftrightarrow ((f \in W \land f \in W) \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B))$
56		anidm	$⊢ (f \in W \land f \in W) \leftrightarrow f \in W$
57	56	anbi1i	$⊢ ((f \in W \land f \in W) \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B)) \leftrightarrow (f \in W \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B))$
58	54 55 57	3bitri	$⊢ f L f \leftrightarrow (f \in W \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ f) ++ B))$
59	53 58	bitr4di	$⊢ (A \in W \land B \in W) \to (f \in W \leftrightarrow f L f)$
60	10 22 33 59	iserd	$⊢ (A \in W \land B \in W) \to L Er W$
61	1 2 3 4	efgtf	$⊢ f \in W \to (T (f) = (a \in (0 \dots \|f\|), b \in (I \times 2_{𝑜}) ⟼ f splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (f) : (0 \dots \|f\|) \times (I \times 2_{𝑜}) ⟶ W)$
62	61	simprd	$⊢ f \in W \to T (f) : (0 \dots \|f\|) \times (I \times 2_{𝑜}) ⟶ W$
63	62	adantl	$⊢ ((A \in W \land B \in W) \land f \in W) \to T (f) : (0 \dots \|f\|) \times (I \times 2_{𝑜}) ⟶ W$
64		ffn	$⊢ T (f) : (0 \dots \|f\|) \times (I \times 2_{𝑜}) ⟶ W \to T (f) Fn ((0 \dots \|f\|) \times (I \times 2_{𝑜}))$
65		ovelrn	$⊢ T (f) Fn ((0 \dots \|f\|) \times (I \times 2_{𝑜})) \to (a \in ran T (f) \leftrightarrow \exists c \in (0 \dots \|f\|) \exists u \in (I \times 2_{𝑜}) a = c T (f) u)$
66	63 64 65	3syl	$⊢ ((A \in W \land B \in W) \land f \in W) \to (a \in ran T (f) \leftrightarrow \exists c \in (0 \dots \|f\|) \exists u \in (I \times 2_{𝑜}) a = c T (f) u)$
67		simplr	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to f \in W$
68	62	ad2antlr	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to T (f) : (0 \dots \|f\|) \times (I \times 2_{𝑜}) ⟶ W$
69		simprl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to c \in (0 \dots \|f\|)$
70		simprr	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to u \in (I \times 2_{𝑜})$
71	68 69 70	fovcdmd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to c T (f) u \in W$
72	50	adantr	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ f) ++ B \in W$
73	37	adantr	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to A \in W$
74	36 73	sselid	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to A \in Word (I \times 2_{𝑜})$
75	40	adantr	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to f \in Word (I \times 2_{𝑜})$
76		pfxcl	$⊢ f \in Word (I \times 2_{𝑜}) \to f prefix c \in Word (I \times 2_{𝑜})$
77	75 76	syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to f prefix c \in Word (I \times 2_{𝑜})$
78		ccatcl	$⊢ (A \in Word (I \times 2_{𝑜}) \land f prefix c \in Word (I \times 2_{𝑜})) \to A ++ (f prefix c) \in Word (I \times 2_{𝑜})$
79	74 77 78	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to A ++ (f prefix c) \in Word (I \times 2_{𝑜})$
80	3	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
81	80	ffvelcdmi	$⊢ u \in (I \times 2_{𝑜}) \to M (u) \in (I \times 2_{𝑜})$
82	81	ad2antll	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to M (u) \in (I \times 2_{𝑜})$
83	70 82	s2cld	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜})$
84		ccatcl	$⊢ (A ++ (f prefix c) \in Word (I \times 2_{𝑜}) \land ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜})) \to (A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜})$
85	79 83 84	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜})$
86		swrdcl	$⊢ f \in Word (I \times 2_{𝑜}) \to f substr ⟨c, \|f\|⟩ \in Word (I \times 2_{𝑜})$
87	75 86	syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to f substr ⟨c, \|f\|⟩ \in Word (I \times 2_{𝑜})$
88	44	adantr	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to B \in Word (I \times 2_{𝑜})$
89		ccatass	$⊢ ((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜}) \land f substr ⟨c, \|f\|⟩ \in Word (I \times 2_{𝑜}) \land B \in Word (I \times 2_{𝑜})) \to (((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩)) ++ B = ((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ ((f substr ⟨c, \|f\|⟩) ++ B)$
90	85 87 88 89	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩)) ++ B = ((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ ((f substr ⟨c, \|f\|⟩) ++ B)$
91		ccatcl	$⊢ (f prefix c \in Word (I \times 2_{𝑜}) \land ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜})) \to (f prefix c) ++ ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜})$
92	77 83 91	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (f prefix c) ++ ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜})$
93		ccatass	$⊢ (A \in Word (I \times 2_{𝑜}) \land (f prefix c) ++ ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜}) \land f substr ⟨c, \|f\|⟩ \in Word (I \times 2_{𝑜})) \to (A ++ ((f prefix c) ++ ⟨“ u M (u) ”⟩)) ++ (f substr ⟨c, \|f\|⟩) = A ++ (((f prefix c) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩))$
94	74 92 87 93	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ ((f prefix c) ++ ⟨“ u M (u) ”⟩)) ++ (f substr ⟨c, \|f\|⟩) = A ++ (((f prefix c) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩))$
95		ccatass	$⊢ (A \in Word (I \times 2_{𝑜}) \land f prefix c \in Word (I \times 2_{𝑜}) \land ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜})) \to (A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩ = A ++ ((f prefix c) ++ ⟨“ u M (u) ”⟩)$
96	74 77 83 95	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩ = A ++ ((f prefix c) ++ ⟨“ u M (u) ”⟩)$
97	96	oveq1d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to ((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩) = (A ++ ((f prefix c) ++ ⟨“ u M (u) ”⟩)) ++ (f substr ⟨c, \|f\|⟩)$
98	1 2 3 4	efgtval	$⊢ (f \in W \land c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜})) \to c T (f) u = f splice ⟨c, c, ⟨“ u M (u) ”⟩⟩$
99	67 69 70 98	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to c T (f) u = f splice ⟨c, c, ⟨“ u M (u) ”⟩⟩$
100		splval	$⊢ (f \in W \land (c \in (0 \dots \|f\|) \land c \in (0 \dots \|f\|) \land ⟨“ u M (u) ”⟩ \in Word (I \times 2_{𝑜}))) \to f splice ⟨c, c, ⟨“ u M (u) ”⟩⟩ = ((f prefix c) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩)$
101	67 69 69 83 100	syl13anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to f splice ⟨c, c, ⟨“ u M (u) ”⟩⟩ = ((f prefix c) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩)$
102	99 101	eqtrd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to c T (f) u = ((f prefix c) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩)$
103	102	oveq2d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to A ++ (c T (f) u) = A ++ (((f prefix c) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩))$
104	94 97 103	3eqtr4rd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to A ++ (c T (f) u) = ((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩)$
105	104	oveq1d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ (c T (f) u)) ++ B = (((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ (f substr ⟨c, \|f\|⟩)) ++ B$
106		lencl	$⊢ A \in Word (I \times 2_{𝑜}) \to \|A\| \in ℕ_{0}$
107	74 106	syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| \in ℕ_{0}$
108		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
109	107 108	eleqtrdi	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| \in ℤ_{\geq 0}$
110		elfznn0	$⊢ c \in (0 \dots \|f\|) \to c \in ℕ_{0}$
111	110	ad2antrl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to c \in ℕ_{0}$
112		uzaddcl	$⊢ (\|A\| \in ℤ_{\geq 0} \land c \in ℕ_{0}) \to \|A\| + c \in ℤ_{\geq 0}$
113	109 111 112	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + c \in ℤ_{\geq 0}$
114	42	adantr	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to A ++ f \in Word (I \times 2_{𝑜})$
115		ccatlen	$⊢ (A ++ f \in Word (I \times 2_{𝑜}) \land B \in Word (I \times 2_{𝑜})) \to \|(A ++ f) ++ B\| = \|A ++ f\| + \|B\|$
116	114 88 115	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|(A ++ f) ++ B\| = \|A ++ f\| + \|B\|$
117		ccatlen	$⊢ (A \in Word (I \times 2_{𝑜}) \land f \in Word (I \times 2_{𝑜})) \to \|A ++ f\| = \|A\| + \|f\|$
118	74 75 117	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A ++ f\| = \|A\| + \|f\|$
119		elfzuz3	$⊢ c \in (0 \dots \|f\|) \to \|f\| \in ℤ_{\geq c}$
120	119	ad2antrl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|f\| \in ℤ_{\geq c}$
121	107	nn0zd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| \in ℤ$
122		eluzadd	$⊢ (\|f\| \in ℤ_{\geq c} \land \|A\| \in ℤ) \to \|f\| + \|A\| \in ℤ_{\geq (c + \|A\|)}$
123	120 121 122	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|f\| + \|A\| \in ℤ_{\geq (c + \|A\|)}$
124		lencl	$⊢ f \in Word (I \times 2_{𝑜}) \to \|f\| \in ℕ_{0}$
125	75 124	syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|f\| \in ℕ_{0}$
126	125	nn0cnd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|f\| \in ℂ$
127	107	nn0cnd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| \in ℂ$
128	126 127	addcomd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|f\| + \|A\| = \|A\| + \|f\|$
129	111	nn0cnd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to c \in ℂ$
130	129 127	addcomd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to c + \|A\| = \|A\| + c$
131	130	fveq2d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to ℤ_{\geq (c + \|A\|)} = ℤ_{\geq (\|A\| + c)}$
132	123 128 131	3eltr3d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + \|f\| \in ℤ_{\geq (\|A\| + c)}$
133	118 132	eqeltrd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A ++ f\| \in ℤ_{\geq (\|A\| + c)}$
134		lencl	$⊢ B \in Word (I \times 2_{𝑜}) \to \|B\| \in ℕ_{0}$
135	88 134	syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|B\| \in ℕ_{0}$
136		uzaddcl	$⊢ (\|A ++ f\| \in ℤ_{\geq (\|A\| + c)} \land \|B\| \in ℕ_{0}) \to \|A ++ f\| + \|B\| \in ℤ_{\geq (\|A\| + c)}$
137	133 135 136	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A ++ f\| + \|B\| \in ℤ_{\geq (\|A\| + c)}$
138	116 137	eqeltrd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|(A ++ f) ++ B\| \in ℤ_{\geq (\|A\| + c)}$
139		elfzuzb	$⊢ \|A\| + c \in (0 \dots \|(A ++ f) ++ B\|) \leftrightarrow (\|A\| + c \in ℤ_{\geq 0} \land \|(A ++ f) ++ B\| \in ℤ_{\geq (\|A\| + c)})$
140	113 138 139	sylanbrc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + c \in (0 \dots \|(A ++ f) ++ B\|)$
141	1 2 3 4	efgtval	$⊢ ((A ++ f) ++ B \in W \land \|A\| + c \in (0 \dots \|(A ++ f) ++ B\|) \land u \in (I \times 2_{𝑜})) \to (\|A\| + c) T ((A ++ f) ++ B) u = ((A ++ f) ++ B) splice ⟨\|A\| + c, \|A\| + c, ⟨“ u M (u) ”⟩⟩$
142	72 140 70 141	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (\|A\| + c) T ((A ++ f) ++ B) u = ((A ++ f) ++ B) splice ⟨\|A\| + c, \|A\| + c, ⟨“ u M (u) ”⟩⟩$
143		wrd0	$⊢ \emptyset \in Word (I \times 2_{𝑜})$
144	143	a1i	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \emptyset \in Word (I \times 2_{𝑜})$
145		ccatcl	$⊢ (f substr ⟨c, \|f\|⟩ \in Word (I \times 2_{𝑜}) \land B \in Word (I \times 2_{𝑜})) \to (f substr ⟨c, \|f\|⟩) ++ B \in Word (I \times 2_{𝑜})$
146	87 88 145	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (f substr ⟨c, \|f\|⟩) ++ B \in Word (I \times 2_{𝑜})$
147		ccatrid	$⊢ A ++ (f prefix c) \in Word (I \times 2_{𝑜}) \to (A ++ (f prefix c)) ++ \emptyset = A ++ (f prefix c)$
148	79 147	syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ (f prefix c)) ++ \emptyset = A ++ (f prefix c)$
149	148	oveq1d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to ((A ++ (f prefix c)) ++ \emptyset) ++ ((f substr ⟨c, \|f\|⟩) ++ B) = (A ++ (f prefix c)) ++ ((f substr ⟨c, \|f\|⟩) ++ B)$
150		ccatass	$⊢ (A ++ (f prefix c) \in Word (I \times 2_{𝑜}) \land f substr ⟨c, \|f\|⟩ \in Word (I \times 2_{𝑜}) \land B \in Word (I \times 2_{𝑜})) \to ((A ++ (f prefix c)) ++ (f substr ⟨c, \|f\|⟩)) ++ B = (A ++ (f prefix c)) ++ ((f substr ⟨c, \|f\|⟩) ++ B)$
151	79 87 88 150	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to ((A ++ (f prefix c)) ++ (f substr ⟨c, \|f\|⟩)) ++ B = (A ++ (f prefix c)) ++ ((f substr ⟨c, \|f\|⟩) ++ B)$
152		ccatass	$⊢ (A \in Word (I \times 2_{𝑜}) \land f prefix c \in Word (I \times 2_{𝑜}) \land f substr ⟨c, \|f\|⟩ \in Word (I \times 2_{𝑜})) \to (A ++ (f prefix c)) ++ (f substr ⟨c, \|f\|⟩) = A ++ ((f prefix c) ++ (f substr ⟨c, \|f\|⟩))$
153	74 77 87 152	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ (f prefix c)) ++ (f substr ⟨c, \|f\|⟩) = A ++ ((f prefix c) ++ (f substr ⟨c, \|f\|⟩))$
154	125 108	eleqtrdi	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|f\| \in ℤ_{\geq 0}$
155		eluzfz2	$⊢ \|f\| \in ℤ_{\geq 0} \to \|f\| \in (0 \dots \|f\|)$
156	154 155	syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|f\| \in (0 \dots \|f\|)$
157		ccatpfx	$⊢ (f \in Word (I \times 2_{𝑜}) \land c \in (0 \dots \|f\|) \land \|f\| \in (0 \dots \|f\|)) \to (f prefix c) ++ (f substr ⟨c, \|f\|⟩) = f prefix \|f\|$
158	75 69 156 157	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (f prefix c) ++ (f substr ⟨c, \|f\|⟩) = f prefix \|f\|$
159		pfxid	$⊢ f \in Word (I \times 2_{𝑜}) \to f prefix \|f\| = f$
160	75 159	syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to f prefix \|f\| = f$
161	158 160	eqtrd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (f prefix c) ++ (f substr ⟨c, \|f\|⟩) = f$
162	161	oveq2d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to A ++ ((f prefix c) ++ (f substr ⟨c, \|f\|⟩)) = A ++ f$
163	153 162	eqtrd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ (f prefix c)) ++ (f substr ⟨c, \|f\|⟩) = A ++ f$
164	163	oveq1d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to ((A ++ (f prefix c)) ++ (f substr ⟨c, \|f\|⟩)) ++ B = (A ++ f) ++ B$
165	149 151 164	3eqtr2rd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ f) ++ B = ((A ++ (f prefix c)) ++ \emptyset) ++ ((f substr ⟨c, \|f\|⟩) ++ B)$
166		ccatlen	$⊢ (A \in Word (I \times 2_{𝑜}) \land f prefix c \in Word (I \times 2_{𝑜})) \to \|A ++ (f prefix c)\| = \|A\| + \|f prefix c\|$
167	74 77 166	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A ++ (f prefix c)\| = \|A\| + \|f prefix c\|$
168		pfxlen	$⊢ (f \in Word (I \times 2_{𝑜}) \land c \in (0 \dots \|f\|)) \to \|f prefix c\| = c$
169	75 69 168	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|f prefix c\| = c$
170	169	oveq2d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + \|f prefix c\| = \|A\| + c$
171	167 170	eqtr2d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + c = \|A ++ (f prefix c)\|$
172		hash0	$⊢ \|\emptyset\| = 0$
173	172	oveq2i	$⊢ \|A\| + c + \|\emptyset\| = \|A\| + c + 0$
174	107 111	nn0addcld	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + c \in ℕ_{0}$
175	174	nn0cnd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + c \in ℂ$
176	175	addridd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + c + 0 = \|A\| + c$
177	173 176	eqtr2id	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to \|A\| + c = \|A\| + c + \|\emptyset\|$
178	79 144 146 83 165 171 177	splval2	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to ((A ++ f) ++ B) splice ⟨\|A\| + c, \|A\| + c, ⟨“ u M (u) ”⟩⟩ = ((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ ((f substr ⟨c, \|f\|⟩) ++ B)$
179	142 178	eqtrd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (\|A\| + c) T ((A ++ f) ++ B) u = ((A ++ (f prefix c)) ++ ⟨“ u M (u) ”⟩) ++ ((f substr ⟨c, \|f\|⟩) ++ B)$
180	90 105 179	3eqtr4d	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ (c T (f) u)) ++ B = (\|A\| + c) T ((A ++ f) ++ B) u$
181	1 2 3 4	efgtf	$⊢ (A ++ f) ++ B \in W \to (T ((A ++ f) ++ B) = (a \in (0 \dots \|(A ++ f) ++ B\|), b \in (I \times 2_{𝑜}) ⟼ ((A ++ f) ++ B) splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T ((A ++ f) ++ B) : (0 \dots \|(A ++ f) ++ B\|) \times (I \times 2_{𝑜}) ⟶ W)$
182	181	simprd	$⊢ (A ++ f) ++ B \in W \to T ((A ++ f) ++ B) : (0 \dots \|(A ++ f) ++ B\|) \times (I \times 2_{𝑜}) ⟶ W$
183		ffn	$⊢ T ((A ++ f) ++ B) : (0 \dots \|(A ++ f) ++ B\|) \times (I \times 2_{𝑜}) ⟶ W \to T ((A ++ f) ++ B) Fn ((0 \dots \|(A ++ f) ++ B\|) \times (I \times 2_{𝑜}))$
184	72 182 183	3syl	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to T ((A ++ f) ++ B) Fn ((0 \dots \|(A ++ f) ++ B\|) \times (I \times 2_{𝑜}))$
185		fnovrn	$⊢ (T ((A ++ f) ++ B) Fn ((0 \dots \|(A ++ f) ++ B\|) \times (I \times 2_{𝑜})) \land \|A\| + c \in (0 \dots \|(A ++ f) ++ B\|) \land u \in (I \times 2_{𝑜})) \to (\|A\| + c) T ((A ++ f) ++ B) u \in ran T ((A ++ f) ++ B)$
186	184 140 70 185	syl3anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (\|A\| + c) T ((A ++ f) ++ B) u \in ran T ((A ++ f) ++ B)$
187	180 186	eqeltrd	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (A ++ (c T (f) u)) ++ B \in ran T ((A ++ f) ++ B)$
188	1 2 3 4	efgi2	$⊢ ((A ++ f) ++ B \in W \land (A ++ (c T (f) u)) ++ B \in ran T ((A ++ f) ++ B)) \to ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ (c T (f) u)) ++ B)$
189	72 187 188	syl2anc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ (c T (f) u)) ++ B)$
190	1 2 3 4 5 6 7	efgcpbllema	$⊢ f L (c T (f) u) \leftrightarrow (f \in W \land c T (f) u \in W \land ((A ++ f) ++ B) \underset{˙}{\sim} ((A ++ (c T (f) u)) ++ B))$
191	67 71 189 190	syl3anbrc	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to f L (c T (f) u)$
192		vex	$⊢ a \in V$
193		vex	$⊢ f \in V$
194	192 193	elec	$⊢ a \in [f] L \leftrightarrow f L a$
195		breq2	$⊢ a = c T (f) u \to (f L a \leftrightarrow f L (c T (f) u))$
196	194 195	bitrid	$⊢ a = c T (f) u \to (a \in [f] L \leftrightarrow f L (c T (f) u))$
197	191 196	syl5ibrcom	$⊢ (((A \in W \land B \in W) \land f \in W) \land (c \in (0 \dots \|f\|) \land u \in (I \times 2_{𝑜}))) \to (a = c T (f) u \to a \in [f] L)$
198	197	rexlimdvva	$⊢ ((A \in W \land B \in W) \land f \in W) \to (\exists c \in (0 \dots \|f\|) \exists u \in (I \times 2_{𝑜}) a = c T (f) u \to a \in [f] L)$
199	66 198	sylbid	$⊢ ((A \in W \land B \in W) \land f \in W) \to (a \in ran T (f) \to a \in [f] L)$
200	199	ssrdv	$⊢ ((A \in W \land B \in W) \land f \in W) \to ran T (f) \subseteq [f] L$
201	200	ralrimiva	$⊢ (A \in W \land B \in W) \to \forall f \in W ran T (f) \subseteq [f] L$
202	1	fvexi	$⊢ W \in V$
203		erex	$⊢ L Er W \to (W \in V \to L \in V)$
204	60 202 203	mpisyl	$⊢ (A \in W \land B \in W) \to L \in V$
205		ereq1	$⊢ r = L \to (r Er W \leftrightarrow L Er W)$
206		eceq2	$⊢ r = L \to [f] r = [f] L$
207	206	sseq2d	$⊢ r = L \to (ran T (f) \subseteq [f] r \leftrightarrow ran T (f) \subseteq [f] L)$
208	207	ralbidv	$⊢ r = L \to (\forall f \in W ran T (f) \subseteq [f] r \leftrightarrow \forall f \in W ran T (f) \subseteq [f] L)$
209	205 208	anbi12d	$⊢ r = L \to ((r Er W \land \forall f \in W ran T (f) \subseteq [f] r) \leftrightarrow (L Er W \land \forall f \in W ran T (f) \subseteq [f] L))$
210	209	elabg	$⊢ L \in V \to (L \in \{r \| (r Er W \land \forall f \in W ran T (f) \subseteq [f] r)\} \leftrightarrow (L Er W \land \forall f \in W ran T (f) \subseteq [f] L))$
211	204 210	syl	$⊢ (A \in W \land B \in W) \to (L \in \{r \| (r Er W \land \forall f \in W ran T (f) \subseteq [f] r)\} \leftrightarrow (L Er W \land \forall f \in W ran T (f) \subseteq [f] L))$
212	60 201 211	mpbir2and	$⊢ (A \in W \land B \in W) \to L \in \{r \| (r Er W \land \forall f \in W ran T (f) \subseteq [f] r)\}$
213		intss1	$⊢ L \in \{r \| (r Er W \land \forall f \in W ran T (f) \subseteq [f] r)\} \to ⋂ \{r \| (r Er W \land \forall f \in W ran T (f) \subseteq [f] r)\} \subseteq L$
214	212 213	syl	$⊢ (A \in W \land B \in W) \to ⋂ \{r \| (r Er W \land \forall f \in W ran T (f) \subseteq [f] r)\} \subseteq L$
215	8 214	eqsstrid	$⊢ (A \in W \land B \in W) \to \underset{˙}{\sim} \subseteq L$

Metamath Proof Explorer

Theorem efgcpbllemb

Proof