Metamath Proof Explorer

Theorem rngisomring

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then both rings are unital. (Contributed by AV, 27-Feb-2025)

Ref Expression
Assertion rngisomring 
|- ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIsom S ) ) -> S e. Ring )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIsom S ) ) -> S e. Rng )
2 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
3 eqid 
 |-  ( Base ` S ) = ( Base ` S )
4 2 3 rngisomfv1 
 |-  ( ( R e. Ring /\ F e. ( R RngIsom S ) ) -> ( F ` ( 1r ` R ) ) e. ( Base ` S ) )
5 4 3adant2 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIsom S ) ) -> ( F ` ( 1r ` R ) ) e. ( Base ` S ) )
6 oveq1 
 |-  ( i = ( F ` ( 1r ` R ) ) -> ( i ( .r ` S ) x ) = ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) )
7 6 eqeq1d 
 |-  ( i = ( F ` ( 1r ` R ) ) -> ( ( i ( .r ` S ) x ) = x <-> ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x ) )
8 oveq2 
 |-  ( i = ( F ` ( 1r ` R ) ) -> ( x ( .r ` S ) i ) = ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) )
9 8 eqeq1d 
 |-  ( i = ( F ` ( 1r ` R ) ) -> ( ( x ( .r ` S ) i ) = x <-> ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) )
10 7 9 anbi12d 
 |-  ( i = ( F ` ( 1r ` R ) ) -> ( ( ( i ( .r ` S ) x ) = x /\ ( x ( .r ` S ) i ) = x ) <-> ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) )
11 10 ralbidv 
 |-  ( i = ( F ` ( 1r ` R ) ) -> ( A. x e. ( Base ` S ) ( ( i ( .r ` S ) x ) = x /\ ( x ( .r ` S ) i ) = x ) <-> A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) )
12 11 adantl 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIsom S ) ) /\ i = ( F ` ( 1r ` R ) ) ) -> ( A. x e. ( Base ` S ) ( ( i ( .r ` S ) x ) = x /\ ( x ( .r ` S ) i ) = x ) <-> A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) )
13 eqid 
 |-  ( .r ` S ) = ( .r ` S )
14 2 3 13 rngisom1 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIsom S ) ) -> A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) )
15 5 12 14 rspcedvd 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIsom S ) ) -> E. i e. ( Base ` S ) A. x e. ( Base ` S ) ( ( i ( .r ` S ) x ) = x /\ ( x ( .r ` S ) i ) = x ) )
16 3 13 isringrng 
 |-  ( S e. Ring <-> ( S e. Rng /\ E. i e. ( Base ` S ) A. x e. ( Base ` S ) ( ( i ( .r ` S ) x ) = x /\ ( x ( .r ` S ) i ) = x ) ) )
17 1 15 16 sylanbrc 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIsom S ) ) -> S e. Ring )