srgrmhm

Description: Right-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringrghm . (Contributed by AV, 23-Aug-2019)

	Ref	Expression
Hypotheses	srglmhm.b	$⊢ B = {Base}_{R}$
	srglmhm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	srgrmhm	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) \in (R MndHom R)$

Proof

Step	Hyp	Ref	Expression
1		srglmhm.b	$⊢ B = {Base}_{R}$
2		srglmhm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		srgmnd	$⊢ R \in SRing \to R \in Mnd$
4	3 3	jca	$⊢ R \in SRing \to (R \in Mnd \land R \in Mnd)$
5	4	adantr	$⊢ (R \in SRing \land X \in B) \to (R \in Mnd \land R \in Mnd)$
6	1 2	srgcl	$⊢ (R \in SRing \land x \in B \land X \in B) \to x \underset{˙}{\cdot} X \in B$
7	6	3com23	$⊢ (R \in SRing \land X \in B \land x \in B) \to x \underset{˙}{\cdot} X \in B$
8	7	3expa	$⊢ ((R \in SRing \land X \in B) \land x \in B) \to x \underset{˙}{\cdot} X \in B$
9	8	fmpttd	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) : B ⟶ B$
10		3anrot	$⊢ (X \in B \land a \in B \land b \in B) \leftrightarrow (a \in B \land b \in B \land X \in B)$
11		3anass	$⊢ (X \in B \land a \in B \land b \in B) \leftrightarrow (X \in B \land (a \in B \land b \in B))$
12	10 11	bitr3i	$⊢ (a \in B \land b \in B \land X \in B) \leftrightarrow (X \in B \land (a \in B \land b \in B))$
13		eqid	$⊢ +_{R} = +_{R}$
14	1 13 2	srgdir	$⊢ (R \in SRing \land (a \in B \land b \in B \land X \in B)) \to (a +_{R} b) \underset{˙}{\cdot} X = (a \underset{˙}{\cdot} X) +_{R} (b \underset{˙}{\cdot} X)$
15	12 14	sylan2br	$⊢ (R \in SRing \land (X \in B \land (a \in B \land b \in B))) \to (a +_{R} b) \underset{˙}{\cdot} X = (a \underset{˙}{\cdot} X) +_{R} (b \underset{˙}{\cdot} X)$
16	15	anassrs	$⊢ ((R \in SRing \land X \in B) \land (a \in B \land b \in B)) \to (a +_{R} b) \underset{˙}{\cdot} X = (a \underset{˙}{\cdot} X) +_{R} (b \underset{˙}{\cdot} X)$
17	1 13	srgacl	$⊢ (R \in SRing \land a \in B \land b \in B) \to a +_{R} b \in B$
18	17	3expb	$⊢ (R \in SRing \land (a \in B \land b \in B)) \to a +_{R} b \in B$
19	18	adantlr	$⊢ ((R \in SRing \land X \in B) \land (a \in B \land b \in B)) \to a +_{R} b \in B$
20		oveq1	$⊢ x = a +_{R} b \to x \underset{˙}{\cdot} X = (a +_{R} b) \underset{˙}{\cdot} X$
21		eqid	$⊢ (x \in B ⟼ x \underset{˙}{\cdot} X) = (x \in B ⟼ x \underset{˙}{\cdot} X)$
22		ovex	$⊢ (a +_{R} b) \underset{˙}{\cdot} X \in V$
23	20 21 22	fvmpt	$⊢ a +_{R} b \in B \to (x \in B ⟼ x \underset{˙}{\cdot} X) (a +_{R} b) = (a +_{R} b) \underset{˙}{\cdot} X$
24	19 23	syl	$⊢ ((R \in SRing \land X \in B) \land (a \in B \land b \in B)) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (a +_{R} b) = (a +_{R} b) \underset{˙}{\cdot} X$
25		oveq1	$⊢ x = a \to x \underset{˙}{\cdot} X = a \underset{˙}{\cdot} X$
26		ovex	$⊢ a \underset{˙}{\cdot} X \in V$
27	25 21 26	fvmpt	$⊢ a \in B \to (x \in B ⟼ x \underset{˙}{\cdot} X) (a) = a \underset{˙}{\cdot} X$
28		oveq1	$⊢ x = b \to x \underset{˙}{\cdot} X = b \underset{˙}{\cdot} X$
29		ovex	$⊢ b \underset{˙}{\cdot} X \in V$
30	28 21 29	fvmpt	$⊢ b \in B \to (x \in B ⟼ x \underset{˙}{\cdot} X) (b) = b \underset{˙}{\cdot} X$
31	27 30	oveqan12d	$⊢ (a \in B \land b \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (a) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (b) = (a \underset{˙}{\cdot} X) +_{R} (b \underset{˙}{\cdot} X)$
32	31	adantl	$⊢ ((R \in SRing \land X \in B) \land (a \in B \land b \in B)) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (a) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (b) = (a \underset{˙}{\cdot} X) +_{R} (b \underset{˙}{\cdot} X)$
33	16 24 32	3eqtr4d	$⊢ ((R \in SRing \land X \in B) \land (a \in B \land b \in B)) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (a +_{R} b) = (x \in B ⟼ x \underset{˙}{\cdot} X) (a) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (b)$
34	33	ralrimivva	$⊢ (R \in SRing \land X \in B) \to \forall a \in B \forall b \in B (x \in B ⟼ x \underset{˙}{\cdot} X) (a +_{R} b) = (x \in B ⟼ x \underset{˙}{\cdot} X) (a) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (b)$
35		eqid	$⊢ 0_{R} = 0_{R}$
36	1 35	srg0cl	$⊢ R \in SRing \to 0_{R} \in B$
37	36	adantr	$⊢ (R \in SRing \land X \in B) \to 0_{R} \in B$
38		oveq1	$⊢ x = 0_{R} \to x \underset{˙}{\cdot} X = 0_{R} \underset{˙}{\cdot} X$
39		ovex	$⊢ 0_{R} \underset{˙}{\cdot} X \in V$
40	38 21 39	fvmpt	$⊢ 0_{R} \in B \to (x \in B ⟼ x \underset{˙}{\cdot} X) (0_{R}) = 0_{R} \underset{˙}{\cdot} X$
41	37 40	syl	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (0_{R}) = 0_{R} \underset{˙}{\cdot} X$
42	1 2 35	srglz	$⊢ (R \in SRing \land X \in B) \to 0_{R} \underset{˙}{\cdot} X = 0_{R}$
43	41 42	eqtrd	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) (0_{R}) = 0_{R}$
44	9 34 43	3jca	$⊢ (R \in SRing \land X \in B) \to ((x \in B ⟼ x \underset{˙}{\cdot} X) : B ⟶ B \land \forall a \in B \forall b \in B (x \in B ⟼ x \underset{˙}{\cdot} X) (a +_{R} b) = (x \in B ⟼ x \underset{˙}{\cdot} X) (a) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (b) \land (x \in B ⟼ x \underset{˙}{\cdot} X) (0_{R}) = 0_{R})$
45	1 1 13 13 35 35	ismhm	$⊢ (x \in B ⟼ x \underset{˙}{\cdot} X) \in (R MndHom R) \leftrightarrow ((R \in Mnd \land R \in Mnd) \land ((x \in B ⟼ x \underset{˙}{\cdot} X) : B ⟶ B \land \forall a \in B \forall b \in B (x \in B ⟼ x \underset{˙}{\cdot} X) (a +_{R} b) = (x \in B ⟼ x \underset{˙}{\cdot} X) (a) +_{R} (x \in B ⟼ x \underset{˙}{\cdot} X) (b) \land (x \in B ⟼ x \underset{˙}{\cdot} X) (0_{R}) = 0_{R}))$
46	5 44 45	sylanbrc	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ x \underset{˙}{\cdot} X) \in (R MndHom R)$

Metamath Proof Explorer

Theorem srgrmhm

Proof