Theorem ablsimpgfindlem2

Description: Lemma for ablsimpgfind . An element of an abelian finite simple group which squares to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	ablsimpgfindlem1.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablsimpgfindlem1.2	⊢ 0 = ( 0g ‘ 𝐺 )
	ablsimpgfindlem1.3	⊢ · = ( .g ‘ 𝐺 )
	ablsimpgfindlem1.4	⊢ 𝑂 = ( od ‘ 𝐺 )
	ablsimpgfindlem1.5	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	ablsimpgfindlem1.6	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
Assertion	ablsimpgfindlem2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 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		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) = 0 ) → ( 2 · 𝑥 ) = 0 )
8	6	simpggrpd	⊢ ( 𝜑 → 𝐺 ∈ Grp )
9	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐺 ∈ Grp )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
11		2z	⊢ 2 ∈ ℤ
12	11	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 2 ∈ ℤ )
13	9 10 12	3jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 2 ∈ ℤ ) )
14	13	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) = 0 ) → ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 2 ∈ ℤ ) )
15	1 4 3 2	oddvds	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 2 ∈ ℤ ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 2 ↔ ( 2 · 𝑥 ) = 0 ) )
16	14 15	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) = 0 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ 2 ↔ ( 2 · 𝑥 ) = 0 ) )
17	7 16	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) = 0 ) → ( 𝑂 ‘ 𝑥 ) ∥ 2 )
18		2ne0	⊢ 2 ≠ 0
19	18	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) = 0 ) → 2 ≠ 0 )
20	19	neneqd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) = 0 ) → ¬ 2 = 0 )
21		0dvds	⊢ ( 2 ∈ ℤ → ( 0 ∥ 2 ↔ 2 = 0 ) )
22	11 21	ax-mp	⊢ ( 0 ∥ 2 ↔ 2 = 0 )
23	20 22	sylnibr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) = 0 ) → ¬ 0 ∥ 2 )
24		nbrne2	⊢ ( ( ( 𝑂 ‘ 𝑥 ) ∥ 2 ∧ ¬ 0 ∥ 2 ) → ( 𝑂 ‘ 𝑥 ) ≠ 0 )
25	17 23 24	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 2 · 𝑥 ) = 0 ) → ( 𝑂 ‘ 𝑥 ) ≠ 0 )