Metamath Proof Explorer

Theorem rngisom1

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 a ring unity of the non-unital ring. (Contributed by AV, 27-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 rngisom1.1 
 |-  .1. = ( 1r ` R )
2 rngisom1.b 
 |-  B = ( Base ` S )
3 rngisom1.t 
 |-  .x. = ( .r ` S )
4 rngimcnv 
 |-  ( F e. ( R RngIso S ) -> `' F e. ( S RngIso R ) )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 2 5 rngimrnghm 
 |-  ( `' F e. ( S RngIso R ) -> `' F e. ( S RngHom R ) )
7 4 6 syl 
 |-  ( F e. ( R RngIso S ) -> `' F e. ( S RngHom R ) )
8 7 3ad2ant3 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> `' F e. ( S RngHom R ) )
9 8 adantr 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> `' F e. ( S RngHom R ) )
10 1 2 rngisomfv1 
 |-  ( ( R e. Ring /\ F e. ( R RngIso S ) ) -> ( F ` .1. ) e. B )
11 10 3adant2 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> ( F ` .1. ) e. B )
12 11 adantr 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F ` .1. ) e. B )
13 simpr 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> x e. B )
14 eqid 
 |-  ( .r ` R ) = ( .r ` R )
15 2 3 14 rnghmmul 
 |-  ( ( `' F e. ( S RngHom R ) /\ ( F ` .1. ) e. B /\ x e. B ) -> ( `' F ` ( ( F ` .1. ) .x. x ) ) = ( ( `' F ` ( F ` .1. ) ) ( .r ` R ) ( `' F ` x ) ) )
16 9 12 13 15 syl3anc 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( `' F ` ( ( F ` .1. ) .x. x ) ) = ( ( `' F ` ( F ` .1. ) ) ( .r ` R ) ( `' F ` x ) ) )
17 16 fveq2d 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F ` ( `' F ` ( ( F ` .1. ) .x. x ) ) ) = ( F ` ( ( `' F ` ( F ` .1. ) ) ( .r ` R ) ( `' F ` x ) ) ) )
18 5 2 rngimf1o 
 |-  ( F e. ( R RngIso S ) -> F : ( Base ` R ) -1-1-onto-> B )
19 18 3ad2ant3 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> F : ( Base ` R ) -1-1-onto-> B )
20 simpl2 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> S e. Rng )
21 2 3 rngcl 
 |-  ( ( S e. Rng /\ ( F ` .1. ) e. B /\ x e. B ) -> ( ( F ` .1. ) .x. x ) e. B )
22 20 12 13 21 syl3anc 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( ( F ` .1. ) .x. x ) e. B )
23 f1ocnvfv2 
 |-  ( ( F : ( Base ` R ) -1-1-onto-> B /\ ( ( F ` .1. ) .x. x ) e. B ) -> ( F ` ( `' F ` ( ( F ` .1. ) .x. x ) ) ) = ( ( F ` .1. ) .x. x ) )
24 19 22 23 syl2an2r 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F ` ( `' F ` ( ( F ` .1. ) .x. x ) ) ) = ( ( F ` .1. ) .x. x ) )
25 5 1 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
26 25 3ad2ant1 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> .1. e. ( Base ` R ) )
27 19 26 jca 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> ( F : ( Base ` R ) -1-1-onto-> B /\ .1. e. ( Base ` R ) ) )
28 27 adantr 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F : ( Base ` R ) -1-1-onto-> B /\ .1. e. ( Base ` R ) ) )
29 f1ocnvfv1 
 |-  ( ( F : ( Base ` R ) -1-1-onto-> B /\ .1. e. ( Base ` R ) ) -> ( `' F ` ( F ` .1. ) ) = .1. )
30 28 29 syl 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( `' F ` ( F ` .1. ) ) = .1. )
31 30 oveq1d 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( ( `' F ` ( F ` .1. ) ) ( .r ` R ) ( `' F ` x ) ) = ( .1. ( .r ` R ) ( `' F ` x ) ) )
32 simpl1 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> R e. Ring )
33 2 5 rngimf1o 
 |-  ( `' F e. ( S RngIso R ) -> `' F : B -1-1-onto-> ( Base ` R ) )
34 f1of 
 |-  ( `' F : B -1-1-onto-> ( Base ` R ) -> `' F : B --> ( Base ` R ) )
35 33 34 syl 
 |-  ( `' F e. ( S RngIso R ) -> `' F : B --> ( Base ` R ) )
36 4 35 syl 
 |-  ( F e. ( R RngIso S ) -> `' F : B --> ( Base ` R ) )
37 36 3ad2ant3 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> `' F : B --> ( Base ` R ) )
38 37 ffvelcdmda 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( `' F ` x ) e. ( Base ` R ) )
39 5 14 1 32 38 ringlidmd 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( .1. ( .r ` R ) ( `' F ` x ) ) = ( `' F ` x ) )
40 31 39 eqtrd 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( ( `' F ` ( F ` .1. ) ) ( .r ` R ) ( `' F ` x ) ) = ( `' F ` x ) )
41 40 fveq2d 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F ` ( ( `' F ` ( F ` .1. ) ) ( .r ` R ) ( `' F ` x ) ) ) = ( F ` ( `' F ` x ) ) )
42 f1ocnvfv2 
 |-  ( ( F : ( Base ` R ) -1-1-onto-> B /\ x e. B ) -> ( F ` ( `' F ` x ) ) = x )
43 19 42 sylan 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F ` ( `' F ` x ) ) = x )
44 41 43 eqtrd 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F ` ( ( `' F ` ( F ` .1. ) ) ( .r ` R ) ( `' F ` x ) ) ) = x )
45 17 24 44 3eqtr3d 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( ( F ` .1. ) .x. x ) = x )
46 4 3ad2ant3 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> `' F e. ( S RngIso R ) )
47 46 6 syl 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> `' F e. ( S RngHom R ) )
48 47 adantr 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> `' F e. ( S RngHom R ) )
49 2 3 14 rnghmmul 
 |-  ( ( `' F e. ( S RngHom R ) /\ x e. B /\ ( F ` .1. ) e. B ) -> ( `' F ` ( x .x. ( F ` .1. ) ) ) = ( ( `' F ` x ) ( .r ` R ) ( `' F ` ( F ` .1. ) ) ) )
50 48 13 12 49 syl3anc 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( `' F ` ( x .x. ( F ` .1. ) ) ) = ( ( `' F ` x ) ( .r ` R ) ( `' F ` ( F ` .1. ) ) ) )
51 30 oveq2d 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( ( `' F ` x ) ( .r ` R ) ( `' F ` ( F ` .1. ) ) ) = ( ( `' F ` x ) ( .r ` R ) .1. ) )
52 5 14 1 32 38 ringridmd 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( ( `' F ` x ) ( .r ` R ) .1. ) = ( `' F ` x ) )
53 50 51 52 3eqtrd 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( `' F ` ( x .x. ( F ` .1. ) ) ) = ( `' F ` x ) )
54 53 fveq2d 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F ` ( `' F ` ( x .x. ( F ` .1. ) ) ) ) = ( F ` ( `' F ` x ) ) )
55 2 3 rngcl 
 |-  ( ( S e. Rng /\ x e. B /\ ( F ` .1. ) e. B ) -> ( x .x. ( F ` .1. ) ) e. B )
56 20 13 12 55 syl3anc 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( x .x. ( F ` .1. ) ) e. B )
57 f1ocnvfv2 
 |-  ( ( F : ( Base ` R ) -1-1-onto-> B /\ ( x .x. ( F ` .1. ) ) e. B ) -> ( F ` ( `' F ` ( x .x. ( F ` .1. ) ) ) ) = ( x .x. ( F ` .1. ) ) )
58 19 56 57 syl2an2r 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( F ` ( `' F ` ( x .x. ( F ` .1. ) ) ) ) = ( x .x. ( F ` .1. ) ) )
59 54 58 43 3eqtr3d 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( x .x. ( F ` .1. ) ) = x )
60 45 59 jca 
 |-  ( ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) /\ x e. B ) -> ( ( ( F ` .1. ) .x. x ) = x /\ ( x .x. ( F ` .1. ) ) = x ) )
61 60 ralrimiva 
 |-  ( ( R e. Ring /\ S e. Rng /\ F e. ( R RngIso S ) ) -> A. x e. B ( ( ( F ` .1. ) .x. x ) = x /\ ( x .x. ( F ` .1. ) ) = x ) )