Theorem 0ringsubrg

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

	Ref	Expression
Hypotheses	0ringsubrg.1	$$⊢B={\mathrm{Base}}_R$$
	0ringsubrg.2	$$⊢\phi \to R\in \mathrm{Ring}$$
	0ringsubrg.3	$$⊢\phi \to \left|B\right|=1$$
	0ringsubrg.4	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
Assertion	0ringsubrg	$$⊢\phi \to \left|S\right|=1$$

Proof

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