Theorem srg1zr

Description: The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010) (Revised by AV, 25-Jan-2020) (Proof shortened by AV, 19-Jun-2026)

	Ref	Expression
Hypotheses	srg1zr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	srg1zr.p	⊢ + = ( +g ‘ 𝑅 )
	srg1zr.t	⊢ ∗ = ( .r ‘ 𝑅 )
Assertion	srg1zr	⊢ ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )

Proof

Step	Hyp	Ref	Expression
1		srg1zr.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		srg1zr.p	⊢ + = ( +g ‘ 𝑅 )
3		srg1zr.t	⊢ ∗ = ( .r ‘ 𝑅 )
4		srgmnd	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
5		mndmgm	⊢ ( 𝑅 ∈ Mnd → 𝑅 ∈ Mgm )
6	4 5	syl	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mgm )
7		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
8	7	srgmgp	⊢ ( 𝑅 ∈ SRing → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
9		mndmgm	⊢ ( ( mulGrp ‘ 𝑅 ) ∈ Mnd → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
10	8 9	syl	⊢ ( 𝑅 ∈ SRing → ( mulGrp ‘ 𝑅 ) ∈ Mgm )
11	6 10	jca	⊢ ( 𝑅 ∈ SRing → ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) )
12	11	3ad2ant1	⊢ ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) )
13	12	adantr	⊢ ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) )
14		3simpc	⊢ ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) → ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) )
15	14	adantr	⊢ ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) )
16		simpr	⊢ ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ∈ 𝐵 )
17	1 2 3	rng1zrlem	⊢ ( ( ( 𝑅 ∈ Mgm ∧ ( mulGrp ‘ 𝑅 ) ∈ Mgm ) ∧ ( + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )
18	13 15 16 17	syl3anc	⊢ ( ( ( 𝑅 ∈ SRing ∧ + Fn ( 𝐵 × 𝐵 ) ∧ ∗ Fn ( 𝐵 × 𝐵 ) ) ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ ( + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ∧ ∗ = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) ) )