ringrghm

Description: Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015)

	Ref	Expression
Hypotheses	ringlghm.b	$⊢ B = {Base}_{R}$
	ringlghm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	ringrghm	$⊢ (R \in Ring \land X \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) \in (R GrpHom R)$

Proof

Step	Hyp	Ref	Expression
1		ringlghm.b	$⊢ B = {Base}_{R}$
2		ringlghm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		eqid	$⊢ +_{R} = +_{R}$
4		ringgrp	$⊢ R \in Ring \to R \in Grp$
5	4	adantr	$⊢ (R \in Ring \land X \in B) \to R \in Grp$
6	1 2	ringcl	$⊢ (R \in Ring \land x \in B \land X \in B) \to x \underset{˙}{\cdot} X \in B$
7	6	3expa	$⊢ ((R \in Ring \land x \in B) \land X \in B) \to x \underset{˙}{\cdot} X \in B$
8	7	an32s	$⊢ ((R \in Ring \land X \in B) \land x \in B) \to x \underset{˙}{\cdot} X \in B$
9	8	fmpttd	$⊢ (R \in Ring \land X \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) : B ⟶ B$
10		df-3an	$⊢ (y \in B \land z \in B \land X \in B) \leftrightarrow ((y \in B \land z \in B) \land X \in B)$
11	1 3 2	ringdir	$⊢ (R \in Ring \land (y \in B \land z \in B \land X \in B)) \to (y +_{R} z) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{R} (z \underset{˙}{\cdot} X)$
12	10 11	sylan2br	$⊢ (R \in Ring \land ((y \in B \land z \in B) \land X \in B)) \to (y +_{R} z) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{R} (z \underset{˙}{\cdot} X)$
13	12	anass1rs	$⊢ ((R \in Ring \land X \in B) \land (y \in B \land z \in B)) \to (y +_{R} z) \underset{˙}{\cdot} X = (y \underset{˙}{\cdot} X) +_{R} (z \underset{˙}{\cdot} X)$
14	1 3	ringacl	$⊢ (R \in Ring \land y \in B \land z \in B) \to y +_{R} z \in B$
15	14	3expb	$⊢ (R \in Ring \land (y \in B \land z \in B)) \to y +_{R} z \in B$
16	15	adantlr	$⊢ ((R \in Ring \land X \in B) \land (y \in B \land z \in B)) \to y +_{R} z \in B$
17		oveq1	$⊢ x = y +_{R} z \to x \underset{˙}{\cdot} X = (y +_{R} z) \underset{˙}{\cdot} X$
18		eqid	$⊢ (x \in B ⟼ x \underset{˙}{\cdot} X) = (x \in B ⟼ x \underset{˙}{\cdot} X)$
19		ovex	$⊢ (y +_{R} z) \underset{˙}{\cdot} X \in V$
20	17 18 19	fvmpt	$⊢ y +_{R} z \in B \to (x \in B ⟼ x \underset{˙}{\cdot} X) (y +_{R} z) = (y +_{R} z) \underset{˙}{\cdot} X$
21	16 20	syl	$⊢ ((R \in Ring \land X \in B) \land (y \in B \land z \in B)) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (y +_{R} z) = (y +_{R} z) \underset{˙}{\cdot} X$
22		oveq1	$⊢ x = y \to x \underset{˙}{\cdot} X = y \underset{˙}{\cdot} X$
23		ovex	$⊢ y \underset{˙}{\cdot} X \in V$
24	22 18 23	fvmpt	$⊢ y \in B \to (x \in B ⟼ x \underset{˙}{\cdot} X) (y) = y \underset{˙}{\cdot} X$
25		oveq1	$⊢ x = z \to x \underset{˙}{\cdot} X = z \underset{˙}{\cdot} X$
26		ovex	$⊢ z \underset{˙}{\cdot} X \in V$
27	25 18 26	fvmpt	$⊢ z \in B \to (x \in B ⟼ x \underset{˙}{\cdot} X) (z) = z \underset{˙}{\cdot} X$
28	24 27	oveqan12d	$⊢ (y \in B \land z \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (y) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (z) = (y \underset{˙}{\cdot} X) +_{R} (z \underset{˙}{\cdot} X)$
29	28	adantl	$⊢ ((R \in Ring \land X \in B) \land (y \in B \land z \in B)) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (y) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (z) = (y \underset{˙}{\cdot} X) +_{R} (z \underset{˙}{\cdot} X)$
30	13 21 29	3eqtr4d	$⊢ ((R \in Ring \land X \in B) \land (y \in B \land z \in B)) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (y +_{R} z) = (x \in B ⟼ x \underset{˙}{\cdot} X) (y) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (z)$
31	1 1 3 3 5 5 9 30	isghmd	$⊢ (R \in Ring \land X \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) \in (R GrpHom R)$

Metamath Proof Explorer

Theorem ringrghm

Proof