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 = ( Base ` R )
	0ringsubrg.2	|- ( ph -> R e. Ring )
	0ringsubrg.3	|- ( ph -> ( # ` B ) = 1 )
	0ringsubrg.4	|- ( ph -> S e. ( SubRing ` R ) )
Assertion	0ringsubrg	|- ( ph -> ( # ` S ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		0ringsubrg.1	|- B = ( Base ` R )
2		0ringsubrg.2	|- ( ph -> R e. Ring )
3		0ringsubrg.3	|- ( ph -> ( # ` B ) = 1 )
4		0ringsubrg.4	|- ( ph -> S e. ( SubRing ` R ) )
5	1	subrgss	|- ( S e. ( SubRing ` R ) -> S C_ B )
6	4 5	syl	|- ( ph -> S C_ B )
7		eqid	|- ( 0g ` R ) = ( 0g ` R )
8	1 7	0ring	|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { ( 0g ` R ) } )
9	2 3 8	syl2anc	|- ( ph -> B = { ( 0g ` R ) } )
10	6 9	sseqtrd	|- ( ph -> S C_ { ( 0g ` R ) } )
11		sssn	|- ( S C_ { ( 0g ` R ) } <-> ( S = (/) \/ S = { ( 0g ` R ) } ) )
12	10 11	sylib	|- ( ph -> ( S = (/) \/ S = { ( 0g ` R ) } ) )
13		eqid	|- ( 1r ` R ) = ( 1r ` R )
14	13	subrg1cl	|- ( S e. ( SubRing ` R ) -> ( 1r ` R ) e. S )
15	4 14	syl	|- ( ph -> ( 1r ` R ) e. S )
16		n0i	|- ( ( 1r ` R ) e. S -> -. S = (/) )
17	15 16	syl	|- ( ph -> -. S = (/) )
18	12 17	orcnd	|- ( ph -> S = { ( 0g ` R ) } )
19	18	fveq2d	|- ( ph -> ( # ` S ) = ( # ` { ( 0g ` R ) } ) )
20		fvex	|- ( 0g ` R ) e. _V
21		hashsng	|- ( ( 0g ` R ) e. _V -> ( # ` { ( 0g ` R ) } ) = 1 )
22	20 21	ax-mp	|- ( # ` { ( 0g ` R ) } ) = 1
23	19 22	eqtrdi	|- ( ph -> ( # ` S ) = 1 )