Theorem rng1zr

Description: The only ring 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, 18-Jun-2026)

	Ref	Expression
Hypotheses	rng1zr.b	|- B = ( Base ` R )
	rng1zr.p	|- .+ = ( +g ` R )
	rng1zr.t	|- .* = ( .r ` R )
Assertion	rng1zr	|- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )

Proof

Step	Hyp	Ref	Expression
1		rng1zr.b	|- B = ( Base ` R )
2		rng1zr.p	|- .+ = ( +g ` R )
3		rng1zr.t	|- .* = ( .r ` R )
4		rnggrp	|- ( R e. Rng -> R e. Grp )
5	4	grpmgmd	|- ( R e. Rng -> R e. Mgm )
6		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
7	6	rngmgp	|- ( R e. Rng -> ( mulGrp ` R ) e. Smgrp )
8		sgrpmgm	|- ( ( mulGrp ` R ) e. Smgrp -> ( mulGrp ` R ) e. Mgm )
9	7 8	syl	|- ( R e. Rng -> ( mulGrp ` R ) e. Mgm )
10	5 9	jca	|- ( R e. Rng -> ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) )
11	10	3ad2ant1	|- ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) )
12	11	adantr	|- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) )
13		3simpc	|- ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) )
14	13	adantr	|- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) )
15		simpr	|- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> Z e. B )
16	1 2 3	rng1zrlem	|- ( ( ( R e. Mgm /\ ( mulGrp ` R ) e. Mgm ) /\ ( .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
17	12 14 15 16	syl3anc	|- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )