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𝑆 ) ‘ ( 𝐹𝐴 ) ) )