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

Metamath Proof Explorer

Theorem subrgsubrng

Description: A subring of a unital ring is a subring of a non-unital ring. (Contributed by AV, 30-Mar-2025)

Ref Expression
Assertion subrgsubrng ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
3 1 2 issubrg ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) )
4 ringrng ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
5 4 ad2antrr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) → 𝑅 ∈ Rng )
6 ringrng ⊢ ( ( 𝑅 ↾s 𝐴 ) ∈ Ring → ( 𝑅 ↾s 𝐴 ) ∈ Rng )
7 6 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) → ( 𝑅 ↾s 𝐴 ) ∈ Rng )
8 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) → 𝐴 ⊆ ( Base ‘ 𝑅 ) )
9 1 issubrng ⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ↔ ( 𝑅 ∈ Rng ∧ ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝐴 ⊆ ( Base ‘ 𝑅 ) ) )
10 5 7 8 9 syl3anbrc ⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑅 ↾s 𝐴 ) ∈ Ring ) ∧ ( 𝐴 ⊆ ( Base ‘ 𝑅 ) ∧ ( 1r ‘ 𝑅 ) ∈ 𝐴 ) ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) )
11 3 10 sylbi ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubRng ‘ 𝑅 ) )