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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gexex.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
Assertion gex2abl ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) → 𝐺 ∈ Abel )

Proof

Step Hyp Ref Expression
1 gexex.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gexex.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
3 1 a1i ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) → 𝑋 = ( Base ‘ 𝐺 ) )
4 eqidd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) )
5 simpl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) → 𝐺 ∈ Grp )
6 simp1l ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝐺 ∈ Grp )
7 simp2 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
8 simp3 ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ 𝑋 )
9 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
10 1 9 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑦 ) ) )
11 6 7 8 8 10 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑦 ) ) )
12 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
13 1 12 9 mulg2 ⊢ ( 𝑦 ∈ 𝑋 → ( 2 ( .g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑦 ) )
14 8 13 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 2 ( .g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑦 ) )
15 simp1r ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 𝐸 ∥ 2 )
16 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
17 1 2 12 16 gexdvdsi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝐸 ∥ 2 ) → ( 2 ( .g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) )
18 6 8 15 17 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 2 ( .g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) )
19 14 18 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑦 ) = ( 0g ‘ 𝐺 ) )
20 19 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) )
21 1 9 16 grprid ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
22 6 7 21 syl2anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( 0g ‘ 𝐺 ) ) = 𝑥 )
23 11 20 22 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) = 𝑥 )
24 23 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑥 ) )
25 1 12 9 mulg2 ⊢ ( 𝑥 ∈ 𝑋 → ( 2 ( .g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑥 ) )
26 7 25 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 2 ( .g ‘ 𝐺 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑥 ) )
27 1 2 12 16 gexdvdsi ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐸 ∥ 2 ) → ( 2 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
28 6 7 15 27 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 2 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
29 24 26 28 3eqtr2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
30 1 9 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
31 6 7 8 30 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 )
32 1 2 12 16 gexdvdsi ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 ∧ 𝐸 ∥ 2 ) → ( 2 ( .g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 0g ‘ 𝐺 ) )
33 6 31 15 32 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 2 ( .g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 0g ‘ 𝐺 ) )
34 1 12 9 mulg2 ⊢ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 → ( 2 ( .g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
35 31 34 syl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 2 ( .g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
36 29 33 35 3eqtr2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
37 1 9 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
38 6 31 8 7 37 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑥 ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
39 36 38 eqtr3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
40 1 9 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑋 )
41 6 8 7 40 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑋 )
42 1 9 grplcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝑋 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑋 ) ) → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
43 6 31 41 31 42 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
44 39 43 mpbid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
45 3 4 5 44 isabld ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐸 ∥ 2 ) → 𝐺 ∈ Abel )