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 9 11 13 3syl 
 |-  ( ph -> ( Z = { .0. } \/ ( ph /\ Z = B ) ) )
15 oveq2 
 |-  ( Z = B -> ( G |`s Z ) = ( G |`s B ) )
16 3 oveq2i 
 |-  ( G |`s Z ) = ( G |`s ( Cntr ` G ) )
17 15 16 eqtr3di 
 |-  ( Z = B -> ( G |`s B ) = ( G |`s ( Cntr ` G ) ) )
18 17 adantl 
 |-  ( ( ph /\ Z = B ) -> ( G |`s B ) = ( G |`s ( Cntr ` G ) ) )
19 1 ressid 
 |-  ( G e. Grp -> ( G |`s B ) = G )
20 5 19 syl 
 |-  ( ph -> ( G |`s B ) = G )
21 20 adantr 
 |-  ( ( ph /\ Z = B ) -> ( G |`s B ) = G )
22 18 21 eqtr3d 
 |-  ( ( ph /\ Z = B ) -> ( G |`s ( Cntr ` G ) ) = G )
23 eqid 
 |-  ( G |`s ( Cntr ` G ) ) = ( G |`s ( Cntr ` G ) )
24 23 cntrabl 
 |-  ( G e. Grp -> ( G |`s ( Cntr ` G ) ) e. Abel )
25 5 24 syl 
 |-  ( ph -> ( G |`s ( Cntr ` G ) ) e. Abel )
26 25 adantr 
 |-  ( ( ph /\ Z = B ) -> ( G |`s ( Cntr ` G ) ) e. Abel )
27 22 26 eqeltrrd 
 |-  ( ( ph /\ Z = B ) -> G e. Abel )
28 27 orim2i 
 |-  ( ( Z = { .0. } \/ ( ph /\ Z = B ) ) -> ( Z = { .0. } \/ G e. Abel ) )
29 14 28 syl 
 |-  ( ph -> ( Z = { .0. } \/ G e. Abel ) )