This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑇 ∘ 𝐴 ) ) )