Metamath Proof Explorer


Theorem elrhmunit

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

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

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> F e. ( R RingHom S ) )
2 eqid
 |-  ( Base ` R ) = ( Base ` R )
3 eqid
 |-  ( Unit ` R ) = ( Unit ` R )
4 2 3 unitss
 |-  ( Unit ` R ) C_ ( Base ` R )
5 simpr
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> A e. ( Unit ` R ) )
6 4 5 sselid
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> A e. ( Base ` R ) )
7 rhmrcl1
 |-  ( F e. ( R RingHom S ) -> R e. Ring )
8 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
9 2 8 ringidcl
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
10 1 7 9 3syl
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) )
11 eqid
 |-  ( ||r ` R ) = ( ||r ` R )
12 eqid
 |-  ( oppR ` R ) = ( oppR ` R )
13 eqid
 |-  ( ||r ` ( oppR ` R ) ) = ( ||r ` ( oppR ` R ) )
14 3 8 11 12 13 isunit
 |-  ( A e. ( Unit ` R ) <-> ( A ( ||r ` R ) ( 1r ` R ) /\ A ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
15 5 14 sylib
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( A ( ||r ` R ) ( 1r ` R ) /\ A ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) )
16 15 simpld
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> A ( ||r ` R ) ( 1r ` R ) )
17 eqid
 |-  ( ||r ` S ) = ( ||r ` S )
18 2 11 17 rhmdvdsr
 |-  ( ( ( F e. ( R RingHom S ) /\ A e. ( Base ` R ) /\ ( 1r ` R ) e. ( Base ` R ) ) /\ A ( ||r ` R ) ( 1r ` R ) ) -> ( F ` A ) ( ||r ` S ) ( F ` ( 1r ` R ) ) )
19 1 6 10 16 18 syl31anc
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` A ) ( ||r ` S ) ( F ` ( 1r ` R ) ) )
20 eqid
 |-  ( 1r ` S ) = ( 1r ` S )
21 8 20 rhm1
 |-  ( F e. ( R RingHom S ) -> ( F ` ( 1r ` R ) ) = ( 1r ` S ) )
22 21 breq2d
 |-  ( F e. ( R RingHom S ) -> ( ( F ` A ) ( ||r ` S ) ( F ` ( 1r ` R ) ) <-> ( F ` A ) ( ||r ` S ) ( 1r ` S ) ) )
23 22 adantr
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( F ` A ) ( ||r ` S ) ( F ` ( 1r ` R ) ) <-> ( F ` A ) ( ||r ` S ) ( 1r ` S ) ) )
24 19 23 mpbid
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` A ) ( ||r ` S ) ( 1r ` S ) )
25 rhmopp
 |-  ( F e. ( R RingHom S ) -> F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) )
26 25 adantr
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) )
27 15 simprd
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> A ( ||r ` ( oppR ` R ) ) ( 1r ` R ) )
28 12 2 opprbas
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
29 eqid
 |-  ( ||r ` ( oppR ` S ) ) = ( ||r ` ( oppR ` S ) )
30 28 13 29 rhmdvdsr
 |-  ( ( ( F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) /\ A e. ( Base ` R ) /\ ( 1r ` R ) e. ( Base ` R ) ) /\ A ( ||r ` ( oppR ` R ) ) ( 1r ` R ) ) -> ( F ` A ) ( ||r ` ( oppR ` S ) ) ( F ` ( 1r ` R ) ) )
31 26 6 10 27 30 syl31anc
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` A ) ( ||r ` ( oppR ` S ) ) ( F ` ( 1r ` R ) ) )
32 21 breq2d
 |-  ( F e. ( R RingHom S ) -> ( ( F ` A ) ( ||r ` ( oppR ` S ) ) ( F ` ( 1r ` R ) ) <-> ( F ` A ) ( ||r ` ( oppR ` S ) ) ( 1r ` S ) ) )
33 32 adantr
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( ( F ` A ) ( ||r ` ( oppR ` S ) ) ( F ` ( 1r ` R ) ) <-> ( F ` A ) ( ||r ` ( oppR ` S ) ) ( 1r ` S ) ) )
34 31 33 mpbid
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` A ) ( ||r ` ( oppR ` S ) ) ( 1r ` S ) )
35 eqid
 |-  ( Unit ` S ) = ( Unit ` S )
36 eqid
 |-  ( oppR ` S ) = ( oppR ` S )
37 35 20 17 36 29 isunit
 |-  ( ( F ` A ) e. ( Unit ` S ) <-> ( ( F ` A ) ( ||r ` S ) ( 1r ` S ) /\ ( F ` A ) ( ||r ` ( oppR ` S ) ) ( 1r ` S ) ) )
38 24 34 37 sylanbrc
 |-  ( ( F e. ( R RingHom S ) /\ A e. ( Unit ` R ) ) -> ( F ` A ) e. ( Unit ` S ) )