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 ˙ = 0 G
simpcntrab.c ⊢ Z = Cntr ⁡ G
simpcntrab.d ⊢ φ → G ∈ SimpGrp
Assertion simpcntrab ⊢ φ → Z = 0 ˙ ∨ G ∈ Abel

Proof

Step Hyp Ref Expression
1 simpcntrab.a ⊢ B = Base G
2 simpcntrab.b ⊢ 0 ˙ = 0 G
3 simpcntrab.c ⊢ Z = Cntr ⁡ G
4 simpcntrab.d ⊢ φ → G ∈ SimpGrp
5 4 simpggrpd ⊢ φ → G ∈ Grp
6 3 cntrnsg ⊢ G ∈ Grp → Z ∈ NrmSGrp ⁡ G
7 5 6 syl ⊢ φ → Z ∈ NrmSGrp ⁡ G
8 1 2 4 7 simpgnsgeqd ⊢ φ → Z = 0 ˙ ∨ Z = B
9 8 ancli ⊢ φ → φ ∧ Z = 0 ˙ ∨ Z = B
10 andi ⊢ φ ∧ Z = 0 ˙ ∨ Z = B ↔ φ ∧ Z = 0 ˙ ∨ φ ∧ Z = B
11 10 biimpi ⊢ φ ∧ Z = 0 ˙ ∨ Z = B → φ ∧ Z = 0 ˙ ∨ φ ∧ Z = B
12 simpr ⊢ φ ∧ Z = 0 ˙ → Z = 0 ˙
13 12 orim1i ⊢ φ ∧ Z = 0 ˙ ∨ φ ∧ Z = B → Z = 0 ˙ ∨ φ ∧ Z = B
14 oveq2 ⊢ Z = B → G ↾ 𝑠 Z = G ↾ 𝑠 B
15 3 oveq2i ⊢ G ↾ 𝑠 Z = G ↾ 𝑠 Cntr ⁡ G
16 14 15 eqtr3di ⊢ Z = B → G ↾ 𝑠 B = G ↾ 𝑠 Cntr ⁡ G
17 16 adantl ⊢ φ ∧ Z = B → G ↾ 𝑠 B = G ↾ 𝑠 Cntr ⁡ G
18 1 ressid ⊢ G ∈ Grp → G ↾ 𝑠 B = G
19 5 18 syl ⊢ φ → G ↾ 𝑠 B = G
20 19 adantr ⊢ φ ∧ Z = B → G ↾ 𝑠 B = G
21 17 20 eqtr3d ⊢ φ ∧ Z = B → G ↾ 𝑠 Cntr ⁡ G = G
22 eqid ⊢ G ↾ 𝑠 Cntr ⁡ G = G ↾ 𝑠 Cntr ⁡ G
23 22 cntrabl ⊢ G ∈ Grp → G ↾ 𝑠 Cntr ⁡ G ∈ Abel
24 5 23 syl ⊢ φ → G ↾ 𝑠 Cntr ⁡ G ∈ Abel
25 24 adantr ⊢ φ ∧ Z = B → G ↾ 𝑠 Cntr ⁡ G ∈ Abel
26 21 25 eqeltrrd ⊢ φ ∧ Z = B → G ∈ Abel
27 26 orim2i ⊢ Z = 0 ˙ ∨ φ ∧ Z = B → Z = 0 ˙ ∨ G ∈ Abel
28 9 11 13 27 4syl ⊢ φ → Z = 0 ˙ ∨ G ∈ Abel