Theorem rngen1zr0

Description: The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010) (Revised by AV, 18-Jun-2026)

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

Proof

Step	Hyp	Ref	Expression
1		rng1zr.b	|- B = ( Base ` R )
2		rng1zr.p	|- .+ = ( +g ` R )
3		rng1zr.t	|- .* = ( .r ` R )
4		rngen1zr0.0	|- .0. = ( 0g ` R )
5	1 4	rng0cl	|- ( R e. Rng -> .0. e. B )
6	5	3ad2ant1	|- ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> .0. e. B )
7	1 2 3	rngen1zr	|- ( ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ .0. e. B ) -> ( B ~~ 1o <-> ( .+ = { <. <. .0. , .0. >. , .0. >. } /\ .* = { <. <. .0. , .0. >. , .0. >. } ) ) )
8	6 7	mpdan	|- ( ( R e. Rng /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. .0. , .0. >. , .0. >. } /\ .* = { <. <. .0. , .0. >. , .0. >. } ) ) )