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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	simpcntrab.b	⊢ 0 = ( 0g ‘ 𝐺 )
	simpcntrab.c	⊢ 𝑍 = ( Cntr ‘ 𝐺 )
	simpcntrab.d	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
Assertion	simpcntrab	⊢ ( 𝜑 → ( 𝑍 = { 0 } ∨ 𝐺 ∈ Abel ) )

Proof

Step	Hyp	Ref	Expression
1		simpcntrab.a	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		simpcntrab.b	⊢ 0 = ( 0g ‘ 𝐺 )
3		simpcntrab.c	⊢ 𝑍 = ( Cntr ‘ 𝐺 )
4		simpcntrab.d	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
5	4	simpggrpd	⊢ ( 𝜑 → 𝐺 ∈ Grp )
6	3	cntrnsg	⊢ ( 𝐺 ∈ Grp → 𝑍 ∈ ( NrmSGrp ‘ 𝐺 ) )
7	5 6	syl	⊢ ( 𝜑 → 𝑍 ∈ ( NrmSGrp ‘ 𝐺 ) )
8	1 2 4 7	simpgnsgeqd	⊢ ( 𝜑 → ( 𝑍 = { 0 } ∨ 𝑍 = 𝐵 ) )
9	8	ancli	⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝑍 = { 0 } ∨ 𝑍 = 𝐵 ) ) )
10		andi	⊢ ( ( 𝜑 ∧ ( 𝑍 = { 0 } ∨ 𝑍 = 𝐵 ) ) ↔ ( ( 𝜑 ∧ 𝑍 = { 0 } ) ∨ ( 𝜑 ∧ 𝑍 = 𝐵 ) ) )
11	10	biimpi	⊢ ( ( 𝜑 ∧ ( 𝑍 = { 0 } ∨ 𝑍 = 𝐵 ) ) → ( ( 𝜑 ∧ 𝑍 = { 0 } ) ∨ ( 𝜑 ∧ 𝑍 = 𝐵 ) ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑍 = { 0 } ) → 𝑍 = { 0 } )
13	12	orim1i	⊢ ( ( ( 𝜑 ∧ 𝑍 = { 0 } ) ∨ ( 𝜑 ∧ 𝑍 = 𝐵 ) ) → ( 𝑍 = { 0 } ∨ ( 𝜑 ∧ 𝑍 = 𝐵 ) ) )
14	9 11 13	3syl	⊢ ( 𝜑 → ( 𝑍 = { 0 } ∨ ( 𝜑 ∧ 𝑍 = 𝐵 ) ) )
15		oveq2	⊢ ( 𝑍 = 𝐵 → ( 𝐺 ↾s 𝑍 ) = ( 𝐺 ↾s 𝐵 ) )
16	3	oveq2i	⊢ ( 𝐺 ↾s 𝑍 ) = ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) )
17	15 16	eqtr3di	⊢ ( 𝑍 = 𝐵 → ( 𝐺 ↾s 𝐵 ) = ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → ( 𝐺 ↾s 𝐵 ) = ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) )
19	1	ressid	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ↾s 𝐵 ) = 𝐺 )
20	5 19	syl	⊢ ( 𝜑 → ( 𝐺 ↾s 𝐵 ) = 𝐺 )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → ( 𝐺 ↾s 𝐵 ) = 𝐺 )
22	18 21	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) = 𝐺 )
23		eqid	⊢ ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) = ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) )
24	23	cntrabl	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) ∈ Abel )
25	5 24	syl	⊢ ( 𝜑 → ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) ∈ Abel )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) ∈ Abel )
27	22 26	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → 𝐺 ∈ Abel )
28	27	orim2i	⊢ ( ( 𝑍 = { 0 } ∨ ( 𝜑 ∧ 𝑍 = 𝐵 ) ) → ( 𝑍 = { 0 } ∨ 𝐺 ∈ Abel ) )
29	14 28	syl	⊢ ( 𝜑 → ( 𝑍 = { 0 } ∨ 𝐺 ∈ Abel ) )