Metamath Proof Explorer


Theorem elrhmunit

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

Ref Expression
Assertion elrhmunit ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹𝐴 ) ∈ ( Unit ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
2 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 eqid ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
4 2 3 unitss ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 )
5 simpr ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐴 ∈ ( Unit ‘ 𝑅 ) )
6 4 5 sseldi ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
7 rhmrcl1 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
8 eqid ( 1r𝑅 ) = ( 1r𝑅 )
9 2 8 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
10 1 7 9 3syl ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
11 eqid ( ∥r𝑅 ) = ( ∥r𝑅 )
12 eqid ( oppr𝑅 ) = ( oppr𝑅 )
13 eqid ( ∥r ‘ ( oppr𝑅 ) ) = ( ∥r ‘ ( oppr𝑅 ) )
14 3 8 11 12 13 isunit ( 𝐴 ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝐴 ( ∥r𝑅 ) ( 1r𝑅 ) ∧ 𝐴 ( ∥r ‘ ( oppr𝑅 ) ) ( 1r𝑅 ) ) )
15 5 14 sylib ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐴 ( ∥r𝑅 ) ( 1r𝑅 ) ∧ 𝐴 ( ∥r ‘ ( oppr𝑅 ) ) ( 1r𝑅 ) ) )
16 15 simpld ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐴 ( ∥r𝑅 ) ( 1r𝑅 ) )
17 eqid ( ∥r𝑆 ) = ( ∥r𝑆 )
18 2 11 17 rhmdvdsr ( ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ 𝐴 ( ∥r𝑅 ) ( 1r𝑅 ) ) → ( 𝐹𝐴 ) ( ∥r𝑆 ) ( 𝐹 ‘ ( 1r𝑅 ) ) )
19 1 6 10 16 18 syl31anc ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹𝐴 ) ( ∥r𝑆 ) ( 𝐹 ‘ ( 1r𝑅 ) ) )
20 eqid ( 1r𝑆 ) = ( 1r𝑆 )
21 8 20 rhm1 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 1r𝑅 ) ) = ( 1r𝑆 ) )
22 21 breq2d ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝐹𝐴 ) ( ∥r𝑆 ) ( 𝐹 ‘ ( 1r𝑅 ) ) ↔ ( 𝐹𝐴 ) ( ∥r𝑆 ) ( 1r𝑆 ) ) )
23 22 adantr ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐹𝐴 ) ( ∥r𝑆 ) ( 𝐹 ‘ ( 1r𝑅 ) ) ↔ ( 𝐹𝐴 ) ( ∥r𝑆 ) ( 1r𝑆 ) ) )
24 19 23 mpbid ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹𝐴 ) ( ∥r𝑆 ) ( 1r𝑆 ) )
25 rhmopp ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( ( oppr𝑅 ) RingHom ( oppr𝑆 ) ) )
26 25 adantr ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐹 ∈ ( ( oppr𝑅 ) RingHom ( oppr𝑆 ) ) )
27 15 simprd ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐴 ( ∥r ‘ ( oppr𝑅 ) ) ( 1r𝑅 ) )
28 12 2 opprbas ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr𝑅 ) )
29 eqid ( ∥r ‘ ( oppr𝑆 ) ) = ( ∥r ‘ ( oppr𝑆 ) )
30 28 13 29 rhmdvdsr ( ( ( 𝐹 ∈ ( ( oppr𝑅 ) RingHom ( oppr𝑆 ) ) ∧ 𝐴 ∈ ( Base ‘ 𝑅 ) ∧ ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) ) ∧ 𝐴 ( ∥r ‘ ( oppr𝑅 ) ) ( 1r𝑅 ) ) → ( 𝐹𝐴 ) ( ∥r ‘ ( oppr𝑆 ) ) ( 𝐹 ‘ ( 1r𝑅 ) ) )
31 26 6 10 27 30 syl31anc ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹𝐴 ) ( ∥r ‘ ( oppr𝑆 ) ) ( 𝐹 ‘ ( 1r𝑅 ) ) )
32 21 breq2d ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( 𝐹𝐴 ) ( ∥r ‘ ( oppr𝑆 ) ) ( 𝐹 ‘ ( 1r𝑅 ) ) ↔ ( 𝐹𝐴 ) ( ∥r ‘ ( oppr𝑆 ) ) ( 1r𝑆 ) ) )
33 32 adantr ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐹𝐴 ) ( ∥r ‘ ( oppr𝑆 ) ) ( 𝐹 ‘ ( 1r𝑅 ) ) ↔ ( 𝐹𝐴 ) ( ∥r ‘ ( oppr𝑆 ) ) ( 1r𝑆 ) ) )
34 31 33 mpbid ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹𝐴 ) ( ∥r ‘ ( oppr𝑆 ) ) ( 1r𝑆 ) )
35 eqid ( Unit ‘ 𝑆 ) = ( Unit ‘ 𝑆 )
36 eqid ( oppr𝑆 ) = ( oppr𝑆 )
37 35 20 17 36 29 isunit ( ( 𝐹𝐴 ) ∈ ( Unit ‘ 𝑆 ) ↔ ( ( 𝐹𝐴 ) ( ∥r𝑆 ) ( 1r𝑆 ) ∧ ( 𝐹𝐴 ) ( ∥r ‘ ( oppr𝑆 ) ) ( 1r𝑆 ) ) )
38 24 34 37 sylanbrc ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹𝐴 ) ∈ ( Unit ‘ 𝑆 ) )