Theorem 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	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
	efgval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
	efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
Assertion	efgtval	⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 × 2o ) ) → ( 𝑁 ( 𝑇 ‘ 𝑋 ) 𝐴 ) = ( 𝑋 splice ⟨ 𝑁 , 𝑁 , ⟨“ 𝐴 ( 𝑀 ‘ 𝐴 ) ”⟩ ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		efgval.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
2		efgval.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
3		efgval2.m	⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ ⟨ 𝑦 , ( 1o ∖ 𝑧 ) ⟩ )
4		efgval2.t	⊢ 𝑇 = ( 𝑣 ∈ 𝑊 ↦ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑣 ) ) , 𝑤 ∈ ( 𝐼 × 2o ) ↦ ( 𝑣 splice ⟨ 𝑛 , 𝑛 , ⟨“ 𝑤 ( 𝑀 ‘ 𝑤 ) ”⟩ ⟩ ) ) )
5	1 2 3 4	efgtf	⊢ ( 𝑋 ∈ 𝑊 → ( ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) ∧ ( 𝑇 ‘ 𝑋 ) : ( ( 0 ... ( ♯ ‘ 𝑋 ) ) × ( 𝐼 × 2o ) ) ⟶ 𝑊 ) )
6	5	simpld	⊢ ( 𝑋 ∈ 𝑊 → ( 𝑇 ‘ 𝑋 ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) )
7	6	oveqd	⊢ ( 𝑋 ∈ 𝑊 → ( 𝑁 ( 𝑇 ‘ 𝑋 ) 𝐴 ) = ( 𝑁 ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) 𝐴 ) )
8		oteq1	⊢ ( 𝑎 = 𝑁 → ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ = ⟨ 𝑁 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ )
9		oteq2	⊢ ( 𝑎 = 𝑁 → ⟨ 𝑁 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ )
10	8 9	eqtrd	⊢ ( 𝑎 = 𝑁 → ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ )
11	10	oveq2d	⊢ ( 𝑎 = 𝑁 → ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ( 𝑋 splice ⟨ 𝑁 , 𝑁 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
12		id	⊢ ( 𝑏 = 𝐴 → 𝑏 = 𝐴 )
13		fveq2	⊢ ( 𝑏 = 𝐴 → ( 𝑀 ‘ 𝑏 ) = ( 𝑀 ‘ 𝐴 ) )
14	12 13	s2eqd	⊢ ( 𝑏 = 𝐴 → ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ = ⟨“ 𝐴 ( 𝑀 ‘ 𝐴 ) ”⟩ )
15	14	oteq3d	⊢ ( 𝑏 = 𝐴 → ⟨ 𝑁 , 𝑁 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ = ⟨ 𝑁 , 𝑁 , ⟨“ 𝐴 ( 𝑀 ‘ 𝐴 ) ”⟩ ⟩ )
16	15	oveq2d	⊢ ( 𝑏 = 𝐴 → ( 𝑋 splice ⟨ 𝑁 , 𝑁 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) = ( 𝑋 splice ⟨ 𝑁 , 𝑁 , ⟨“ 𝐴 ( 𝑀 ‘ 𝐴 ) ”⟩ ⟩ ) )
17		eqid	⊢ ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) = ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) )
18		ovex	⊢ ( 𝑋 splice ⟨ 𝑁 , 𝑁 , ⟨“ 𝐴 ( 𝑀 ‘ 𝐴 ) ”⟩ ⟩ ) ∈ V
19	11 16 17 18	ovmpo	⊢ ( ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 × 2o ) ) → ( 𝑁 ( 𝑎 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) , 𝑏 ∈ ( 𝐼 × 2o ) ↦ ( 𝑋 splice ⟨ 𝑎 , 𝑎 , ⟨“ 𝑏 ( 𝑀 ‘ 𝑏 ) ”⟩ ⟩ ) ) 𝐴 ) = ( 𝑋 splice ⟨ 𝑁 , 𝑁 , ⟨“ 𝐴 ( 𝑀 ‘ 𝐴 ) ”⟩ ⟩ ) )
20	7 19	sylan9eq	⊢ ( ( 𝑋 ∈ 𝑊 ∧ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 × 2o ) ) ) → ( 𝑁 ( 𝑇 ‘ 𝑋 ) 𝐴 ) = ( 𝑋 splice ⟨ 𝑁 , 𝑁 , ⟨“ 𝐴 ( 𝑀 ‘ 𝐴 ) ”⟩ ⟩ ) )
21	20	3impb	⊢ ( ( 𝑋 ∈ 𝑊 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑋 ) ) ∧ 𝐴 ∈ ( 𝐼 × 2o ) ) → ( 𝑁 ( 𝑇 ‘ 𝑋 ) 𝐴 ) = ( 𝑋 splice ⟨ 𝑁 , 𝑁 , ⟨“ 𝐴 ( 𝑀 ‘ 𝐴 ) ”⟩ ⟩ ) )