elrhmunit

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

		Ref	Expression
	Assertion	elrhmunit	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to F (A) \in Unit (S)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to F \in (R RingHom S)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ Unit (R) = Unit (R)$
4	2 3	unitss	$⊢ Unit (R) \subseteq {Base}_{R}$
5		simpr	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to A \in Unit (R)$
6	4 5	sselid	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to A \in {Base}_{R}$
7		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
8		eqid	$⊢ 1_{R} = 1_{R}$
9	2 8	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
10	1 7 9	3syl	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to 1_{R} \in {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 \in Unit (R) \leftrightarrow (A ∥_{r} (R) 1_{R} \land A ∥_{r} ({opp}_{r} (R)) 1_{R})$
15	14	bilani	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to (A ∥_{r} (R) 1_{R} \land A ∥_{r} ({opp}_{r} (R)) 1_{R})$
16	15	simpld	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to A ∥_{r} (R) 1_{R}$
17		eqid	$⊢ ∥_{r} (S) = ∥_{r} (S)$
18	2 11 17	rhmdvdsr	$⊢ ((F \in (R RingHom S) \land A \in {Base}_{R} \land 1_{R} \in {Base}_{R}) \land A ∥_{r} (R) 1_{R}) \to F (A) ∥_{r} (S) F (1_{R})$
19	1 6 10 16 18	syl31anc	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to F (A) ∥_{r} (S) F (1_{R})$
20		eqid	$⊢ 1_{S} = 1_{S}$
21	8 20	rhm1	$⊢ F \in (R RingHom S) \to F (1_{R}) = 1_{S}$
22	21	breq2d	$⊢ F \in (R RingHom S) \to (F (A) ∥_{r} (S) F (1_{R}) \leftrightarrow F (A) ∥_{r} (S) 1_{S})$
23	22	adantr	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to (F (A) ∥_{r} (S) F (1_{R}) \leftrightarrow F (A) ∥_{r} (S) 1_{S})$
24	19 23	mpbid	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to F (A) ∥_{r} (S) 1_{S}$
25		rhmopp	$⊢ F \in (R RingHom S) \to F \in ({opp}_{r} (R) RingHom {opp}_{r} (S))$
26	25	adantr	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to F \in ({opp}_{r} (R) RingHom {opp}_{r} (S))$
27	15	simprd	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to 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 \in ({opp}_{r} (R) RingHom {opp}_{r} (S)) \land A \in {Base}_{R} \land 1_{R} \in {Base}_{R}) \land A ∥_{r} ({opp}_{r} (R)) 1_{R}) \to F (A) ∥_{r} ({opp}_{r} (S)) F (1_{R})$
31	26 6 10 27 30	syl31anc	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to F (A) ∥_{r} ({opp}_{r} (S)) F (1_{R})$
32	21	breq2d	$⊢ F \in (R RingHom S) \to (F (A) ∥_{r} ({opp}_{r} (S)) F (1_{R}) \leftrightarrow F (A) ∥_{r} ({opp}_{r} (S)) 1_{S})$
33	32	adantr	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to (F (A) ∥_{r} ({opp}_{r} (S)) F (1_{R}) \leftrightarrow F (A) ∥_{r} ({opp}_{r} (S)) 1_{S})$
34	31 33	mpbid	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to 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) \in Unit (S) \leftrightarrow (F (A) ∥_{r} (S) 1_{S} \land F (A) ∥_{r} ({opp}_{r} (S)) 1_{S})$
38	24 34 37	sylanbrc	$⊢ (F \in (R RingHom S) \land A \in Unit (R)) \to F (A) \in Unit (S)$

Metamath Proof Explorer

Theorem elrhmunit

Proof