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