efgtval

Description: Value of the extension function, which maps a word (a representation of the group element as a sequence of elements and their inverses) to its direct extensions, defined as the original representation with an element and its inverse inserted somewhere in the string. (Contributed by Mario Carneiro, 29-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) ”⟩⟩))$
Assertion	efgtval	$⊢ (X \in W \land N \in (0 \dots \|X\|) \land A \in (I \times 2_{𝑜})) \to N T (X) A = X splice ⟨N, N, ⟨“ A M (A) ”⟩⟩$

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	1 2 3 4	efgtf	$⊢ X \in W \to (T (X) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (X) : (0 \dots \|X\|) \times (I \times 2_{𝑜}) ⟶ W)$
6	5	simpld	$⊢ X \in W \to T (X) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
7	6	oveqd	$⊢ X \in W \to N T (X) A = N (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) A$
8		oteq1	$⊢ a = N \to ⟨a, a, ⟨“ b M (b) ”⟩⟩ = ⟨N, a, ⟨“ b M (b) ”⟩⟩$
9		oteq2	$⊢ a = N \to ⟨N, a, ⟨“ b M (b) ”⟩⟩ = ⟨N, N, ⟨“ b M (b) ”⟩⟩$
10	8 9	eqtrd	$⊢ a = N \to ⟨a, a, ⟨“ b M (b) ”⟩⟩ = ⟨N, N, ⟨“ b M (b) ”⟩⟩$
11	10	oveq2d	$⊢ a = N \to X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ = X splice ⟨N, N, ⟨“ b M (b) ”⟩⟩$
12		id	$⊢ b = A \to b = A$
13		fveq2	$⊢ b = A \to M (b) = M (A)$
14	12 13	s2eqd	$⊢ b = A \to ⟨“ b M (b) ”⟩ = ⟨“ A M (A) ”⟩$
15	14	oteq3d	$⊢ b = A \to ⟨N, N, ⟨“ b M (b) ”⟩⟩ = ⟨N, N, ⟨“ A M (A) ”⟩⟩$
16	15	oveq2d	$⊢ b = A \to X splice ⟨N, N, ⟨“ b M (b) ”⟩⟩ = X splice ⟨N, N, ⟨“ A M (A) ”⟩⟩$
17		eqid	$⊢ (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) = (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
18		ovex	$⊢ X splice ⟨N, N, ⟨“ A M (A) ”⟩⟩ \in V$
19	11 16 17 18	ovmpo	$⊢ (N \in (0 \dots \|X\|) \land A \in (I \times 2_{𝑜})) \to N (a \in (0 \dots \|X\|), b \in (I \times 2_{𝑜}) ⟼ X splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) A = X splice ⟨N, N, ⟨“ A M (A) ”⟩⟩$
20	7 19	sylan9eq	$⊢ (X \in W \land (N \in (0 \dots \|X\|) \land A \in (I \times 2_{𝑜}))) \to N T (X) A = X splice ⟨N, N, ⟨“ A M (A) ”⟩⟩$
21	20	3impb	$⊢ (X \in W \land N \in (0 \dots \|X\|) \land A \in (I \times 2_{𝑜})) \to N T (X) A = X splice ⟨N, N, ⟨“ A M (A) ”⟩⟩$

Metamath Proof Explorer

Theorem efgtval

Proof