Metamath Proof Explorer

Theorem rngisomring1

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the ring unity of the second ring is the function value of the ring unity of the first ring for the isomorphism. (Contributed by AV, 16-Mar-2025)

Ref Expression
Assertion rngisomring1 
|- ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> ( 1r ` S ) = ( F ` ( 1r ` R ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
2 eqid 
 |-  ( Base ` S ) = ( Base ` S )
3 eqid 
 |-  ( .r ` S ) = ( .r ` S )
4 1 2 3 rngisom1 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) )
5 eqidd 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) -> ( Base ` S ) = ( Base ` S ) )
6 eqidd 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) -> ( .r ` S ) = ( .r ` S ) )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 7 2 rngimf1o 
 |-  ( F e. ( R RngIso S ) -> F : ( Base ` R ) -1-1-onto-> ( Base ` S ) )
9 f1of 
 |-  ( F : ( Base ` R ) -1-1-onto-> ( Base ` S ) -> F : ( Base ` R ) --> ( Base ` S ) )
10 8 9 syl 
 |-  ( F e. ( R RngIso S ) -> F : ( Base ` R ) --> ( Base ` S ) )
11 10 3ad2ant3 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> F : ( Base ` R ) --> ( Base ` S ) )
12 7 1 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
13 12 3ad2ant1 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> ( 1r ` R ) e. ( Base ` R ) )
14 11 13 ffvelcdmd 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> ( F ` ( 1r ` R ) ) e. ( Base ` S ) )
15 14 adantr 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) -> ( F ` ( 1r ` R ) ) e. ( Base ` S ) )
16 oveq2 
 |-  ( x = y -> ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) )
17 id 
 |-  ( x = y -> x = y )
18 16 17 eqeq12d 
 |-  ( x = y -> ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x <-> ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y ) )
19 oveq1 
 |-  ( x = y -> ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) )
20 19 17 eqeq12d 
 |-  ( x = y -> ( ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x <-> ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y ) )
21 18 20 anbi12d 
 |-  ( x = y -> ( ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) <-> ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y ) ) )
22 21 rspccv 
 |-  ( A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) -> ( y e. ( Base ` S ) -> ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y ) ) )
23 22 adantl 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) -> ( y e. ( Base ` S ) -> ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y ) ) )
24 simpl 
 |-  ( ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y ) -> ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y )
25 23 24 syl6 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) -> ( y e. ( Base ` S ) -> ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y ) )
26 25 imp 
 |-  ( ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) /\ y e. ( Base ` S ) ) -> ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y )
27 simpr 
 |-  ( ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) y ) = y /\ ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y ) -> ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y )
28 23 27 syl6 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) -> ( y e. ( Base ` S ) -> ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y ) )
29 28 imp 
 |-  ( ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) /\ y e. ( Base ` S ) ) -> ( y ( .r ` S ) ( F ` ( 1r ` R ) ) ) = y )
30 5 6 15 26 29 ringurd 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ A. x e. ( Base ` S ) ( ( ( F ` ( 1r ` R ) ) ( .r ` S ) x ) = x /\ ( x ( .r ` S ) ( F ` ( 1r ` R ) ) ) = x ) ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
31 4 30 mpdan 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
32 31 eqcomd 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> ( 1r ` S ) = ( F ` ( 1r ` R ) ) )