0ringsubrg

Description: A subring of a zero ring is a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025)

Step	Hyp	Ref	Expression
1		0ringsubrg.1	$⊢ B = {Base}_{R}$
2		0ringsubrg.2	$⊢ φ \to R \in Ring$
3		0ringsubrg.3	$⊢ φ \to \|B\| = 1$
4		0ringsubrg.4	$⊢ φ \to S \in SubRing (R)$
5	1	subrgss	$⊢ S \in SubRing (R) \to S \subseteq B$
6	4 5	syl	$⊢ φ \to S \subseteq B$
7		eqid	$⊢ 0_{R} = 0_{R}$
8	1 7	0ring	$⊢ (R \in Ring \land \|B\| = 1) \to B = \{0_{R}\}$
9	2 3 8	syl2anc	$⊢ φ \to B = \{0_{R}\}$
10	6 9	sseqtrd	$⊢ φ \to S \subseteq \{0_{R}\}$
11		sssn	$⊢ S \subseteq \{0_{R}\} \leftrightarrow (S = \emptyset \lor S = \{0_{R}\})$
12	10 11	sylib	$⊢ φ \to (S = \emptyset \lor S = \{0_{R}\})$
13		eqid	$⊢ 1_{R} = 1_{R}$
14	13	subrg1cl	$⊢ S \in SubRing (R) \to 1_{R} \in S$
15	4 14	syl	$⊢ φ \to 1_{R} \in S$
16		n0i	$⊢ 1_{R} \in S \to \neg S = \emptyset$
17	15 16	syl	$⊢ φ \to \neg S = \emptyset$
18	12 17	orcnd	$⊢ φ \to S = \{0_{R}\}$
19	18	fveq2d	$⊢ φ \to \|S\| = \|\{0_{R}\}\|$
20		fvex	$⊢ 0_{R} \in V$
21		hashsng	$⊢ 0_{R} \in V \to \|\{0_{R}\}\| = 1$
22	20 21	ax-mp	$⊢ \|\{0_{R}\}\| = 1$
23	19 22	eqtrdi	$⊢ φ \to \|S\| = 1$

Metamath Proof Explorer