Metamath Proof Explorer


Theorem frgp0

Description: The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 27-Feb-2016)

Ref Expression
Hypotheses frgp0.m G=freeGrpI
frgp0.r ˙=~FGI
Assertion frgp0 IVGGrp˙=0G

Proof

Step Hyp Ref Expression
1 frgp0.m G=freeGrpI
2 frgp0.r ˙=~FGI
3 eqid freeMndI×2𝑜=freeMndI×2𝑜
4 1 3 2 frgpval IVG=freeMndI×2𝑜/𝑠˙
5 2on 2𝑜On
6 xpexg IV2𝑜OnI×2𝑜V
7 5 6 mpan2 IVI×2𝑜V
8 eqid BasefreeMndI×2𝑜=BasefreeMndI×2𝑜
9 3 8 frmdbas I×2𝑜VBasefreeMndI×2𝑜=WordI×2𝑜
10 7 9 syl IVBasefreeMndI×2𝑜=WordI×2𝑜
11 10 eqcomd IVWordI×2𝑜=BasefreeMndI×2𝑜
12 eqidd IV+freeMndI×2𝑜=+freeMndI×2𝑜
13 eqid IWordI×2𝑜=IWordI×2𝑜
14 13 2 efger ˙ErIWordI×2𝑜
15 wrdexg I×2𝑜VWordI×2𝑜V
16 fvi WordI×2𝑜VIWordI×2𝑜=WordI×2𝑜
17 7 15 16 3syl IVIWordI×2𝑜=WordI×2𝑜
18 ereq2 IWordI×2𝑜=WordI×2𝑜˙ErIWordI×2𝑜˙ErWordI×2𝑜
19 17 18 syl IV˙ErIWordI×2𝑜˙ErWordI×2𝑜
20 14 19 mpbii IV˙ErWordI×2𝑜
21 fvexd IVfreeMndI×2𝑜V
22 eqid +freeMndI×2𝑜=+freeMndI×2𝑜
23 1 3 2 22 frgpcpbl a˙bc˙da+freeMndI×2𝑜c˙b+freeMndI×2𝑜d
24 23 a1i IVa˙bc˙da+freeMndI×2𝑜c˙b+freeMndI×2𝑜d
25 3 frmdmnd I×2𝑜VfreeMndI×2𝑜Mnd
26 7 25 syl IVfreeMndI×2𝑜Mnd
27 26 3ad2ant1 IVxWordI×2𝑜yWordI×2𝑜freeMndI×2𝑜Mnd
28 simp2 IVxWordI×2𝑜yWordI×2𝑜xWordI×2𝑜
29 11 3ad2ant1 IVxWordI×2𝑜yWordI×2𝑜WordI×2𝑜=BasefreeMndI×2𝑜
30 28 29 eleqtrd IVxWordI×2𝑜yWordI×2𝑜xBasefreeMndI×2𝑜
31 simp3 IVxWordI×2𝑜yWordI×2𝑜yWordI×2𝑜
32 31 29 eleqtrd IVxWordI×2𝑜yWordI×2𝑜yBasefreeMndI×2𝑜
33 8 22 mndcl freeMndI×2𝑜MndxBasefreeMndI×2𝑜yBasefreeMndI×2𝑜x+freeMndI×2𝑜yBasefreeMndI×2𝑜
34 27 30 32 33 syl3anc IVxWordI×2𝑜yWordI×2𝑜x+freeMndI×2𝑜yBasefreeMndI×2𝑜
35 34 29 eleqtrrd IVxWordI×2𝑜yWordI×2𝑜x+freeMndI×2𝑜yWordI×2𝑜
36 20 adantr IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜˙ErWordI×2𝑜
37 26 adantr IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜freeMndI×2𝑜Mnd
38 34 3adant3r3 IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜x+freeMndI×2𝑜yBasefreeMndI×2𝑜
39 simpr3 IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜zWordI×2𝑜
40 11 adantr IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜WordI×2𝑜=BasefreeMndI×2𝑜
41 39 40 eleqtrd IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜zBasefreeMndI×2𝑜
42 8 22 mndcl freeMndI×2𝑜Mndx+freeMndI×2𝑜yBasefreeMndI×2𝑜zBasefreeMndI×2𝑜x+freeMndI×2𝑜y+freeMndI×2𝑜zBasefreeMndI×2𝑜
43 37 38 41 42 syl3anc IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜x+freeMndI×2𝑜y+freeMndI×2𝑜zBasefreeMndI×2𝑜
44 43 40 eleqtrrd IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜x+freeMndI×2𝑜y+freeMndI×2𝑜zWordI×2𝑜
45 36 44 erref IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜x+freeMndI×2𝑜y+freeMndI×2𝑜z˙x+freeMndI×2𝑜y+freeMndI×2𝑜z
46 30 3adant3r3 IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜xBasefreeMndI×2𝑜
47 32 3adant3r3 IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜yBasefreeMndI×2𝑜
48 8 22 mndass freeMndI×2𝑜MndxBasefreeMndI×2𝑜yBasefreeMndI×2𝑜zBasefreeMndI×2𝑜x+freeMndI×2𝑜y+freeMndI×2𝑜z=x+freeMndI×2𝑜y+freeMndI×2𝑜z
49 37 46 47 41 48 syl13anc IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜x+freeMndI×2𝑜y+freeMndI×2𝑜z=x+freeMndI×2𝑜y+freeMndI×2𝑜z
50 45 49 breqtrd IVxWordI×2𝑜yWordI×2𝑜zWordI×2𝑜x+freeMndI×2𝑜y+freeMndI×2𝑜z˙x+freeMndI×2𝑜y+freeMndI×2𝑜z
51 wrd0 WordI×2𝑜
52 51 a1i IVWordI×2𝑜
53 51 11 eleqtrid IVBasefreeMndI×2𝑜
54 53 adantr IVxWordI×2𝑜BasefreeMndI×2𝑜
55 11 eleq2d IVxWordI×2𝑜xBasefreeMndI×2𝑜
56 55 biimpa IVxWordI×2𝑜xBasefreeMndI×2𝑜
57 3 8 22 frmdadd BasefreeMndI×2𝑜xBasefreeMndI×2𝑜+freeMndI×2𝑜x=++x
58 54 56 57 syl2anc IVxWordI×2𝑜+freeMndI×2𝑜x=++x
59 ccatlid xWordI×2𝑜++x=x
60 59 adantl IVxWordI×2𝑜++x=x
61 58 60 eqtrd IVxWordI×2𝑜+freeMndI×2𝑜x=x
62 20 adantr IVxWordI×2𝑜˙ErWordI×2𝑜
63 simpr IVxWordI×2𝑜xWordI×2𝑜
64 62 63 erref IVxWordI×2𝑜x˙x
65 61 64 eqbrtrd IVxWordI×2𝑜+freeMndI×2𝑜x˙x
66 revcl xWordI×2𝑜reversexWordI×2𝑜
67 66 adantl IVxWordI×2𝑜reversexWordI×2𝑜
68 eqid yI,z2𝑜y1𝑜z=yI,z2𝑜y1𝑜z
69 68 efgmf yI,z2𝑜y1𝑜z:I×2𝑜I×2𝑜
70 69 a1i IVxWordI×2𝑜yI,z2𝑜y1𝑜z:I×2𝑜I×2𝑜
71 wrdco reversexWordI×2𝑜yI,z2𝑜y1𝑜z:I×2𝑜I×2𝑜yI,z2𝑜y1𝑜zreversexWordI×2𝑜
72 67 70 71 syl2anc IVxWordI×2𝑜yI,z2𝑜y1𝑜zreversexWordI×2𝑜
73 11 adantr IVxWordI×2𝑜WordI×2𝑜=BasefreeMndI×2𝑜
74 72 73 eleqtrd IVxWordI×2𝑜yI,z2𝑜y1𝑜zreversexBasefreeMndI×2𝑜
75 3 8 22 frmdadd yI,z2𝑜y1𝑜zreversexBasefreeMndI×2𝑜xBasefreeMndI×2𝑜yI,z2𝑜y1𝑜zreversex+freeMndI×2𝑜x=yI,z2𝑜y1𝑜zreversex++x
76 74 56 75 syl2anc IVxWordI×2𝑜yI,z2𝑜y1𝑜zreversex+freeMndI×2𝑜x=yI,z2𝑜y1𝑜zreversex++x
77 17 eleq2d IVxIWordI×2𝑜xWordI×2𝑜
78 77 biimpar IVxWordI×2𝑜xIWordI×2𝑜
79 eqid vIWordI×2𝑜n0v,wI×2𝑜vsplicenn⟨“wyI,z2𝑜y1𝑜zw”⟩=vIWordI×2𝑜n0v,wI×2𝑜vsplicenn⟨“wyI,z2𝑜y1𝑜zw”⟩
80 13 2 68 79 efginvrel1 xIWordI×2𝑜yI,z2𝑜y1𝑜zreversex++x˙
81 78 80 syl IVxWordI×2𝑜yI,z2𝑜y1𝑜zreversex++x˙
82 76 81 eqbrtrd IVxWordI×2𝑜yI,z2𝑜y1𝑜zreversex+freeMndI×2𝑜x˙
83 4 11 12 20 21 24 35 50 52 65 72 82 qusgrp2 IVGGrp˙=0G