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 
|- ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
3 1 2 issubrg 
 |-  ( A e. ( SubRing ` R ) <-> ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A ) ) )
4 ringrng 
 |-  ( R e. Ring -> R e. Rng )
5 4 ad2antrr 
 |-  ( ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A ) ) -> R e. Rng )
6 ringrng 
 |-  ( ( R |`s A ) e. Ring -> ( R |`s A ) e. Rng )
7 6 ad2antlr 
 |-  ( ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A ) ) -> ( R |`s A ) e. Rng )
8 simprl 
 |-  ( ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A ) ) -> A C_ ( Base ` R ) )
9 1 issubrng 
 |-  ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ ( Base ` R ) ) )
10 5 7 8 9 syl3anbrc 
 |-  ( ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ ( Base ` R ) /\ ( 1r ` R ) e. A ) ) -> A e. ( SubRng ` R ) )
11 3 10 sylbi 
 |-  ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) )