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 9 11 13 3syl ⊢ φ → Z = 0 ˙ ∨ φ ∧ Z = B
15 oveq2 ⊢ Z = B → G ↾ 𝑠 Z = G ↾ 𝑠 B
16 3 oveq2i ⊢ G ↾ 𝑠 Z = G ↾ 𝑠 Cntr ⁡ G
17 15 16 eqtr3di ⊢ Z = B → G ↾ 𝑠 B = G ↾ 𝑠 Cntr ⁡ G
18 17 adantl ⊢ φ ∧ Z = B → G ↾ 𝑠 B = G ↾ 𝑠 Cntr ⁡ G
19 1 ressid ⊢ G ∈ Grp → G ↾ 𝑠 B = G
20 5 19 syl ⊢ φ → G ↾ 𝑠 B = G
21 20 adantr ⊢ φ ∧ Z = B → G ↾ 𝑠 B = G
22 18 21 eqtr3d ⊢ φ ∧ Z = B → G ↾ 𝑠 Cntr ⁡ G = G
23 eqid ⊢ G ↾ 𝑠 Cntr ⁡ G = G ↾ 𝑠 Cntr ⁡ G
24 23 cntrabl ⊢ G ∈ Grp → G ↾ 𝑠 Cntr ⁡ G ∈ Abel
25 5 24 syl ⊢ φ → G ↾ 𝑠 Cntr ⁡ G ∈ Abel
26 25 adantr ⊢ φ ∧ Z = B → G ↾ 𝑠 Cntr ⁡ G ∈ Abel
27 22 26 eqeltrrd ⊢ φ ∧ Z = B → G ∈ Abel
28 27 orim2i ⊢ Z = 0 ˙ ∨ φ ∧ Z = B → Z = 0 ˙ ∨ G ∈ Abel
29 14 28 syl ⊢ φ → Z = 0 ˙ ∨ G ∈ Abel