This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frgpnabl

Description: The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypothesis frgpnabl.g 
|- G = ( freeGrp ` I )
Assertion frgpnabl 
|- ( 1o ~< I -> -. G e. Abel )

Proof

Step Hyp Ref Expression
1 frgpnabl.g 
 |-  G = ( freeGrp ` I )
2 relsdom 
 |-  Rel ~<
3 2 brrelex2i 
 |-  ( 1o ~< I -> I e. _V )
4 1sdom 
 |-  ( I e. _V -> ( 1o ~< I <-> E. a e. I E. b e. I -. a = b ) )
5 3 4 syl 
 |-  ( 1o ~< I -> ( 1o ~< I <-> E. a e. I E. b e. I -. a = b ) )
6 5 ibi 
 |-  ( 1o ~< I -> E. a e. I E. b e. I -. a = b )
7 eqid 
 |-  ( _I ` Word ( I X. 2o ) ) = ( _I ` Word ( I X. 2o ) )
8 eqid 
 |-  ( ~FG ` I ) = ( ~FG ` I )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 eqid 
 |-  ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
11 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 ) "> >. ) ) )
12 eqid 
 |-  ( ( _I ` Word ( I X. 2o ) ) \ U_ x e. ( _I ` Word ( I X. 2o ) ) ran ( ( 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 ) "> >. ) ) ) ` x ) ) = ( ( _I ` Word ( I X. 2o ) ) \ U_ x e. ( _I ` Word ( I X. 2o ) ) ran ( ( 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 ) "> >. ) ) ) ` x ) )
13 eqid 
 |-  ( varFGrp ` I ) = ( varFGrp ` I )
14 3 ad2antrr 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> I e. _V )
15 simplrl 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> a e. I )
16 simplrr 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> b e. I )
17 simpr 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> G e. Abel )
18 eqid 
 |-  ( Base ` G ) = ( Base ` G )
19 8 13 1 18 vrgpf 
 |-  ( I e. _V -> ( varFGrp ` I ) : I --> ( Base ` G ) )
20 14 19 syl 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> ( varFGrp ` I ) : I --> ( Base ` G ) )
21 20 15 ffvelcdmd 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> ( ( varFGrp ` I ) ` a ) e. ( Base ` G ) )
22 20 16 ffvelcdmd 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> ( ( varFGrp ` I ) ` b ) e. ( Base ` G ) )
23 18 9 ablcom 
 |-  ( ( G e. Abel /\ ( ( varFGrp ` I ) ` a ) e. ( Base ` G ) /\ ( ( varFGrp ` I ) ` b ) e. ( Base ` G ) ) -> ( ( ( varFGrp ` I ) ` a ) ( +g ` G ) ( ( varFGrp ` I ) ` b ) ) = ( ( ( varFGrp ` I ) ` b ) ( +g ` G ) ( ( varFGrp ` I ) ` a ) ) )
24 17 21 22 23 syl3anc 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> ( ( ( varFGrp ` I ) ` a ) ( +g ` G ) ( ( varFGrp ` I ) ` b ) ) = ( ( ( varFGrp ` I ) ` b ) ( +g ` G ) ( ( varFGrp ` I ) ` a ) ) )
25 1 7 8 9 10 11 12 13 14 15 16 24 frgpnabllem2 
 |-  ( ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) /\ G e. Abel ) -> a = b )
26 25 ex 
 |-  ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) -> ( G e. Abel -> a = b ) )
27 26 con3d 
 |-  ( ( 1o ~< I /\ ( a e. I /\ b e. I ) ) -> ( -. a = b -> -. G e. Abel ) )
28 27 rexlimdvva 
 |-  ( 1o ~< I -> ( E. a e. I E. b e. I -. a = b -> -. G e. Abel ) )
29 6 28 mpd 
 |-  ( 1o ~< I -> -. G e. Abel )