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 F R RingHom S A Unit R F inv r R A = inv r S F A

Proof

Step Hyp Ref Expression
1 rhmrcl1 F R RingHom S R Ring
2 eqid Unit R = Unit R
3 eqid inv r R = inv r R
4 eqid R = R
5 eqid 1 R = 1 R
6 2 3 4 5 unitlinv R Ring A Unit R inv r R A R A = 1 R
7 1 6 sylan F R RingHom S A Unit R inv r R A R A = 1 R
8 7 fveq2d F R RingHom S A Unit R F inv r R A R A = F 1 R
9 simpl F R RingHom S A Unit R F R RingHom S
10 eqid Base R = Base R
11 10 2 unitss Unit R Base R
12 2 3 unitinvcl R Ring A Unit R inv r R A Unit R
13 1 12 sylan F R RingHom S A Unit R inv r R A Unit R
14 11 13 sselid F R RingHom S A Unit R inv r R A Base R
15 simpr F R RingHom S A Unit R A Unit R
16 11 15 sselid F R RingHom S A Unit R A Base R
17 eqid S = S
18 10 4 17 rhmmul F R RingHom S inv r R A Base R A Base R F inv r R A R A = F inv r R A S F A
19 9 14 16 18 syl3anc F R RingHom S A Unit R F inv r R A R A = F inv r R A S F A
20 eqid 1 S = 1 S
21 5 20 rhm1 F R RingHom S F 1 R = 1 S
22 21 adantr F R RingHom S A Unit R F 1 R = 1 S
23 8 19 22 3eqtr3d F R RingHom S A Unit R F inv r R A S F A = 1 S
24 rhmrcl2 F R RingHom S S Ring
25 24 adantr F R RingHom S A Unit R S Ring
26 elrhmunit F R RingHom S A Unit R F A Unit S
27 eqid Unit S = Unit S
28 eqid inv r S = inv r S
29 27 28 17 20 unitlinv S Ring F A Unit S inv r S F A S F A = 1 S
30 25 26 29 syl2anc F R RingHom S A Unit R inv r S F A S F A = 1 S
31 23 30 eqtr4d F R RingHom S A Unit R F inv r R A S F A = inv r S F A S F A
32 eqid mulGrp S 𝑠 Unit S = mulGrp S 𝑠 Unit S
33 27 32 unitgrp S Ring mulGrp S 𝑠 Unit S Grp
34 24 33 syl F R RingHom S mulGrp S 𝑠 Unit S Grp
35 34 adantr F R RingHom S A Unit R mulGrp S 𝑠 Unit S Grp
36 elrhmunit F R RingHom S inv r R A Unit R F inv r R A Unit S
37 13 36 syldan F R RingHom S A Unit R F inv r R A Unit S
38 27 28 unitinvcl S Ring F A Unit S inv r S F A Unit S
39 25 26 38 syl2anc F R RingHom S A Unit R inv r S F A Unit S
40 27 32 unitgrpbas Unit S = Base mulGrp S 𝑠 Unit S
41 fvex Unit S V
42 eqid mulGrp S = mulGrp S
43 42 17 mgpplusg S = + mulGrp S
44 32 43 ressplusg Unit S V S = + mulGrp S 𝑠 Unit S
45 41 44 ax-mp S = + mulGrp S 𝑠 Unit S
46 40 45 grprcan mulGrp S 𝑠 Unit S Grp F inv r R A Unit S inv r S F A Unit S F A Unit S F inv r R A S F A = inv r S F A S F A F inv r R A = inv r S F A
47 35 37 39 26 46 syl13anc F R RingHom S A Unit R F inv r R A S F A = inv r S F A S F A F inv r R A = inv r S F A
48 31 47 mpbid F R RingHom S A Unit R F inv r R A = inv r S F A