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

Metamath Proof Explorer

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 )