Metamath Proof Explorer

Theorem simpcntrab

Description: The center of a simple group is trivial or the group is abelian. (Contributed by SS, 3-Jan-2024)

Ref Expression
Hypotheses simpcntrab.a 
|- B = ( Base ` G )
simpcntrab.b 
|- .0. = ( 0g ` G )
simpcntrab.c 
|- Z = ( Cntr ` G )
simpcntrab.d 
|- ( ph -> G e. SimpGrp )
Assertion simpcntrab 
|- ( ph -> ( Z = { .0. } \/ G e. Abel ) )

Proof

Step Hyp Ref Expression
1 simpcntrab.a 
 |-  B = ( Base ` G )
2 simpcntrab.b 
 |-  .0. = ( 0g ` G )
3 simpcntrab.c 
 |-  Z = ( Cntr ` G )
4 simpcntrab.d 
 |-  ( ph -> G e. SimpGrp )
5 4 simpggrpd 
 |-  ( ph -> G e. Grp )
6 3 cntrnsg 
 |-  ( G e. Grp -> Z e. ( NrmSGrp ` G ) )
7 5 6 syl 
 |-  ( ph -> Z e. ( NrmSGrp ` G ) )
8 1 2 4 7 simpgnsgeqd 
 |-  ( ph -> ( Z = { .0. } \/ Z = B ) )
9 8 ancli 
 |-  ( ph -> ( ph /\ ( Z = { .0. } \/ Z = B ) ) )
10 andi 
 |-  ( ( ph /\ ( Z = { .0. } \/ Z = B ) ) <-> ( ( ph /\ Z = { .0. } ) \/ ( ph /\ Z = B ) ) )
11 10 biimpi 
 |-  ( ( ph /\ ( Z = { .0. } \/ Z = B ) ) -> ( ( ph /\ Z = { .0. } ) \/ ( ph /\ Z = B ) ) )
12 simpr 
 |-  ( ( ph /\ Z = { .0. } ) -> Z = { .0. } )
13 12 orim1i 
 |-  ( ( ( ph /\ Z = { .0. } ) \/ ( ph /\ Z = B ) ) -> ( Z = { .0. } \/ ( ph /\ Z = B ) ) )
14 oveq2 
 |-  ( Z = B -> ( G |`s Z ) = ( G |`s B ) )
15 3 oveq2i 
 |-  ( G |`s Z ) = ( G |`s ( Cntr ` G ) )
16 14 15 eqtr3di 
 |-  ( Z = B -> ( G |`s B ) = ( G |`s ( Cntr ` G ) ) )
17 16 adantl 
 |-  ( ( ph /\ Z = B ) -> ( G |`s B ) = ( G |`s ( Cntr ` G ) ) )
18 1 ressid 
 |-  ( G e. Grp -> ( G |`s B ) = G )
19 5 18 syl 
 |-  ( ph -> ( G |`s B ) = G )
20 19 adantr 
 |-  ( ( ph /\ Z = B ) -> ( G |`s B ) = G )
21 17 20 eqtr3d 
 |-  ( ( ph /\ Z = B ) -> ( G |`s ( Cntr ` G ) ) = G )
22 eqid 
 |-  ( G |`s ( Cntr ` G ) ) = ( G |`s ( Cntr ` G ) )
23 22 cntrabl 
 |-  ( G e. Grp -> ( G |`s ( Cntr ` G ) ) e. Abel )
24 5 23 syl 
 |-  ( ph -> ( G |`s ( Cntr ` G ) ) e. Abel )
25 24 adantr 
 |-  ( ( ph /\ Z = B ) -> ( G |`s ( Cntr ` G ) ) e. Abel )
26 21 25 eqeltrrd 
 |-  ( ( ph /\ Z = B ) -> G e. Abel )
27 26 orim2i 
 |-  ( ( Z = { .0. } \/ ( ph /\ Z = B ) ) -> ( Z = { .0. } \/ G e. Abel ) )
28 9 11 13 27 4syl 
 |-  ( ph -> ( Z = { .0. } \/ G e. Abel ) )