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 ⊢ 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
frgpup.w ⊢ W = I ⁡ Word I × 2 𝑜
frgpup.r ⊢ ∼ ˙ = ~ FG ⁡ I
frgpup.g ⊢ G = freeGrp ⁡ I
frgpup.x ⊢ X = Base G
frgpup.e ⊢ E = ran ⁡ g ∈ W ⟼ g ∼ ˙ ∑ H T ∘ g
Assertion frgpupval ⊢ φ ∧ A ∈ W → E ⁡ A ∼ ˙ = ∑ H T ∘ A

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 frgpup.w ⊢ W = I ⁡ Word I × 2 𝑜
8 frgpup.r ⊢ ∼ ˙ = ~ FG ⁡ I
9 frgpup.g ⊢ G = freeGrp ⁡ I
10 frgpup.x ⊢ X = Base G
11 frgpup.e ⊢ E = ran ⁡ g ∈ W ⟼ g ∼ ˙ ∑ H T ∘ g
12 ovexd ⊢ φ ∧ g ∈ W → ∑ H T ∘ g ∈ V
13 7 8 efger ⊢ ∼ ˙ Er W
14 13 a1i ⊢ φ → ∼ ˙ Er W
15 7 fvexi ⊢ W ∈ V
16 15 a1i ⊢ φ → W ∈ V
17 coeq2 ⊢ g = A → T ∘ g = T ∘ A
18 17 oveq2d ⊢ g = A → ∑ H T ∘ g = ∑ H T ∘ A
19 1 2 3 4 5 6 7 8 9 10 11 frgpupf ⊢ φ → E : X ⟶ B
20 19 ffund ⊢ φ → Fun ⁡ E
21 11 12 14 16 18 20 qliftval ⊢ φ ∧ A ∈ W → E ⁡ A ∼ ˙ = ∑ H T ∘ A