rhmunitinv

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

		Ref	Expression
	Assertion	rhmunitinv	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to F ({inv}_{r} (R) (A)) = {inv}_{r} (S) (F (A))$

Proof

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

Metamath Proof Explorer

Theorem rhmunitinv

Proof