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	$⊢ B = {Base}_{G}$
	ablsimpgfindlem1.2	$⊢ \underset{˙}{0} = 0_{G}$
	ablsimpgfindlem1.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	ablsimpgfindlem1.4	$⊢ O = od (G)$
	ablsimpgfindlem1.5	$⊢ φ \to G \in Abel$
	ablsimpgfindlem1.6	$⊢ φ \to G \in SimpGrp$
Assertion	ablsimpgfindlem2	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to O (x) \neq 0$

Proof

Step	Hyp	Ref	Expression
1		ablsimpgfindlem1.1	$⊢ B = {Base}_{G}$
2		ablsimpgfindlem1.2	$⊢ \underset{˙}{0} = 0_{G}$
3		ablsimpgfindlem1.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		ablsimpgfindlem1.4	$⊢ O = od (G)$
5		ablsimpgfindlem1.5	$⊢ φ \to G \in Abel$
6		ablsimpgfindlem1.6	$⊢ φ \to G \in SimpGrp$
7		simpr	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to 2 \underset{˙}{\cdot} x = \underset{˙}{0}$
8	6	simpggrpd	$⊢ φ \to G \in Grp$
9	8	adantr	$⊢ (φ \land x \in B) \to G \in Grp$
10		simpr	$⊢ (φ \land x \in B) \to x \in B$
11		2z	$⊢ 2 \in ℤ$
12	11	a1i	$⊢ (φ \land x \in B) \to 2 \in ℤ$
13	9 10 12	3jca	$⊢ (φ \land x \in B) \to (G \in Grp \land x \in B \land 2 \in ℤ)$
14	13	adantr	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to (G \in Grp \land x \in B \land 2 \in ℤ)$
15	1 4 3 2	oddvds	$⊢ (G \in Grp \land x \in B \land 2 \in ℤ) \to (O (x) ∥ 2 \leftrightarrow 2 \underset{˙}{\cdot} x = \underset{˙}{0})$
16	14 15	syl	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to (O (x) ∥ 2 \leftrightarrow 2 \underset{˙}{\cdot} x = \underset{˙}{0})$
17	7 16	mpbird	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to O (x) ∥ 2$
18		2ne0	$⊢ 2 \neq 0$
19	18	a1i	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to 2 \neq 0$
20	19	neneqd	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to \neg 2 = 0$
21		0dvds	$⊢ 2 \in ℤ \to (0 ∥ 2 \leftrightarrow 2 = 0)$
22	11 21	ax-mp	$⊢ 0 ∥ 2 \leftrightarrow 2 = 0$
23	20 22	sylnibr	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to \neg 0 ∥ 2$
24		nbrne2	$⊢ (O (x) ∥ 2 \land \neg 0 ∥ 2) \to O (x) \neq 0$
25	17 23 24	syl2anc	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x = \underset{˙}{0}) \to O (x) \neq 0$

Metamath Proof Explorer

Theorem ablsimpgfindlem2

Proof