gexdvdsi

Description: Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gexcl.1	$⊢ X = {Base}_{G}$
	gexcl.2	$⊢ E = gEx (G)$
	gexid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	gexid.4	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	gexdvdsi	$⊢ (G \in Grp \land A \in X \land E ∥ N) \to N \underset{˙}{\cdot} A = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		gexcl.1	$⊢ X = {Base}_{G}$
2		gexcl.2	$⊢ E = gEx (G)$
3		gexid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		gexid.4	$⊢ \underset{˙}{0} = 0_{G}$
5		simp3	$⊢ (G \in Grp \land A \in X \land E ∥ N) \to E ∥ N$
6		dvdszrcl	$⊢ E ∥ N \to (E \in ℤ \land N \in ℤ)$
7		divides	$⊢ (E \in ℤ \land N \in ℤ) \to (E ∥ N \leftrightarrow \exists x \in ℤ x E = N)$
8	6 7	biadanii	$⊢ E ∥ N \leftrightarrow ((E \in ℤ \land N \in ℤ) \land \exists x \in ℤ x E = N)$
9	5 8	sylib	$⊢ (G \in Grp \land A \in X \land E ∥ N) \to ((E \in ℤ \land N \in ℤ) \land \exists x \in ℤ x E = N)$
10	9	simprd	$⊢ (G \in Grp \land A \in X \land E ∥ N) \to \exists x \in ℤ x E = N$
11		simpl1	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to G \in Grp$
12		simpr	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to x \in ℤ$
13	9	simplld	$⊢ (G \in Grp \land A \in X \land E ∥ N) \to E \in ℤ$
14	13	adantr	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to E \in ℤ$
15		simpl2	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to A \in X$
16	1 3	mulgass	$⊢ (G \in Grp \land (x \in ℤ \land E \in ℤ \land A \in X)) \to x E \underset{˙}{\cdot} A = x \underset{˙}{\cdot} (E \underset{˙}{\cdot} A)$
17	11 12 14 15 16	syl13anc	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to x E \underset{˙}{\cdot} A = x \underset{˙}{\cdot} (E \underset{˙}{\cdot} A)$
18	1 2 3 4	gexid	$⊢ A \in X \to E \underset{˙}{\cdot} A = \underset{˙}{0}$
19	15 18	syl	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to E \underset{˙}{\cdot} A = \underset{˙}{0}$
20	19	oveq2d	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to x \underset{˙}{\cdot} (E \underset{˙}{\cdot} A) = x \underset{˙}{\cdot} \underset{˙}{0}$
21	1 3 4	mulgz	$⊢ (G \in Grp \land x \in ℤ) \to x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
22	21	3ad2antl1	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to x \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
23	17 20 22	3eqtrd	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to x E \underset{˙}{\cdot} A = \underset{˙}{0}$
24		oveq1	$⊢ x E = N \to x E \underset{˙}{\cdot} A = N \underset{˙}{\cdot} A$
25	24	eqeq1d	$⊢ x E = N \to (x E \underset{˙}{\cdot} A = \underset{˙}{0} \leftrightarrow N \underset{˙}{\cdot} A = \underset{˙}{0})$
26	23 25	syl5ibcom	$⊢ ((G \in Grp \land A \in X \land E ∥ N) \land x \in ℤ) \to (x E = N \to N \underset{˙}{\cdot} A = \underset{˙}{0})$
27	26	rexlimdva	$⊢ (G \in Grp \land A \in X \land E ∥ N) \to (\exists x \in ℤ x E = N \to N \underset{˙}{\cdot} A = \underset{˙}{0})$
28	10 27	mpd	$⊢ (G \in Grp \land A \in X \land E ∥ N) \to N \underset{˙}{\cdot} A = \underset{˙}{0}$

Metamath Proof Explorer

Theorem gexdvdsi

Proof