Metamath Proof Explorer

Theorem gex2abl

Description: A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexex.1 
|- X = ( Base ` G )
gexex.2 
|- E = ( gEx ` G )
Assertion gex2abl 
|- ( ( G e. Grp /\ E || 2 ) -> G e. Abel )

Proof

Step Hyp Ref Expression
1 gexex.1 
 |-  X = ( Base ` G )
2 gexex.2 
 |-  E = ( gEx ` G )
3 1 a1i 
 |-  ( ( G e. Grp /\ E || 2 ) -> X = ( Base ` G ) )
4 eqidd 
 |-  ( ( G e. Grp /\ E || 2 ) -> ( +g ` G ) = ( +g ` G ) )
5 simpl 
 |-  ( ( G e. Grp /\ E || 2 ) -> G e. Grp )
6 simp1l 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> G e. Grp )
7 simp2 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> x e. X )
8 simp3 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> y e. X )
9 eqid 
 |-  ( +g ` G ) = ( +g ` G )
10 1 9 grpass 
 |-  ( ( G e. Grp /\ ( x e. X /\ y e. X /\ y e. X ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) y ) = ( x ( +g ` G ) ( y ( +g ` G ) y ) ) )
11 6 7 8 8 10 syl13anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) y ) = ( x ( +g ` G ) ( y ( +g ` G ) y ) ) )
12 eqid 
 |-  ( .g ` G ) = ( .g ` G )
13 1 12 9 mulg2 
 |-  ( y e. X -> ( 2 ( .g ` G ) y ) = ( y ( +g ` G ) y ) )
14 8 13 syl 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( 2 ( .g ` G ) y ) = ( y ( +g ` G ) y ) )
15 simp1r 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> E || 2 )
16 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
17 1 2 12 16 gexdvdsi 
 |-  ( ( G e. Grp /\ y e. X /\ E || 2 ) -> ( 2 ( .g ` G ) y ) = ( 0g ` G ) )
18 6 8 15 17 syl3anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( 2 ( .g ` G ) y ) = ( 0g ` G ) )
19 14 18 eqtr3d 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( y ( +g ` G ) y ) = ( 0g ` G ) )
20 19 oveq2d 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( x ( +g ` G ) ( y ( +g ` G ) y ) ) = ( x ( +g ` G ) ( 0g ` G ) ) )
21 1 9 16 grprid 
 |-  ( ( G e. Grp /\ x e. X ) -> ( x ( +g ` G ) ( 0g ` G ) ) = x )
22 6 7 21 syl2anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( x ( +g ` G ) ( 0g ` G ) ) = x )
23 11 20 22 3eqtrd 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) y ) = x )
24 23 oveq1d 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( ( ( x ( +g ` G ) y ) ( +g ` G ) y ) ( +g ` G ) x ) = ( x ( +g ` G ) x ) )
25 1 12 9 mulg2 
 |-  ( x e. X -> ( 2 ( .g ` G ) x ) = ( x ( +g ` G ) x ) )
26 7 25 syl 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( 2 ( .g ` G ) x ) = ( x ( +g ` G ) x ) )
27 1 2 12 16 gexdvdsi 
 |-  ( ( G e. Grp /\ x e. X /\ E || 2 ) -> ( 2 ( .g ` G ) x ) = ( 0g ` G ) )
28 6 7 15 27 syl3anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( 2 ( .g ` G ) x ) = ( 0g ` G ) )
29 24 26 28 3eqtr2d 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( ( ( x ( +g ` G ) y ) ( +g ` G ) y ) ( +g ` G ) x ) = ( 0g ` G ) )
30 1 9 grpcl 
 |-  ( ( G e. Grp /\ x e. X /\ y e. X ) -> ( x ( +g ` G ) y ) e. X )
31 6 7 8 30 syl3anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( x ( +g ` G ) y ) e. X )
32 1 2 12 16 gexdvdsi 
 |-  ( ( G e. Grp /\ ( x ( +g ` G ) y ) e. X /\ E || 2 ) -> ( 2 ( .g ` G ) ( x ( +g ` G ) y ) ) = ( 0g ` G ) )
33 6 31 15 32 syl3anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( 2 ( .g ` G ) ( x ( +g ` G ) y ) ) = ( 0g ` G ) )
34 1 12 9 mulg2 
 |-  ( ( x ( +g ` G ) y ) e. X -> ( 2 ( .g ` G ) ( x ( +g ` G ) y ) ) = ( ( x ( +g ` G ) y ) ( +g ` G ) ( x ( +g ` G ) y ) ) )
35 31 34 syl 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( 2 ( .g ` G ) ( x ( +g ` G ) y ) ) = ( ( x ( +g ` G ) y ) ( +g ` G ) ( x ( +g ` G ) y ) ) )
36 29 33 35 3eqtr2d 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( ( ( x ( +g ` G ) y ) ( +g ` G ) y ) ( +g ` G ) x ) = ( ( x ( +g ` G ) y ) ( +g ` G ) ( x ( +g ` G ) y ) ) )
37 1 9 grpass 
 |-  ( ( G e. Grp /\ ( ( x ( +g ` G ) y ) e. X /\ y e. X /\ x e. X ) ) -> ( ( ( x ( +g ` G ) y ) ( +g ` G ) y ) ( +g ` G ) x ) = ( ( x ( +g ` G ) y ) ( +g ` G ) ( y ( +g ` G ) x ) ) )
38 6 31 8 7 37 syl13anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( ( ( x ( +g ` G ) y ) ( +g ` G ) y ) ( +g ` G ) x ) = ( ( x ( +g ` G ) y ) ( +g ` G ) ( y ( +g ` G ) x ) ) )
39 36 38 eqtr3d 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) ( x ( +g ` G ) y ) ) = ( ( x ( +g ` G ) y ) ( +g ` G ) ( y ( +g ` G ) x ) ) )
40 1 9 grpcl 
 |-  ( ( G e. Grp /\ y e. X /\ x e. X ) -> ( y ( +g ` G ) x ) e. X )
41 6 8 7 40 syl3anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( y ( +g ` G ) x ) e. X )
42 1 9 grplcan 
 |-  ( ( G e. Grp /\ ( ( x ( +g ` G ) y ) e. X /\ ( y ( +g ` G ) x ) e. X /\ ( x ( +g ` G ) y ) e. X ) ) -> ( ( ( x ( +g ` G ) y ) ( +g ` G ) ( x ( +g ` G ) y ) ) = ( ( x ( +g ` G ) y ) ( +g ` G ) ( y ( +g ` G ) x ) ) <-> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
43 6 31 41 31 42 syl13anc 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( ( ( x ( +g ` G ) y ) ( +g ` G ) ( x ( +g ` G ) y ) ) = ( ( x ( +g ` G ) y ) ( +g ` G ) ( y ( +g ` G ) x ) ) <-> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) ) )
44 39 43 mpbid 
 |-  ( ( ( G e. Grp /\ E || 2 ) /\ x e. X /\ y e. X ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
45 3 4 5 44 isabld 
 |-  ( ( G e. Grp /\ E || 2 ) -> G e. Abel )