Metamath Proof Explorer

Theorem ablsimpgfindlem1

Description: Lemma for ablsimpgfind . An element of an abelian finite simple group which doesn't square to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023) (Proof shortened by Rohan Ridenour, 31-Oct-2023)

Ref Expression
Hypotheses ablsimpgfindlem1.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablsimpgfindlem1.2 ⊢ 0 = ( 0g ‘ 𝐺 )
ablsimpgfindlem1.3 ⊢ · = ( .g ‘ 𝐺 )
ablsimpgfindlem1.4 ⊢ 𝑂 = ( od ‘ 𝐺 )
ablsimpgfindlem1.5 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablsimpgfindlem1.6 ⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
Assertion ablsimpgfindlem1 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) ≠ 0 ) → ( 𝑂 ‘ 𝑥 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 ablsimpgfindlem1.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablsimpgfindlem1.2 ⊢ 0 = ( 0g ‘ 𝐺 )
3 ablsimpgfindlem1.3 ⊢ · = ( .g ‘ 𝐺 )
4 ablsimpgfindlem1.4 ⊢ 𝑂 = ( od ‘ 𝐺 )
5 ablsimpgfindlem1.5 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
6 ablsimpgfindlem1.6 ⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
7 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → 𝐺 ∈ Abel )
8 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → 𝐺 ∈ SimpGrp )
9 6 simpggrpd ⊢ ( 𝜑 → 𝐺 ∈ Grp )
10 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → 𝐺 ∈ Grp )
11 2z ⊢ 2 ∈ ℤ
12 11 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → 2 ∈ ℤ )
13 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → 𝑥 ∈ 𝐵 )
14 1 3 10 12 13 mulgcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → ( 2 · 𝑥 ) ∈ 𝐵 )
15 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → ( 2 · 𝑥 ) ≠ 0 )
16 15 neneqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → ¬ ( 2 · 𝑥 ) = 0 )
17 1 2 3 7 8 14 16 13 ablsimpg1gend ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → ∃ 𝑦 ∈ ℤ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) )
18 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) )
19 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → 𝑥 ∈ 𝐵 )
20 1 3 mulg1 ⊢ ( 𝑥 ∈ 𝐵 → ( 1 · 𝑥 ) = 𝑥 )
21 19 20 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( 1 · 𝑥 ) = 𝑥 )
22 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → 𝐺 ∈ Grp )
23 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → 𝑦 ∈ ℤ )
24 11 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → 2 ∈ ℤ )
25 1 3 mulgassr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ ℤ ∧ 2 ∈ ℤ ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 2 · 𝑦 ) · 𝑥 ) = ( 𝑦 · ( 2 · 𝑥 ) ) )
26 22 23 24 19 25 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( ( 2 · 𝑦 ) · 𝑥 ) = ( 𝑦 · ( 2 · 𝑥 ) ) )
27 18 21 26 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( ( 2 · 𝑦 ) · 𝑥 ) = ( 1 · 𝑥 ) )
28 24 23 zmulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( 2 · 𝑦 ) ∈ ℤ )
29 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → 1 ∈ ℤ )
30 1 4 3 2 odcong ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ ( ( 2 · 𝑦 ) ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( ( 𝑂 ‘ 𝑥 ) ∥ ( ( 2 · 𝑦 ) − 1 ) ↔ ( ( 2 · 𝑦 ) · 𝑥 ) = ( 1 · 𝑥 ) ) )
31 22 19 28 29 30 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( ( 𝑂 ‘ 𝑥 ) ∥ ( ( 2 · 𝑦 ) − 1 ) ↔ ( ( 2 · 𝑦 ) · 𝑥 ) = ( 1 · 𝑥 ) ) )
32 27 31 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ( 2 · 𝑦 ) − 1 ) )
33 0zd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → 0 ∈ ℤ )
34 zneo ⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 2 · 𝑦 ) ≠ ( ( 2 · 0 ) + 1 ) )
35 2t0e0 ⊢ ( 2 · 0 ) = 0
36 35 oveq1i ⊢ ( ( 2 · 0 ) + 1 ) = ( 0 + 1 )
37 0p1e1 ⊢ ( 0 + 1 ) = 1
38 36 37 eqtri ⊢ ( ( 2 · 0 ) + 1 ) = 1
39 38 a1i ⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ∈ ℤ ) → ( ( 2 · 0 ) + 1 ) = 1 )
40 34 39 neeqtrd ⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 2 · 𝑦 ) ≠ 1 )
41 oveq1 ⊢ ( ( ( 2 · 𝑦 ) − 1 ) = 0 → ( ( ( 2 · 𝑦 ) − 1 ) + 1 ) = ( 0 + 1 ) )
42 41 37 eqtr2di ⊢ ( ( ( 2 · 𝑦 ) − 1 ) = 0 → 1 = ( ( ( 2 · 𝑦 ) − 1 ) + 1 ) )
43 42 adantl ⊢ ( ( 𝑦 ∈ ℤ ∧ ( ( 2 · 𝑦 ) − 1 ) = 0 ) → 1 = ( ( ( 2 · 𝑦 ) − 1 ) + 1 ) )
44 2cnd ⊢ ( 𝑦 ∈ ℤ → 2 ∈ ℂ )
45 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
46 44 45 mulcld ⊢ ( 𝑦 ∈ ℤ → ( 2 · 𝑦 ) ∈ ℂ )
47 1cnd ⊢ ( ( ( 2 · 𝑦 ) − 1 ) = 0 → 1 ∈ ℂ )
48 npcan ⊢ ( ( ( 2 · 𝑦 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑦 ) − 1 ) + 1 ) = ( 2 · 𝑦 ) )
49 46 47 48 syl2an ⊢ ( ( 𝑦 ∈ ℤ ∧ ( ( 2 · 𝑦 ) − 1 ) = 0 ) → ( ( ( 2 · 𝑦 ) − 1 ) + 1 ) = ( 2 · 𝑦 ) )
50 43 49 eqtr2d ⊢ ( ( 𝑦 ∈ ℤ ∧ ( ( 2 · 𝑦 ) − 1 ) = 0 ) → ( 2 · 𝑦 ) = 1 )
51 50 ex ⊢ ( 𝑦 ∈ ℤ → ( ( ( 2 · 𝑦 ) − 1 ) = 0 → ( 2 · 𝑦 ) = 1 ) )
52 51 necon3ad ⊢ ( 𝑦 ∈ ℤ → ( ( 2 · 𝑦 ) ≠ 1 → ¬ ( ( 2 · 𝑦 ) − 1 ) = 0 ) )
53 40 52 syl5 ⊢ ( 𝑦 ∈ ℤ → ( ( 𝑦 ∈ ℤ ∧ 0 ∈ ℤ ) → ¬ ( ( 2 · 𝑦 ) − 1 ) = 0 ) )
54 53 anabsi5 ⊢ ( ( 𝑦 ∈ ℤ ∧ 0 ∈ ℤ ) → ¬ ( ( 2 · 𝑦 ) − 1 ) = 0 )
55 23 33 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ¬ ( ( 2 · 𝑦 ) − 1 ) = 0 )
56 28 29 zsubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( ( 2 · 𝑦 ) − 1 ) ∈ ℤ )
57 0dvds ⊢ ( ( ( 2 · 𝑦 ) − 1 ) ∈ ℤ → ( 0 ∥ ( ( 2 · 𝑦 ) − 1 ) ↔ ( ( 2 · 𝑦 ) − 1 ) = 0 ) )
58 56 57 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( 0 ∥ ( ( 2 · 𝑦 ) − 1 ) ↔ ( ( 2 · 𝑦 ) − 1 ) = 0 ) )
59 55 58 mtbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ¬ 0 ∥ ( ( 2 · 𝑦 ) − 1 ) )
60 nbrne2 ⊢ ( ( ( 𝑂 ‘ 𝑥 ) ∥ ( ( 2 · 𝑦 ) − 1 ) ∧ ¬ 0 ∥ ( ( 2 · 𝑦 ) − 1 ) ) → ( 𝑂 ‘ 𝑥 ) ≠ 0 )
61 32 59 60 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑥 = ( 𝑦 · ( 2 · 𝑥 ) ) ) ) → ( 𝑂 ‘ 𝑥 ) ≠ 0 )
62 17 61 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ( 2 · 𝑥 ) ≠ 0 ) → ( 𝑂 ‘ 𝑥 ) ≠ 0 )
63 62 3expa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) ≠ 0 ) → ( 𝑂 ‘ 𝑥 ) ≠ 0 )