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 sselid
 |-  ( ( 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 sselid
 |-  ( ( 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 ) ) )