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

Metamath Proof Explorer

Theorem rngisomfv1

Description: If there is a non-unital ring isomorphism between a unital ring and a non-unital ring, then the function value of the ring unity of the unital ring is an element of the base set of the non-unital ring. (Contributed by AV, 27-Feb-2025)

Ref Expression
Hypotheses rngisom1.1 
|- .1. = ( 1r ` R )
rngisom1.b 
|- B = ( Base ` S )
Assertion rngisomfv1 
|- ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> ( F ` .1. ) e. B )

Proof

Step Hyp Ref Expression
1 rngisom1.1 
 |-  .1. = ( 1r ` R )
2 rngisom1.b 
 |-  B = ( Base ` S )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 2 rngimf1o 
 |-  ( F e. ( R RngIso S ) -> F : ( Base ` R ) -1-1-onto-> B )
5 f1of 
 |-  ( F : ( Base ` R ) -1-1-onto-> B -> F : ( Base ` R ) --> B )
6 4 5 syl 
 |-  ( F e. ( R RngIso S ) -> F : ( Base ` R ) --> B )
7 6 adantl 
 |-  ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> F : ( Base ` R ) --> B )
8 3 1 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
9 8 adantr 
 |-  ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> .1. e. ( Base ` R ) )
10 7 9 ffvelcdmd 
 |-  ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> ( F ` .1. ) e. B )