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 = ( freeGrp ` I )
frgp0.r 
|- .~ = ( ~FG ` I )
Assertion frgp0 
|- ( I e. V -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )

Proof

Step Hyp Ref Expression
1 frgp0.m 
 |-  G = ( freeGrp ` I )
2 frgp0.r 
 |-  .~ = ( ~FG ` I )
3 eqid 
 |-  ( freeMnd ` ( I X. 2o ) ) = ( freeMnd ` ( I X. 2o ) )
4 1 3 2 frgpval 
 |-  ( I e. V -> G = ( ( freeMnd ` ( I X. 2o ) ) /s .~ ) )
5 2on 
 |-  2o e. On
6 xpexg 
 |-  ( ( I e. V /\ 2o e. On ) -> ( I X. 2o ) e. _V )
7 5 6 mpan2 
 |-  ( I e. V -> ( I X. 2o ) e. _V )
8 eqid 
 |-  ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) )
9 3 8 frmdbas 
 |-  ( ( I X. 2o ) e. _V -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
10 7 9 syl 
 |-  ( I e. V -> ( Base ` ( freeMnd ` ( I X. 2o ) ) ) = Word ( I X. 2o ) )
11 10 eqcomd 
 |-  ( I e. V -> Word ( I X. 2o ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
12 eqidd 
 |-  ( I e. V -> ( +g ` ( freeMnd ` ( I X. 2o ) ) ) = ( +g ` ( freeMnd ` ( I X. 2o ) ) ) )
13 eqid 
 |-  ( _I ` Word ( I X. 2o ) ) = ( _I ` Word ( I X. 2o ) )
14 13 2 efger 
 |-  .~ Er ( _I ` Word ( I X. 2o ) )
15 wrdexg 
 |-  ( ( I X. 2o ) e. _V -> Word ( I X. 2o ) e. _V )
16 fvi 
 |-  ( Word ( I X. 2o ) e. _V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
17 7 15 16 3syl 
 |-  ( I e. V -> ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) )
18 ereq2 
 |-  ( ( _I ` Word ( I X. 2o ) ) = Word ( I X. 2o ) -> ( .~ Er ( _I ` Word ( I X. 2o ) ) <-> .~ Er Word ( I X. 2o ) ) )
19 17 18 syl 
 |-  ( I e. V -> ( .~ Er ( _I ` Word ( I X. 2o ) ) <-> .~ Er Word ( I X. 2o ) ) )
20 14 19 mpbii 
 |-  ( I e. V -> .~ Er Word ( I X. 2o ) )
21 fvexd 
 |-  ( I e. V -> ( freeMnd ` ( I X. 2o ) ) e. _V )
22 eqid 
 |-  ( +g ` ( freeMnd ` ( I X. 2o ) ) ) = ( +g ` ( freeMnd ` ( I X. 2o ) ) )
23 1 3 2 22 frgpcpbl 
 |-  ( ( a .~ b /\ c .~ d ) -> ( a ( +g ` ( freeMnd ` ( I X. 2o ) ) ) c ) .~ ( b ( +g ` ( freeMnd ` ( I X. 2o ) ) ) d ) )
24 23 a1i 
 |-  ( I e. V -> ( ( a .~ b /\ c .~ d ) -> ( a ( +g ` ( freeMnd ` ( I X. 2o ) ) ) c ) .~ ( b ( +g ` ( freeMnd ` ( I X. 2o ) ) ) d ) ) )
25 3 frmdmnd 
 |-  ( ( I X. 2o ) e. _V -> ( freeMnd ` ( I X. 2o ) ) e. Mnd )
26 7 25 syl 
 |-  ( I e. V -> ( freeMnd ` ( I X. 2o ) ) e. Mnd )
27 26 3ad2ant1 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) ) -> ( freeMnd ` ( I X. 2o ) ) e. Mnd )
28 simp2 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) ) -> x e. Word ( I X. 2o ) )
29 11 3ad2ant1 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) ) -> Word ( I X. 2o ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
30 28 29 eleqtrd 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) ) -> x e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
31 simp3 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) ) -> y e. Word ( I X. 2o ) )
32 31 29 eleqtrd 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) ) -> y e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
33 8 22 mndcl 
 |-  ( ( ( freeMnd ` ( I X. 2o ) ) e. Mnd /\ x e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) /\ y e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) -> ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
34 27 30 32 33 syl3anc 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) ) -> ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
35 34 29 eleqtrrd 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) ) -> ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) e. Word ( I X. 2o ) )
36 20 adantr 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> .~ Er Word ( I X. 2o ) )
37 26 adantr 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> ( freeMnd ` ( I X. 2o ) ) e. Mnd )
38 34 3adant3r3 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
39 simpr3 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> z e. Word ( I X. 2o ) )
40 11 adantr 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> Word ( I X. 2o ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
41 39 40 eleqtrd 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> z e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
42 8 22 mndcl 
 |-  ( ( ( freeMnd ` ( I X. 2o ) ) e. Mnd /\ ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) /\ z e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) -> ( ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
43 37 38 41 42 syl3anc 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> ( ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
44 43 40 eleqtrrd 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> ( ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) e. Word ( I X. 2o ) )
45 36 44 erref 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> ( ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) .~ ( ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) )
46 30 3adant3r3 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> x e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
47 32 3adant3r3 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> y e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
48 8 22 mndass 
 |-  ( ( ( freeMnd ` ( I X. 2o ) ) e. Mnd /\ ( x e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) /\ y e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) /\ z e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) ) -> ( ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) = ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) ( y ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) ) )
49 37 46 47 41 48 syl13anc 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> ( ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) = ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) ( y ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) ) )
50 45 49 breqtrd 
 |-  ( ( I e. V /\ ( x e. Word ( I X. 2o ) /\ y e. Word ( I X. 2o ) /\ z e. Word ( I X. 2o ) ) ) -> ( ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) y ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) .~ ( x ( +g ` ( freeMnd ` ( I X. 2o ) ) ) ( y ( +g ` ( freeMnd ` ( I X. 2o ) ) ) z ) ) )
51 wrd0 
 |-  (/) e. Word ( I X. 2o )
52 51 a1i 
 |-  ( I e. V -> (/) e. Word ( I X. 2o ) )
53 51 11 eleqtrid 
 |-  ( I e. V -> (/) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
54 53 adantr 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> (/) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
55 11 eleq2d 
 |-  ( I e. V -> ( x e. Word ( I X. 2o ) <-> x e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) )
56 55 biimpa 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> x e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
57 3 8 22 frmdadd 
 |-  ( ( (/) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) /\ x e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) -> ( (/) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) x ) = ( (/) ++ x ) )
58 54 56 57 syl2anc 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( (/) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) x ) = ( (/) ++ x ) )
59 ccatlid 
 |-  ( x e. Word ( I X. 2o ) -> ( (/) ++ x ) = x )
60 59 adantl 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( (/) ++ x ) = x )
61 58 60 eqtrd 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( (/) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) x ) = x )
62 20 adantr 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> .~ Er Word ( I X. 2o ) )
63 simpr 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> x e. Word ( I X. 2o ) )
64 62 63 erref 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> x .~ x )
65 61 64 eqbrtrd 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( (/) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) x ) .~ x )
66 revcl 
 |-  ( x e. Word ( I X. 2o ) -> ( reverse ` x ) e. Word ( I X. 2o ) )
67 66 adantl 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( reverse ` x ) e. Word ( I X. 2o ) )
68 eqid 
 |-  ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
69 68 efgmf 
 |-  ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) : ( I X. 2o ) --> ( I X. 2o )
70 69 a1i 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) : ( I X. 2o ) --> ( I X. 2o ) )
71 wrdco 
 |-  ( ( ( reverse ` x ) e. Word ( I X. 2o ) /\ ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) : ( I X. 2o ) --> ( I X. 2o ) ) -> ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) e. Word ( I X. 2o ) )
72 67 70 71 syl2anc 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) e. Word ( I X. 2o ) )
73 11 adantr 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> Word ( I X. 2o ) = ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
74 72 73 eleqtrd 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) )
75 3 8 22 frmdadd 
 |-  ( ( ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) /\ x e. ( Base ` ( freeMnd ` ( I X. 2o ) ) ) ) -> ( ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) x ) = ( ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) ++ x ) )
76 74 56 75 syl2anc 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) x ) = ( ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) ++ x ) )
77 17 eleq2d 
 |-  ( I e. V -> ( x e. ( _I ` Word ( I X. 2o ) ) <-> x e. Word ( I X. 2o ) ) )
78 77 biimpar 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> x e. ( _I ` Word ( I X. 2o ) ) )
79 eqid 
 |-  ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) ) = ( v e. ( _I ` Word ( I X. 2o ) ) |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` w ) "> >. ) ) )
80 13 2 68 79 efginvrel1 
 |-  ( x e. ( _I ` Word ( I X. 2o ) ) -> ( ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) ++ x ) .~ (/) )
81 78 80 syl 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) ++ x ) .~ (/) )
82 76 81 eqbrtrd 
 |-  ( ( I e. V /\ x e. Word ( I X. 2o ) ) -> ( ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) o. ( reverse ` x ) ) ( +g ` ( freeMnd ` ( I X. 2o ) ) ) x ) .~ (/) )
83 4 11 12 20 21 24 35 50 52 65 72 82 qusgrp2 
 |-  ( I e. V -> ( G e. Grp /\ [ (/) ] .~ = ( 0g ` G ) ) )