Metamath Proof Explorer

Theorem frgpup3

Description: Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses frgpup3.g ⊢ G = freeGrp ⁡ I
frgpup3.b ⊢ B = Base H
frgpup3.u ⊢ U = var FGrp ⁡ I
Assertion frgpup3 ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → ∃! m ∈ G GrpHom H m ∘ U = F

Proof

Step Hyp Ref Expression
1 frgpup3.g ⊢ G = freeGrp ⁡ I
2 frgpup3.b ⊢ B = Base H
3 frgpup3.u ⊢ U = var FGrp ⁡ I
4 eqid ⊢ inv g ⁡ H = inv g ⁡ H
5 eqid ⊢ y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y = y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y
6 simp1 ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → H ∈ Grp
7 simp2 ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → I ∈ V
8 simp3 ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → F : I ⟶ B
9 eqid ⊢ I ⁡ Word I × 2 𝑜 = I ⁡ Word I × 2 𝑜
10 eqid ⊢ ~ FG ⁡ I = ~ FG ⁡ I
11 eqid ⊢ Base G = Base G
12 eqid ⊢ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g = ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g
13 2 4 5 6 7 8 9 10 1 11 12 frgpup1 ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∈ G GrpHom H
14 6 adantr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ k ∈ I → H ∈ Grp
15 7 adantr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ k ∈ I → I ∈ V
16 8 adantr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ k ∈ I → F : I ⟶ B
17 simpr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ k ∈ I → k ∈ I
18 2 4 5 14 15 16 9 10 1 11 12 3 17 frgpup2 ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ k ∈ I → ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ⁡ U ⁡ k = F ⁡ k
19 18 mpteq2dva ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → k ∈ I ⟼ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ⁡ U ⁡ k = k ∈ I ⟼ F ⁡ k
20 11 2 ghmf ⊢ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∈ G GrpHom H → ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g : Base G ⟶ B
21 13 20 syl ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g : Base G ⟶ B
22 10 3 1 11 vrgpf ⊢ I ∈ V → U : I ⟶ Base G
23 7 22 syl ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → U : I ⟶ Base G
24 fcompt ⊢ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g : Base G ⟶ B ∧ U : I ⟶ Base G → ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∘ U = k ∈ I ⟼ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ⁡ U ⁡ k
25 21 23 24 syl2anc ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∘ U = k ∈ I ⟼ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ⁡ U ⁡ k
26 8 feqmptd ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → F = k ∈ I ⟼ F ⁡ k
27 19 25 26 3eqtr4d ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∘ U = F
28 6 adantr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ m ∈ G GrpHom H ∧ m ∘ U = F → H ∈ Grp
29 7 adantr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ m ∈ G GrpHom H ∧ m ∘ U = F → I ∈ V
30 8 adantr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ m ∈ G GrpHom H ∧ m ∘ U = F → F : I ⟶ B
31 simprl ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ m ∈ G GrpHom H ∧ m ∘ U = F → m ∈ G GrpHom H
32 simprr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ m ∈ G GrpHom H ∧ m ∘ U = F → m ∘ U = F
33 2 4 5 28 29 30 9 10 1 11 12 3 31 32 frgpup3lem ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ m ∈ G GrpHom H ∧ m ∘ U = F → m = ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g
34 33 expr ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B ∧ m ∈ G GrpHom H → m ∘ U = F → m = ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g
35 34 ralrimiva ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → ∀ m ∈ G GrpHom H m ∘ U = F → m = ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g
36 coeq1 ⊢ m = ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g → m ∘ U = ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∘ U
37 36 eqeq1d ⊢ m = ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g → m ∘ U = F ↔ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∘ U = F
38 37 eqreu ⊢ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∈ G GrpHom H ∧ ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g ∘ U = F ∧ ∀ m ∈ G GrpHom H m ∘ U = F → m = ran ⁡ g ∈ I ⁡ Word I × 2 𝑜 ⟼ g ~ FG ⁡ I ∑ H y ∈ I , z ∈ 2 𝑜 ⟼ if z = ∅ F ⁡ y inv g ⁡ H ⁡ F ⁡ y ∘ g → ∃! m ∈ G GrpHom H m ∘ U = F
39 13 27 35 38 syl3anc ⊢ H ∈ Grp ∧ I ∈ V ∧ F : I ⟶ B → ∃! m ∈ G GrpHom H m ∘ U = F