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		oveq2	⊢ ( 𝑍 = 𝐵 → ( 𝐺 ↾s 𝑍 ) = ( 𝐺 ↾s 𝐵 ) )
15	3	oveq2i	⊢ ( 𝐺 ↾s 𝑍 ) = ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) )
16	14 15	eqtr3di	⊢ ( 𝑍 = 𝐵 → ( 𝐺 ↾s 𝐵 ) = ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → ( 𝐺 ↾s 𝐵 ) = ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) )
18	1	ressid	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ↾s 𝐵 ) = 𝐺 )
19	5 18	syl	⊢ ( 𝜑 → ( 𝐺 ↾s 𝐵 ) = 𝐺 )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → ( 𝐺 ↾s 𝐵 ) = 𝐺 )
21	17 20	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) = 𝐺 )
22		eqid	⊢ ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) = ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) )
23	22	cntrabl	⊢ ( 𝐺 ∈ Grp → ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) ∈ Abel )
24	5 23	syl	⊢ ( 𝜑 → ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) ∈ Abel )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → ( 𝐺 ↾s ( Cntr ‘ 𝐺 ) ) ∈ Abel )
26	21 25	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑍 = 𝐵 ) → 𝐺 ∈ Abel )
27	26	orim2i	⊢ ( ( 𝑍 = { 0 } ∨ ( 𝜑 ∧ 𝑍 = 𝐵 ) ) → ( 𝑍 = { 0 } ∨ 𝐺 ∈ Abel ) )
28	9 11 13 27	4syl	⊢ ( 𝜑 → ( 𝑍 = { 0 } ∨ 𝐺 ∈ Abel ) )