This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sselid ⊢ ( ( 𝐹 ∈ ( 𝑅 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 ‘ 𝑆 ) )