Theorem frgpupval

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	frgpup.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
	frgpup.n	⊢ 𝑁 = ( invg ‘ 𝐻 )
	frgpup.t	⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
	frgpup.h	⊢ ( 𝜑 → 𝐻 ∈ Grp )
	frgpup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	frgpup.a	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
	frgpup.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
	frgpup.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
	frgpup.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
	frgpup.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	frgpup.e	⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ⟩ )
Assertion	frgpupval	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐸 ‘ [ 𝐴 ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		frgpup.b	⊢ 𝐵 = ( Base ‘ 𝐻 )
2		frgpup.n	⊢ 𝑁 = ( invg ‘ 𝐻 )
3		frgpup.t	⊢ 𝑇 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
4		frgpup.h	⊢ ( 𝜑 → 𝐻 ∈ Grp )
5		frgpup.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		frgpup.a	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
7		frgpup.w	⊢ 𝑊 = ( I ‘ Word ( 𝐼 × 2o ) )
8		frgpup.r	⊢ ∼ = ( ~FG ‘ 𝐼 )
9		frgpup.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
10		frgpup.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
11		frgpup.e	⊢ 𝐸 = ran ( 𝑔 ∈ 𝑊 ↦ ⟨ [ 𝑔 ] ∼ , ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ⟩ )
12		ovexd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑊 ) → ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) ∈ V )
13	7 8	efger	⊢ ∼ Er 𝑊
14	13	a1i	⊢ ( 𝜑 → ∼ Er 𝑊 )
15	7	fvexi	⊢ 𝑊 ∈ V
16	15	a1i	⊢ ( 𝜑 → 𝑊 ∈ V )
17		coeq2	⊢ ( 𝑔 = 𝐴 → ( 𝑇 ∘ 𝑔 ) = ( 𝑇 ∘ 𝐴 ) )
18	17	oveq2d	⊢ ( 𝑔 = 𝐴 → ( 𝐻 Σg ( 𝑇 ∘ 𝑔 ) ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) )
19	1 2 3 4 5 6 7 8 9 10 11	frgpupf	⊢ ( 𝜑 → 𝐸 : 𝑋 ⟶ 𝐵 )
20	19	ffund	⊢ ( 𝜑 → Fun 𝐸 )
21	11 12 14 16 18 20	qliftval	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑊 ) → ( 𝐸 ‘ [ 𝐴 ] ∼ ) = ( 𝐻 Σg ( 𝑇 ∘ 𝐴 ) ) )