This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rng0cl

Description: The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025)

Ref Expression
Hypotheses rng0cl.b ⊢ B = Base R
rng0cl.z ⊢ 0 ˙ = 0 R
Assertion rng0cl ⊢ R ∈ Rng → 0 ˙ ∈ B

Proof

Step Hyp Ref Expression
1 rng0cl.b ⊢ B = Base R
2 rng0cl.z ⊢ 0 ˙ = 0 R
3 rnggrp ⊢ R ∈ Rng → R ∈ Grp
4 1 2 grpidcl ⊢ R ∈ Grp → 0 ˙ ∈ B
5 3 4 syl ⊢ R ∈ Rng → 0 ˙ ∈ B