Metamath Proof Explorer


Theorem elrhmunit

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

Ref Expression
Assertion elrhmunit F R RingHom S A Unit R F A Unit S

Proof

Step Hyp Ref Expression
1 simpl F R RingHom S A Unit R F R RingHom S
2 eqid Base R = Base R
3 eqid Unit R = Unit R
4 2 3 unitss Unit R Base R
5 simpr F R RingHom S A Unit R A Unit R
6 4 5 sselid F R RingHom S A Unit R A Base R
7 rhmrcl1 F R RingHom S R Ring
8 eqid 1 R = 1 R
9 2 8 ringidcl R Ring 1 R Base R
10 1 7 9 3syl F R RingHom S A Unit R 1 R Base R
11 eqid r R = r R
12 eqid opp r R = opp r R
13 eqid r opp r R = r opp r R
14 3 8 11 12 13 isunit A Unit R A r R 1 R A r opp r R 1 R
15 5 14 sylib F R RingHom S A Unit R A r R 1 R A r opp r R 1 R
16 15 simpld F R RingHom S A Unit R A r R 1 R
17 eqid r S = r S
18 2 11 17 rhmdvdsr F R RingHom S A Base R 1 R Base R A r R 1 R F A r S F 1 R
19 1 6 10 16 18 syl31anc F R RingHom S A Unit R F A r S F 1 R
20 eqid 1 S = 1 S
21 8 20 rhm1 F R RingHom S F 1 R = 1 S
22 21 breq2d F R RingHom S F A r S F 1 R F A r S 1 S
23 22 adantr F R RingHom S A Unit R F A r S F 1 R F A r S 1 S
24 19 23 mpbid F R RingHom S A Unit R F A r S 1 S
25 rhmopp F R RingHom S F opp r R RingHom opp r S
26 25 adantr F R RingHom S A Unit R F opp r R RingHom opp r S
27 15 simprd F R RingHom S A Unit R A r opp r R 1 R
28 12 2 opprbas Base R = Base opp r R
29 eqid r opp r S = r opp r S
30 28 13 29 rhmdvdsr F opp r R RingHom opp r S A Base R 1 R Base R A r opp r R 1 R F A r opp r S F 1 R
31 26 6 10 27 30 syl31anc F R RingHom S A Unit R F A r opp r S F 1 R
32 21 breq2d F R RingHom S F A r opp r S F 1 R F A r opp r S 1 S
33 32 adantr F R RingHom S A Unit R F A r opp r S F 1 R F A r opp r S 1 S
34 31 33 mpbid F R RingHom S A Unit R F A r opp r S 1 S
35 eqid Unit S = Unit S
36 eqid opp r S = opp r S
37 35 20 17 36 29 isunit F A Unit S F A r S 1 S F A r opp r S 1 S
38 24 34 37 sylanbrc F R RingHom S A Unit R F A Unit S