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