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 ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) = ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 rhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
2 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
3 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
4 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6 2 3 4 5 unitlinv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) = ( 1r ‘ 𝑅 ) )
7 1 6 sylan ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) = ( 1r ‘ 𝑅 ) )
8 7 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) ) = ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) )
9 simpl ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 10 2 unitss ⊢ ( Unit ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 )
12 2 3 unitinvcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Unit ‘ 𝑅 ) )
13 1 12 sylan ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Unit ‘ 𝑅 ) )
14 11 13 sselid ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝑅 ) )
15 simpr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐴 ∈ ( Unit ‘ 𝑅 ) )
16 11 15 sselid ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
17 eqid ⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
18 10 4 17 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝐴 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) ) = ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) )
19 9 14 16 18 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ( .r ‘ 𝑅 ) 𝐴 ) ) = ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) )
20 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
21 5 20 rhm1 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
22 21 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
23 8 19 22 3eqtr3d ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) = ( 1r ‘ 𝑆 ) )
24 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
25 24 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → 𝑆 ∈ Ring )
26 elrhmunit ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Unit ‘ 𝑆 ) )
27 eqid ⊢ ( Unit ‘ 𝑆 ) = ( Unit ‘ 𝑆 )
28 eqid ⊢ ( invr ‘ 𝑆 ) = ( invr ‘ 𝑆 )
29 27 28 17 20 unitlinv ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Unit ‘ 𝑆 ) ) → ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) = ( 1r ‘ 𝑆 ) )
30 25 26 29 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) = ( 1r ‘ 𝑆 ) )
31 23 30 eqtr4d ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) = ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) )
32 eqid ⊢ ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) ) = ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) )
33 27 32 unitgrp ⊢ ( 𝑆 ∈ Ring → ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) ) ∈ Grp )
34 24 33 syl ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) ) ∈ Grp )
35 34 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) ) ∈ Grp )
36 elrhmunit ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ∈ ( Unit ‘ 𝑆 ) )
37 13 36 syldan ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ∈ ( Unit ‘ 𝑆 ) )
38 27 28 unitinvcl ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Unit ‘ 𝑆 ) ) → ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ( Unit ‘ 𝑆 ) )
39 25 26 38 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ( Unit ‘ 𝑆 ) )
40 27 32 unitgrpbas ⊢ ( Unit ‘ 𝑆 ) = ( Base ‘ ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) ) )
41 fvex ⊢ ( Unit ‘ 𝑆 ) ∈ V
42 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
43 42 17 mgpplusg ⊢ ( .r ‘ 𝑆 ) = ( +g ‘ ( mulGrp ‘ 𝑆 ) )
44 32 43 ressplusg ⊢ ( ( Unit ‘ 𝑆 ) ∈ V → ( .r ‘ 𝑆 ) = ( +g ‘ ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) ) ) )
45 41 44 ax-mp ⊢ ( .r ‘ 𝑆 ) = ( +g ‘ ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) ) )
46 40 45 grprcan ⊢ ( ( ( ( mulGrp ‘ 𝑆 ) ↾s ( Unit ‘ 𝑆 ) ) ∈ Grp ∧ ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ∈ ( Unit ‘ 𝑆 ) ∧ ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ∈ ( Unit ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Unit ‘ 𝑆 ) ) ) → ( ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) = ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) ↔ ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) = ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
47 35 37 39 26 46 syl13anc ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( ( ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) = ( ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ( .r ‘ 𝑆 ) ( 𝐹 ‘ 𝐴 ) ) ↔ ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) = ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) ) )
48 31 47 mpbid ⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ ( Unit ‘ 𝑅 ) ) → ( 𝐹 ‘ ( ( invr ‘ 𝑅 ) ‘ 𝐴 ) ) = ( ( invr ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝐴 ) ) )