efgcpbllema

Description: Lemma for efgrelex . Define an auxiliary equivalence relation L such that A L B if there are sequences from A to B passing through the same reduced word. (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	efgcpbllema	$⊢ X L Y \leftrightarrow (X \in W \land Y \in W \land ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B))$

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		oveq2	$⊢ i = X \to A ++ i = A ++ X$
9	8	oveq1d	$⊢ i = X \to (A ++ i) ++ B = (A ++ X) ++ B$
10		oveq2	$⊢ j = Y \to A ++ j = A ++ Y$
11	10	oveq1d	$⊢ j = Y \to (A ++ j) ++ B = (A ++ Y) ++ B$
12	9 11	breqan12d	$⊢ (i = X \land j = Y) \to (((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B) \leftrightarrow ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B))$
13		vex	$⊢ i \in V$
14		vex	$⊢ j \in V$
15	13 14	prss	$⊢ (i \in W \land j \in W) \leftrightarrow \{i, j\} \subseteq W$
16	15	anbi1i	$⊢ ((i \in W \land j \in W) \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B)) \leftrightarrow (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))$
17	16	opabbii	$⊢ \{⟨i, j⟩ \| ((i \in W \land j \in W) \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\} = \{⟨i, j⟩ \| (\{i, j\} \subseteq W \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\}$
18	7 17	eqtr4i	$⊢ L = \{⟨i, j⟩ \| ((i \in W \land j \in W) \land ((A ++ i) ++ B) \underset{˙}{\sim} ((A ++ j) ++ B))\}$
19	12 18	brab2a	$⊢ X L Y \leftrightarrow ((X \in W \land Y \in W) \land ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B))$
20		df-3an	$⊢ (X \in W \land Y \in W \land ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B)) \leftrightarrow ((X \in W \land Y \in W) \land ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B))$
21	19 20	bitr4i	$⊢ X L Y \leftrightarrow (X \in W \land Y \in W \land ((A ++ X) ++ B) \underset{˙}{\sim} ((A ++ Y) ++ B))$

Metamath Proof Explorer

Theorem efgcpbllema

Proof