Metamath Proof Explorer


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 )