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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	0ringsubrg.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	0ringsubrg.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
	0ringsubrg.4	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
Assertion	0ringsubrg	⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		0ringsubrg.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		0ringsubrg.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		0ringsubrg.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = 1 )
4		0ringsubrg.4	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
5	1	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
6	4 5	syl	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8	1 7	0ring	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { ( 0g ‘ 𝑅 ) } )
9	2 3 8	syl2anc	⊢ ( 𝜑 → 𝐵 = { ( 0g ‘ 𝑅 ) } )
10	6 9	sseqtrd	⊢ ( 𝜑 → 𝑆 ⊆ { ( 0g ‘ 𝑅 ) } )
11		sssn	⊢ ( 𝑆 ⊆ { ( 0g ‘ 𝑅 ) } ↔ ( 𝑆 = ∅ ∨ 𝑆 = { ( 0g ‘ 𝑅 ) } ) )
12	10 11	sylib	⊢ ( 𝜑 → ( 𝑆 = ∅ ∨ 𝑆 = { ( 0g ‘ 𝑅 ) } ) )
13		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
14	13	subrg1cl	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
15	4 14	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
16		n0i	⊢ ( ( 1r ‘ 𝑅 ) ∈ 𝑆 → ¬ 𝑆 = ∅ )
17	15 16	syl	⊢ ( 𝜑 → ¬ 𝑆 = ∅ )
18	12 17	orcnd	⊢ ( 𝜑 → 𝑆 = { ( 0g ‘ 𝑅 ) } )
19	18	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) )
20		fvex	⊢ ( 0g ‘ 𝑅 ) ∈ V
21		hashsng	⊢ ( ( 0g ‘ 𝑅 ) ∈ V → ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = 1 )
22	20 21	ax-mp	⊢ ( ♯ ‘ { ( 0g ‘ 𝑅 ) } ) = 1
23	19 22	eqtrdi	⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = 1 )