ringlghm

Description: Left-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	ringlghm	$⊢ (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	fmpttd	$⊢ (R \in Ring \land X \in B) \to (x \in B ⟼ X \underset{˙}{\cdot} x) : B ⟶ B$
9		3anass	$⊢ (X \in B \land y \in B \land z \in B) \leftrightarrow (X \in B \land (y \in B \land z \in B))$
10	1 3 2	ringdi	$⊢ (R \in Ring \land (X \in B \land y \in B \land z \in B)) \to X \underset{˙}{\cdot} (y +_{R} z) = (X \underset{˙}{\cdot} y) +_{R} (X \underset{˙}{\cdot} z)$
11	9 10	sylan2br	$⊢ (R \in Ring \land (X \in B \land (y \in B \land z \in B))) \to X \underset{˙}{\cdot} (y +_{R} z) = (X \underset{˙}{\cdot} y) +_{R} (X \underset{˙}{\cdot} z)$
12	11	anassrs	$⊢ ((R \in Ring \land X \in B) \land (y \in B \land z \in B)) \to X \underset{˙}{\cdot} (y +_{R} z) = (X \underset{˙}{\cdot} y) +_{R} (X \underset{˙}{\cdot} z)$
13	1 3	ringacl	$⊢ (R \in Ring \land y \in B \land z \in B) \to y +_{R} z \in B$
14	13	3expb	$⊢ (R \in Ring \land (y \in B \land z \in B)) \to y +_{R} z \in B$
15	14	adantlr	$⊢ ((R \in Ring \land X \in B) \land (y \in B \land z \in B)) \to y +_{R} z \in B$
16		oveq2	$⊢ x = y +_{R} z \to X \underset{˙}{\cdot} x = X \underset{˙}{\cdot} (y +_{R} z)$
17		eqid	$⊢ (x \in B ⟼ X \underset{˙}{\cdot} x) = (x \in B ⟼ X \underset{˙}{\cdot} x)$
18		ovex	$⊢ X \underset{˙}{\cdot} (y +_{R} z) \in V$
19	16 17 18	fvmpt	$⊢ y +_{R} z \in B \to (x \in B ⟼ X \underset{˙}{\cdot} x) (y +_{R} z) = X \underset{˙}{\cdot} (y +_{R} z)$
20	15 19	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) = X \underset{˙}{\cdot} (y +_{R} z)$
21		oveq2	$⊢ x = y \to X \underset{˙}{\cdot} x = X \underset{˙}{\cdot} y$
22		ovex	$⊢ X \underset{˙}{\cdot} y \in V$
23	21 17 22	fvmpt	$⊢ y \in B \to (x \in B ⟼ X \underset{˙}{\cdot} x) (y) = X \underset{˙}{\cdot} y$
24		oveq2	$⊢ x = z \to X \underset{˙}{\cdot} x = X \underset{˙}{\cdot} z$
25		ovex	$⊢ X \underset{˙}{\cdot} z \in V$
26	24 17 25	fvmpt	$⊢ z \in B \to (x \in B ⟼ X \underset{˙}{\cdot} x) (z) = X \underset{˙}{\cdot} z$
27	23 26	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) = (X \underset{˙}{\cdot} y) +_{R} (X \underset{˙}{\cdot} z)$
28	27	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) = (X \underset{˙}{\cdot} y) +_{R} (X \underset{˙}{\cdot} z)$
29	12 20 28	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)$
30	1 1 3 3 5 5 8 29	isghmd	$⊢ (R \in Ring \land X \in B) \to (x \in B ⟼ X \underset{˙}{\cdot} x) \in (R GrpHom R)$

Metamath Proof Explorer

Theorem ringlghm

Proof