Metamath Proof Explorer

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 
|- 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 ablsimpgfindlem2 
|- ( ( ( 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 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) = .0. ) -> ( 2 .x. x ) = .0. )
8 6 simpggrpd 
 |-  ( ph -> G e. Grp )
9 8 adantr 
 |-  ( ( ph /\ x e. B ) -> G e. Grp )
10 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
11 2z 
 |-  2 e. ZZ
12 11 a1i 
 |-  ( ( ph /\ x e. B ) -> 2 e. ZZ )
13 9 10 12 3jca 
 |-  ( ( ph /\ x e. B ) -> ( G e. Grp /\ x e. B /\ 2 e. ZZ ) )
14 13 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) = .0. ) -> ( G e. Grp /\ x e. B /\ 2 e. ZZ ) )
15 1 4 3 2 oddvds 
 |-  ( ( G e. Grp /\ x e. B /\ 2 e. ZZ ) -> ( ( O ` x ) || 2 <-> ( 2 .x. x ) = .0. ) )
16 14 15 syl 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) = .0. ) -> ( ( O ` x ) || 2 <-> ( 2 .x. x ) = .0. ) )
17 7 16 mpbird 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) = .0. ) -> ( O ` x ) || 2 )
18 2ne0 
 |-  2 =/= 0
19 18 a1i 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) = .0. ) -> 2 =/= 0 )
20 19 neneqd 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) = .0. ) -> -. 2 = 0 )
21 0dvds 
 |-  ( 2 e. ZZ -> ( 0 || 2 <-> 2 = 0 ) )
22 11 21 ax-mp 
 |-  ( 0 || 2 <-> 2 = 0 )
23 20 22 sylnibr 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) = .0. ) -> -. 0 || 2 )
24 nbrne2 
 |-  ( ( ( O ` x ) || 2 /\ -. 0 || 2 ) -> ( O ` x ) =/= 0 )
25 17 23 24 syl2anc 
 |-  ( ( ( ph /\ x e. B ) /\ ( 2 .x. x ) = .0. ) -> ( O ` x ) =/= 0 )