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	$⊢ 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	ablsimpgfindlem1	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x \neq \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	5	3ad2ant1	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to G \in Abel$
8	6	3ad2ant1	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to G \in SimpGrp$
9	6	simpggrpd	$⊢ φ \to G \in Grp$
10	9	3ad2ant1	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to G \in Grp$
11		2z	$⊢ 2 \in ℤ$
12	11	a1i	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to 2 \in ℤ$
13		simp2	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to x \in B$
14	1 3 10 12 13	mulgcld	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to 2 \underset{˙}{\cdot} x \in B$
15		simp3	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}$
16	15	neneqd	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to \neg 2 \underset{˙}{\cdot} x = \underset{˙}{0}$
17	1 2 3 7 8 14 16 13	ablsimpg1gend	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to \exists y \in ℤ x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x)$
18		simprr	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x)$
19		simpl2	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to x \in B$
20	1 3	mulg1	$⊢ x \in B \to 1 \underset{˙}{\cdot} x = x$
21	19 20	syl	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to 1 \underset{˙}{\cdot} x = x$
22	10	adantr	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to G \in Grp$
23		simprl	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to y \in ℤ$
24	11	a1i	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to 2 \in ℤ$
25	1 3	mulgassr	$⊢ (G \in Grp \land (y \in ℤ \land 2 \in ℤ \land x \in B)) \to 2 y \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x)$
26	22 23 24 19 25	syl13anc	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to 2 y \underset{˙}{\cdot} x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x)$
27	18 21 26	3eqtr4rd	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to 2 y \underset{˙}{\cdot} x = 1 \underset{˙}{\cdot} x$
28	24 23	zmulcld	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to 2 y \in ℤ$
29		1zzd	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to 1 \in ℤ$
30	1 4 3 2	odcong	$⊢ (G \in Grp \land x \in B \land (2 y \in ℤ \land 1 \in ℤ)) \to (O (x) ∥ (2 y - 1) \leftrightarrow 2 y \underset{˙}{\cdot} x = 1 \underset{˙}{\cdot} x)$
31	22 19 28 29 30	syl112anc	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to (O (x) ∥ (2 y - 1) \leftrightarrow 2 y \underset{˙}{\cdot} x = 1 \underset{˙}{\cdot} x)$
32	27 31	mpbird	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to O (x) ∥ (2 y - 1)$
33		0zd	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to 0 \in ℤ$
34		zneo	$⊢ (y \in ℤ \land 0 \in ℤ) \to 2 y \neq 2 \cdot 0 + 1$
35		2t0e0	$⊢ 2 \cdot 0 = 0$
36	35	oveq1i	$⊢ 2 \cdot 0 + 1 = 0 + 1$
37		0p1e1	$⊢ 0 + 1 = 1$
38	36 37	eqtri	$⊢ 2 \cdot 0 + 1 = 1$
39	38	a1i	$⊢ (y \in ℤ \land 0 \in ℤ) \to 2 \cdot 0 + 1 = 1$
40	34 39	neeqtrd	$⊢ (y \in ℤ \land 0 \in ℤ) \to 2 y \neq 1$
41		oveq1	$⊢ 2 y - 1 = 0 \to 2 y - 1 + 1 = 0 + 1$
42	41 37	syl6req	$⊢ 2 y - 1 = 0 \to 1 = 2 y - 1 + 1$
43	42	adantl	$⊢ (y \in ℤ \land 2 y - 1 = 0) \to 1 = 2 y - 1 + 1$
44		2cnd	$⊢ y \in ℤ \to 2 \in ℂ$
45		zcn	$⊢ y \in ℤ \to y \in ℂ$
46	44 45	mulcld	$⊢ y \in ℤ \to 2 y \in ℂ$
47		1cnd	$⊢ 2 y - 1 = 0 \to 1 \in ℂ$
48		npcan	$⊢ (2 y \in ℂ \land 1 \in ℂ) \to 2 y - 1 + 1 = 2 y$
49	46 47 48	syl2an	$⊢ (y \in ℤ \land 2 y - 1 = 0) \to 2 y - 1 + 1 = 2 y$
50	43 49	eqtr2d	$⊢ (y \in ℤ \land 2 y - 1 = 0) \to 2 y = 1$
51	50	ex	$⊢ y \in ℤ \to (2 y - 1 = 0 \to 2 y = 1)$
52	51	necon3ad	$⊢ y \in ℤ \to (2 y \neq 1 \to \neg 2 y - 1 = 0)$
53	40 52	syl5	$⊢ y \in ℤ \to ((y \in ℤ \land 0 \in ℤ) \to \neg 2 y - 1 = 0)$
54	53	anabsi5	$⊢ (y \in ℤ \land 0 \in ℤ) \to \neg 2 y - 1 = 0$
55	23 33 54	syl2anc	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to \neg 2 y - 1 = 0$
56	28 29	zsubcld	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to 2 y - 1 \in ℤ$
57		0dvds	$⊢ 2 y - 1 \in ℤ \to (0 ∥ (2 y - 1) \leftrightarrow 2 y - 1 = 0)$
58	56 57	syl	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to (0 ∥ (2 y - 1) \leftrightarrow 2 y - 1 = 0)$
59	55 58	mtbird	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to \neg 0 ∥ (2 y - 1)$
60		nbrne2	$⊢ (O (x) ∥ (2 y - 1) \land \neg 0 ∥ (2 y - 1)) \to O (x) \neq 0$
61	32 59 60	syl2anc	$⊢ ((φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \land (y \in ℤ \land x = y \underset{˙}{\cdot} (2 \underset{˙}{\cdot} x))) \to O (x) \neq 0$
62	17 61	rexlimddv	$⊢ (φ \land x \in B \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to O (x) \neq 0$
63	62	3expa	$⊢ ((φ \land x \in B) \land 2 \underset{˙}{\cdot} x \neq \underset{˙}{0}) \to O (x) \neq 0$

Metamath Proof Explorer

Theorem ablsimpgfindlem1

Proof