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=BaseH
frgpup3.u ⊢U=varFGrp⁡I
Assertion frgpup3 ⊢H∈Grp∧I∈V∧F:I⟶B→∃!m∈GGrpHomHm∘U=F

Proof

Step Hyp Ref Expression
1 frgpup3.g ⊢G=freeGrp⁡I
2 frgpup3.b ⊢B=BaseH
3 frgpup3.u ⊢U=varFGrp⁡I
4 eqid ⊢invg⁡H=invg⁡H
5 eqid ⊢y∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y=y∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡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⁡WordI×2𝑜=I⁡WordI×2𝑜
10 eqid ⊢~FG⁡I=~FG⁡I
11 eqid ⊢BaseG=BaseG
12 eqid ⊢ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g=ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡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⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∈GGrpHomH
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⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g⁡U⁡k=F⁡k
19 18 mpteq2dva ⊢H∈Grp∧I∈V∧F:I⟶B→k∈I⟼ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g⁡U⁡k=k∈I⟼F⁡k
20 11 2 ghmf ⊢ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∈GGrpHomH→ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g:BaseG⟶B
21 13 20 syl ⊢H∈Grp∧I∈V∧F:I⟶B→ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g:BaseG⟶B
22 10 3 1 11 vrgpf ⊢I∈V→U:I⟶BaseG
23 7 22 syl ⊢H∈Grp∧I∈V∧F:I⟶B→U:I⟶BaseG
24 fcompt ⊢ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g:BaseG⟶B∧U:I⟶BaseG→ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∘U=k∈I⟼ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g⁡U⁡k
25 21 23 24 syl2anc ⊢H∈Grp∧I∈V∧F:I⟶B→ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∘U=k∈I⟼ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡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⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∘U=F
28 6 adantr ⊢H∈Grp∧I∈V∧F:I⟶B∧m∈GGrpHomH∧m∘U=F→H∈Grp
29 7 adantr ⊢H∈Grp∧I∈V∧F:I⟶B∧m∈GGrpHomH∧m∘U=F→I∈V
30 8 adantr ⊢H∈Grp∧I∈V∧F:I⟶B∧m∈GGrpHomH∧m∘U=F→F:I⟶B
31 simprl ⊢H∈Grp∧I∈V∧F:I⟶B∧m∈GGrpHomH∧m∘U=F→m∈GGrpHomH
32 simprr ⊢H∈Grp∧I∈V∧F:I⟶B∧m∈GGrpHomH∧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∈GGrpHomH∧m∘U=F→m=ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g
34 33 expr ⊢H∈Grp∧I∈V∧F:I⟶B∧m∈GGrpHomH→m∘U=F→m=ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g
35 34 ralrimiva ⊢H∈Grp∧I∈V∧F:I⟶B→∀m∈GGrpHomHm∘U=F→m=ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g
36 coeq1 ⊢m=ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g→m∘U=ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∘U
37 36 eqeq1d ⊢m=ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g→m∘U=F↔ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∘U=F
38 37 eqreu ⊢ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∈GGrpHomH∧ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g∘U=F∧∀m∈GGrpHomHm∘U=F→m=ran⁡g∈I⁡WordI×2𝑜⟼g~FG⁡I∑Hy∈I,z∈2𝑜⟼ifz=∅F⁡yinvg⁡H⁡F⁡y∘g→∃!m∈GGrpHomHm∘U=F
39 13 27 35 38 syl3anc ⊢H∈Grp∧I∈V∧F:I⟶B→∃!m∈GGrpHomHm∘U=F