Theorem 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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	gexcl.2	⊢ 𝐸 = ( gEx ‘ 𝐺 )
	gexid.3	⊢ · = ( .g ‘ 𝐺 )
	gexid.4	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	gexdvdsi	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) → ( 𝑁 · 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		gexcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		gexcl.2	⊢ 𝐸 = ( gEx ‘ 𝐺 )
3		gexid.3	⊢ · = ( .g ‘ 𝐺 )
4		gexid.4	⊢ 0 = ( 0g ‘ 𝐺 )
5		simp3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) → 𝐸 ∥ 𝑁 )
6		dvdszrcl	⊢ ( 𝐸 ∥ 𝑁 → ( 𝐸 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
7		divides	⊢ ( ( 𝐸 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐸 ∥ 𝑁 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐸 ) = 𝑁 ) )
8	6 7	biadanii	⊢ ( 𝐸 ∥ 𝑁 ↔ ( ( 𝐸 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐸 ) = 𝑁 ) )
9	5 8	sylib	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) → ( ( 𝐸 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐸 ) = 𝑁 ) )
10	9	simprd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) → ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐸 ) = 𝑁 )
11		simpl1	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → 𝐺 ∈ Grp )
12		simpr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
13	9	simplld	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) → 𝐸 ∈ ℤ )
14	13	adantr	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → 𝐸 ∈ ℤ )
15		simpl2	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → 𝐴 ∈ 𝑋 )
16	1 3	mulgass	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝐸 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑥 · 𝐸 ) · 𝐴 ) = ( 𝑥 · ( 𝐸 · 𝐴 ) ) )
17	11 12 14 15 16	syl13anc	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝐸 ) · 𝐴 ) = ( 𝑥 · ( 𝐸 · 𝐴 ) ) )
18	1 2 3 4	gexid	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐸 · 𝐴 ) = 0 )
19	15 18	syl	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → ( 𝐸 · 𝐴 ) = 0 )
20	19	oveq2d	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · ( 𝐸 · 𝐴 ) ) = ( 𝑥 · 0 ) )
21	1 3 4	mulgz	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 0 ) = 0 )
22	21	3ad2antl1	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 0 ) = 0 )
23	17 20 22	3eqtrd	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝐸 ) · 𝐴 ) = 0 )
24		oveq1	⊢ ( ( 𝑥 · 𝐸 ) = 𝑁 → ( ( 𝑥 · 𝐸 ) · 𝐴 ) = ( 𝑁 · 𝐴 ) )
25	24	eqeq1d	⊢ ( ( 𝑥 · 𝐸 ) = 𝑁 → ( ( ( 𝑥 · 𝐸 ) · 𝐴 ) = 0 ↔ ( 𝑁 · 𝐴 ) = 0 ) )
26	23 25	syl5ibcom	⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝐸 ) = 𝑁 → ( 𝑁 · 𝐴 ) = 0 ) )
27	26	rexlimdva	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝐸 ) = 𝑁 → ( 𝑁 · 𝐴 ) = 0 ) )
28	10 27	mpd	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁 ) → ( 𝑁 · 𝐴 ) = 0 )