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

Metamath Proof Explorer

Theorem subrng0

Description: A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025)

Step	Hyp	Ref	Expression
1		subrng0.1	$⊢ S = R ↾_{𝑠} A$
2		subrng0.2	$⊢ \underset{˙}{0} = 0_{R}$
3		subrngsubg	$⊢ A \in SubRng (R) \to A \in SubGrp (R)$
4	1 2	subg0	$⊢ A \in SubGrp (R) \to \underset{˙}{0} = 0_{S}$
5	3 4	syl	$⊢ A \in SubRng (R) \to \underset{˙}{0} = 0_{S}$