Metamath Proof Explorer

Theorem rhmunitinv

Description: Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017)

Ref Expression
Assertion rhmunitinv 
|- ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` ( ( invr ` R ) ` A ) ) = ( ( invr ` S ) ` ( F ` A ) ) )

Proof

Step Hyp Ref Expression
1 rhmrcl1 
 |-  ( F e. ( R RingHom S ) -> R e. Ring )
2 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
3 eqid 
 |-  ( invr ` R ) = ( invr ` R )
4 eqid 
 |-  ( .r ` R ) = ( .r ` R )
5 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
6 2 3 4 5 unitlinv 
 |-  ( ( R e. Ring /\ A e. ( Unit ` R ) ) -> ( ( ( invr ` R ) ` A ) ( .r ` R ) A ) = ( 1r ` R ) )
7 1 6 sylan 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( ( invr ` R ) ` A ) ( .r ` R ) A ) = ( 1r ` R ) )
8 7 fveq2d 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` ( ( ( invr ` R ) ` A ) ( .r ` R ) A ) ) = ( F ` ( 1r ` R ) ) )
9 simpl 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> F e. ( R RingHom S ) )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 10 2 unitss 
 |-  ( Unit ` R ) C_ ( Base ` R )
12 2 3 unitinvcl 
 |-  ( ( R e. Ring /\ A e. ( Unit ` R ) ) -> ( ( invr ` R ) ` A ) e. ( Unit ` R ) )
13 1 12 sylan 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( invr ` R ) ` A ) e. ( Unit ` R ) )
14 11 13 sseldi 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( invr ` R ) ` A ) e. ( Base ` R ) )
15 simpr 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> A e. ( Unit ` R ) )
16 11 15 sseldi 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> A e. ( Base ` R ) )
17 eqid 
 |-  ( .r ` S ) = ( .r ` S )
18 10 4 17 rhmmul 
 |-  ( ( F e. ( R RingHom S ) /\ ( ( invr ` R ) ` A ) e. ( Base ` R ) /\ A e. ( Base ` R ) ) -> ( F ` ( ( ( invr ` R ) ` A ) ( .r ` R ) A ) ) = ( ( F ` ( ( invr ` R ) ` A ) ) ( .r ` S ) ( F ` A ) ) )
19 9 14 16 18 syl3anc 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` ( ( ( invr ` R ) ` A ) ( .r ` R ) A ) ) = ( ( F ` ( ( invr ` R ) ` A ) ) ( .r ` S ) ( F ` A ) ) )
20 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
21 5 20 rhm1 
 |-  ( F e. ( R RingHom S ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
22 21 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
23 8 19 22 3eqtr3d 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( F ` ( ( invr ` R ) ` A ) ) ( .r ` S ) ( F ` A ) ) = ( 1r ` S ) )
24 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
25 24 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> S e. Ring )
26 elrhmunit 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` A ) e. ( Unit ` S ) )
27 eqid 
 |-  ( Unit ` S ) = ( Unit ` S )
28 eqid 
 |-  ( invr ` S ) = ( invr ` S )
29 27 28 17 20 unitlinv 
 |-  ( ( S e. Ring /\ ( F ` A ) e. ( Unit ` S ) ) -> ( ( ( invr ` S ) ` ( F ` A ) ) ( .r ` S ) ( F ` A ) ) = ( 1r ` S ) )
30 25 26 29 syl2anc 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( ( invr ` S ) ` ( F ` A ) ) ( .r ` S ) ( F ` A ) ) = ( 1r ` S ) )
31 23 30 eqtr4d 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( F ` ( ( invr ` R ) ` A ) ) ( .r ` S ) ( F ` A ) ) = ( ( ( invr ` S ) ` ( F ` A ) ) ( .r ` S ) ( F ` A ) ) )
32 eqid 
 |-  ( ( mulGrp ` S ) |`s ( Unit ` S ) ) = ( ( mulGrp ` S ) |`s ( Unit ` S ) )
33 27 32 unitgrp 
 |-  ( S e. Ring -> ( ( mulGrp ` S ) |`s ( Unit ` S ) ) e. Grp )
34 24 33 syl 
 |-  ( F e. ( R RingHom S ) -> ( ( mulGrp ` S ) |`s ( Unit ` S ) ) e. Grp )
35 34 adantr 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( mulGrp ` S ) |`s ( Unit ` S ) ) e. Grp )
36 elrhmunit 
 |-  ( ( F e. ( R RingHom S ) /\ ( ( invr ` R ) ` A ) e. ( Unit ` R ) ) -> ( F ` ( ( invr ` R ) ` A ) ) e. ( Unit ` S ) )
37 13 36 syldan 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` ( ( invr ` R ) ` A ) ) e. ( Unit ` S ) )
38 27 28 unitinvcl 
 |-  ( ( S e. Ring /\ ( F ` A ) e. ( Unit ` S ) ) -> ( ( invr ` S ) ` ( F ` A ) ) e. ( Unit ` S ) )
39 25 26 38 syl2anc 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( invr ` S ) ` ( F ` A ) ) e. ( Unit ` S ) )
40 27 32 unitgrpbas 
 |-  ( Unit ` S ) = ( Base ` ( ( mulGrp ` S ) |`s ( Unit ` S ) ) )
41 fvex 
 |-  ( Unit ` S ) e. _V
42 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
43 42 17 mgpplusg 
 |-  ( .r ` S ) = ( +g ` ( mulGrp ` S ) )
44 32 43 ressplusg 
 |-  ( ( Unit ` S ) e. _V -> ( .r ` S ) = ( +g ` ( ( mulGrp ` S ) |`s ( Unit ` S ) ) ) )
45 41 44 ax-mp 
 |-  ( .r ` S ) = ( +g ` ( ( mulGrp ` S ) |`s ( Unit ` S ) ) )
46 40 45 grprcan 
 |-  ( ( ( ( mulGrp ` S ) |`s ( Unit ` S ) ) e. Grp /\ ( ( F ` ( ( invr ` R ) ` A ) ) e. ( Unit ` S ) /\ ( ( invr ` S ) ` ( F ` A ) ) e. ( Unit ` S ) /\ ( F ` A ) e. ( Unit ` S ) ) ) -> ( ( ( F ` ( ( invr ` R ) ` A ) ) ( .r ` S ) ( F ` A ) ) = ( ( ( invr ` S ) ` ( F ` A ) ) ( .r ` S ) ( F ` A ) ) <-> ( F ` ( ( invr ` R ) ` A ) ) = ( ( invr ` S ) ` ( F ` A ) ) ) )
47 35 37 39 26 46 syl13anc 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( ( F ` ( ( invr ` R ) ` A ) ) ( .r ` S ) ( F ` A ) ) = ( ( ( invr ` S ) ` ( F ` A ) ) ( .r ` S ) ( F ` A ) ) <-> ( F ` ( ( invr ` R ) ` A ) ) = ( ( invr ` S ) ` ( F ` A ) ) ) )
48 31 47 mpbid 
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` ( ( invr ` R ) ` A ) ) = ( ( invr ` S ) ` ( F ` A ) ) )