This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )