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 
|- B = ( Base ` G )
ablsimpgfindlem1.2 
|- .0. = ( 0g ` G )
ablsimpgfindlem1.3 
|- .x. = ( .g ` G )
ablsimpgfindlem1.4 
|- O = ( od ` G )
ablsimpgfindlem1.5 
|- ( ph -> G e. Abel )
ablsimpgfindlem1.6 
|- ( ph -> G e. SimpGrp )
Assertion ablsimpgfindlem1 
|- ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) =/= .0. ) -> ( O ` x ) =/= 0 )

Proof

Step Hyp Ref Expression
1 ablsimpgfindlem1.1 
 |-  B = ( Base ` G )
2 ablsimpgfindlem1.2 
 |-  .0. = ( 0g ` G )
3 ablsimpgfindlem1.3 
 |-  .x. = ( .g ` G )
4 ablsimpgfindlem1.4 
 |-  O = ( od ` G )
5 ablsimpgfindlem1.5 
 |-  ( ph -> G e. Abel )
6 ablsimpgfindlem1.6 
 |-  ( ph -> G e. SimpGrp )
7 5 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> G e. Abel )
8 6 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> G e. SimpGrp )
9 6 simpggrpd 
 |-  ( ph -> G e. Grp )
10 9 3ad2ant1 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> G e. Grp )
11 2z 
 |-  2 e. ZZ
12 11 a1i 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> 2 e. ZZ )
13 simp2 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> x e. B )
14 1 3 10 12 13 mulgcld 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> ( 2 .x. x ) e. B )
15 simp3 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> ( 2 .x. x ) =/= .0. )
16 15 neneqd 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> -. ( 2 .x. x ) = .0. )
17 1 2 3 7 8 14 16 13 ablsimpg1gend 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> E. y e. ZZ x = ( y .x. ( 2 .x. x ) ) )
18 simprr 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> x = ( y .x. ( 2 .x. x ) ) )
19 simpl2 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> x e. B )
20 1 3 mulg1 
 |-  ( x e. B -> ( 1 .x. x ) = x )
21 19 20 syl 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( 1 .x. x ) = x )
22 10 adantr 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> G e. Grp )
23 simprl 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> y e. ZZ )
24 11 a1i 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> 2 e. ZZ )
25 1 3 mulgassr 
 |-  ( ( G e. Grp /\ ( y e. ZZ /\ 2 e. ZZ /\ x e. B ) ) -> ( ( 2 x. y ) .x. x ) = ( y .x. ( 2 .x. x ) ) )
26 22 23 24 19 25 syl13anc 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( ( 2 x. y ) .x. x ) = ( y .x. ( 2 .x. x ) ) )
27 18 21 26 3eqtr4rd 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( ( 2 x. y ) .x. x ) = ( 1 .x. x ) )
28 24 23 zmulcld 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( 2 x. y ) e. ZZ )
29 1zzd 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> 1 e. ZZ )
30 1 4 3 2 odcong 
 |-  ( ( G e. Grp /\ x e. B /\ ( ( 2 x. y ) e. ZZ /\ 1 e. ZZ ) ) -> ( ( O ` x ) || ( ( 2 x. y ) - 1 ) <-> ( ( 2 x. y ) .x. x ) = ( 1 .x. x ) ) )
31 22 19 28 29 30 syl112anc 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( ( O ` x ) || ( ( 2 x. y ) - 1 ) <-> ( ( 2 x. y ) .x. x ) = ( 1 .x. x ) ) )
32 27 31 mpbird 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( O ` x ) || ( ( 2 x. y ) - 1 ) )
33 0zd 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> 0 e. ZZ )
34 zneo 
 |-  ( ( y e. ZZ /\ 0 e. ZZ ) -> ( 2 x. y ) =/= ( ( 2 x. 0 ) + 1 ) )
35 2t0e0 
 |-  ( 2 x. 0 ) = 0
36 35 oveq1i 
 |-  ( ( 2 x. 0 ) + 1 ) = ( 0 + 1 )
37 0p1e1 
 |-  ( 0 + 1 ) = 1
38 36 37 eqtri 
 |-  ( ( 2 x. 0 ) + 1 ) = 1
39 38 a1i 
 |-  ( ( y e. ZZ /\ 0 e. ZZ ) -> ( ( 2 x. 0 ) + 1 ) = 1 )
40 34 39 neeqtrd 
 |-  ( ( y e. ZZ /\ 0 e. ZZ ) -> ( 2 x. y ) =/= 1 )
41 oveq1 
 |-  ( ( ( 2 x. y ) - 1 ) = 0 -> ( ( ( 2 x. y ) - 1 ) + 1 ) = ( 0 + 1 ) )
42 41 37 eqtr2di 
 |-  ( ( ( 2 x. y ) - 1 ) = 0 -> 1 = ( ( ( 2 x. y ) - 1 ) + 1 ) )
43 42 adantl 
 |-  ( ( y e. ZZ /\ ( ( 2 x. y ) - 1 ) = 0 ) -> 1 = ( ( ( 2 x. y ) - 1 ) + 1 ) )
44 2cnd 
 |-  ( y e. ZZ -> 2 e. CC )
45 zcn 
 |-  ( y e. ZZ -> y e. CC )
46 44 45 mulcld 
 |-  ( y e. ZZ -> ( 2 x. y ) e. CC )
47 1cnd 
 |-  ( ( ( 2 x. y ) - 1 ) = 0 -> 1 e. CC )
48 npcan 
 |-  ( ( ( 2 x. y ) e. CC /\ 1 e. CC ) -> ( ( ( 2 x. y ) - 1 ) + 1 ) = ( 2 x. y ) )
49 46 47 48 syl2an 
 |-  ( ( y e. ZZ /\ ( ( 2 x. y ) - 1 ) = 0 ) -> ( ( ( 2 x. y ) - 1 ) + 1 ) = ( 2 x. y ) )
50 43 49 eqtr2d 
 |-  ( ( y e. ZZ /\ ( ( 2 x. y ) - 1 ) = 0 ) -> ( 2 x. y ) = 1 )
51 50 ex 
 |-  ( y e. ZZ -> ( ( ( 2 x. y ) - 1 ) = 0 -> ( 2 x. y ) = 1 ) )
52 51 necon3ad 
 |-  ( y e. ZZ -> ( ( 2 x. y ) =/= 1 -> -. ( ( 2 x. y ) - 1 ) = 0 ) )
53 40 52 syl5 
 |-  ( y e. ZZ -> ( ( y e. ZZ /\ 0 e. ZZ ) -> -. ( ( 2 x. y ) - 1 ) = 0 ) )
54 53 anabsi5 
 |-  ( ( y e. ZZ /\ 0 e. ZZ ) -> -. ( ( 2 x. y ) - 1 ) = 0 )
55 23 33 54 syl2anc 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> -. ( ( 2 x. y ) - 1 ) = 0 )
56 28 29 zsubcld 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( ( 2 x. y ) - 1 ) e. ZZ )
57 0dvds 
 |-  ( ( ( 2 x. y ) - 1 ) e. ZZ -> ( 0 || ( ( 2 x. y ) - 1 ) <-> ( ( 2 x. y ) - 1 ) = 0 ) )
58 56 57 syl 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( 0 || ( ( 2 x. y ) - 1 ) <-> ( ( 2 x. y ) - 1 ) = 0 ) )
59 55 58 mtbird 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> -. 0 || ( ( 2 x. y ) - 1 ) )
60 nbrne2 
 |-  ( ( ( O ` x ) || ( ( 2 x. y ) - 1 ) /\ -. 0 || ( ( 2 x. y ) - 1 ) ) -> ( O ` x ) =/= 0 )
61 32 59 60 syl2anc 
 |-  ( ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) /\ ( y e. ZZ /\ x = ( y .x. ( 2 .x. x ) ) ) ) -> ( O ` x ) =/= 0 )
62 17 61 rexlimddv 
 |-  ( ( ph /\ x e. B /\ ( 2 .x. x ) =/= .0. ) -> ( O ` x ) =/= 0 )
63 62 3expa 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) =/= .0. ) -> ( O ` x ) =/= 0 )