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

Metamath Proof Explorer

Theorem ring0cl

Description: The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014)

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

Proof

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