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

Metamath Proof Explorer

Theorem frgpuptf

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 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐵 )
Assertion frgpuptf ( 𝜑 → 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )

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 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
8 7 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
9 1 2 grpinvcl ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
10 4 8 9 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
11 8 10 ifcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 2o ) ) → if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ 𝐵 )
12 11 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ 𝐵 )
13 3 fmpo ⊢ ( ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 2o if ( 𝑧 = ∅ , ( 𝐹 ‘ 𝑦 ) , ( 𝑁 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ 𝐵 ↔ 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )
14 12 13 sylib ⊢ ( 𝜑 → 𝑇 : ( 𝐼 × 2o ) ⟶ 𝐵 )