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 ⊢ B = Base H
frgpup.n ⊢ N = inv g ⁡ H
frgpup.t ⊢ T = y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y N ⁡ F ⁡ y
frgpup.h ⊢ φ → H ∈ Grp
frgpup.i ⊢ φ → I ∈ V
frgpup.a ⊢ φ → F : I ⟶ B
Assertion frgpuptf ⊢ φ → T : I × 2 𝑜 ⟶ B

Proof

Step Hyp Ref Expression
1 frgpup.b ⊢ B = Base H
2 frgpup.n ⊢ N = inv g ⁡ H
3 frgpup.t ⊢ T = y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y N ⁡ F ⁡ y
4 frgpup.h ⊢ φ → H ∈ Grp
5 frgpup.i ⊢ φ → I ∈ V
6 frgpup.a ⊢ φ → F : I ⟶ B
7 6 ffvelcdmda ⊢ φ ∧ y ∈ I → F ⁡ y ∈ B
8 7 adantrr ⊢ φ ∧ y ∈ I ∧ z ∈ 2 𝑜 → F ⁡ y ∈ B
9 1 2 grpinvcl ⊢ H ∈ Grp ∧ F ⁡ y ∈ B → N ⁡ F ⁡ y ∈ B
10 4 8 9 syl2an2r ⊢ φ ∧ y ∈ I ∧ z ∈ 2 𝑜 → N ⁡ F ⁡ y ∈ B
11 8 10 ifcld ⊢ φ ∧ y ∈ I ∧ z ∈ 2 𝑜 → if z = ∅ F ⁡ y N ⁡ F ⁡ y ∈ B
12 11 ralrimivva ⊢ φ → ∀ y ∈ I ∀ z ∈ 2 𝑜 if z = ∅ F ⁡ y N ⁡ F ⁡ y ∈ B
13 3 fmpo ⊢ ∀ y ∈ I ∀ z ∈ 2 𝑜 if z = ∅ F ⁡ y N ⁡ F ⁡ y ∈ B ↔ T : I × 2 𝑜 ⟶ B
14 12 13 sylib ⊢ φ → T : I × 2 𝑜 ⟶ B