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 ) ⟶ 𝐵 )