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 \in Grp \land E ∥ 2) \to G \in Abel$

Proof

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

Metamath Proof Explorer

Theorem gex2abl

Proof