srglmhm

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

	Ref	Expression
Hypotheses	srglmhm.b	$⊢ B = {Base}_{R}$
	srglmhm.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	srglmhm	$⊢ (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	3expa	$⊢ ((R \in SRing \land X \in B) \land x \in B) \to X \underset{˙}{\cdot} x \in B$
8	7	fmpttd	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ X \underset{˙}{\cdot} x) : B ⟶ B$
9		3anass	$⊢ (X \in B \land a \in B \land b \in B) \leftrightarrow (X \in B \land (a \in B \land b \in B))$
10		eqid	$⊢ +_{R} = +_{R}$
11	1 10 2	srgdi	$⊢ (R \in SRing \land (X \in B \land a \in B \land b \in B)) \to X \underset{˙}{\cdot} (a +_{R} b) = (X \underset{˙}{\cdot} a) +_{R} (X \underset{˙}{\cdot} b)$
12	9 11	sylan2br	$⊢ (R \in SRing \land (X \in B \land (a \in B \land b \in B))) \to X \underset{˙}{\cdot} (a +_{R} b) = (X \underset{˙}{\cdot} a) +_{R} (X \underset{˙}{\cdot} b)$
13	12	anassrs	$⊢ ((R \in SRing \land X \in B) \land (a \in B \land b \in B)) \to X \underset{˙}{\cdot} (a +_{R} b) = (X \underset{˙}{\cdot} a) +_{R} (X \underset{˙}{\cdot} b)$
14	1 10	srgacl	$⊢ (R \in SRing \land a \in B \land b \in B) \to a +_{R} b \in B$
15	14	3expb	$⊢ (R \in SRing \land (a \in B \land b \in B)) \to a +_{R} b \in B$
16	15	adantlr	$⊢ ((R \in SRing \land X \in B) \land (a \in B \land b \in B)) \to a +_{R} b \in B$
17		oveq2	$⊢ x = a +_{R} b \to X \underset{˙}{\cdot} x = X \underset{˙}{\cdot} (a +_{R} b)$
18		eqid	$⊢ (x \in B ⟼ X \underset{˙}{\cdot} x) = (x \in B ⟼ X \underset{˙}{\cdot} x)$
19		ovex	$⊢ X \underset{˙}{\cdot} (a +_{R} b) \in V$
20	17 18 19	fvmpt	$⊢ a +_{R} b \in B \to (x \in B ⟼ X \underset{˙}{\cdot} x) (a +_{R} b) = X \underset{˙}{\cdot} (a +_{R} b)$
21	16 20	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) = X \underset{˙}{\cdot} (a +_{R} b)$
22		oveq2	$⊢ x = a \to X \underset{˙}{\cdot} x = X \underset{˙}{\cdot} a$
23		ovex	$⊢ X \underset{˙}{\cdot} a \in V$
24	22 18 23	fvmpt	$⊢ a \in B \to (x \in B ⟼ X \underset{˙}{\cdot} x) (a) = X \underset{˙}{\cdot} a$
25		oveq2	$⊢ x = b \to X \underset{˙}{\cdot} x = X \underset{˙}{\cdot} b$
26		ovex	$⊢ X \underset{˙}{\cdot} b \in V$
27	25 18 26	fvmpt	$⊢ b \in B \to (x \in B ⟼ X \underset{˙}{\cdot} x) (b) = X \underset{˙}{\cdot} b$
28	24 27	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) = (X \underset{˙}{\cdot} a) +_{R} (X \underset{˙}{\cdot} b)$
29	28	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) = (X \underset{˙}{\cdot} a) +_{R} (X \underset{˙}{\cdot} b)$
30	13 21 29	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)$
31	30	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)$
32		eqid	$⊢ 0_{R} = 0_{R}$
33	1 32	srg0cl	$⊢ R \in SRing \to 0_{R} \in B$
34	33	adantr	$⊢ (R \in SRing \land X \in B) \to 0_{R} \in B$
35		oveq2	$⊢ x = 0_{R} \to X \underset{˙}{\cdot} x = X \underset{˙}{\cdot} 0_{R}$
36		ovex	$⊢ X \underset{˙}{\cdot} 0_{R} \in V$
37	35 18 36	fvmpt	$⊢ 0_{R} \in B \to (x \in B ⟼ X \underset{˙}{\cdot} x) (0_{R}) = X \underset{˙}{\cdot} 0_{R}$
38	34 37	syl	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ X \underset{˙}{\cdot} x) (0_{R}) = X \underset{˙}{\cdot} 0_{R}$
39	1 2 32	srgrz	$⊢ (R \in SRing \land X \in B) \to X \underset{˙}{\cdot} 0_{R} = 0_{R}$
40	38 39	eqtrd	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ X \underset{˙}{\cdot} x) (0_{R}) = 0_{R}$
41	8 31 40	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})$
42	1 1 10 10 32 32	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}))$
43	5 41 42	sylanbrc	$⊢ (R \in SRing \land X \in B) \to (x \in B ⟼ X \underset{˙}{\cdot} x) \in (R MndHom R)$

Metamath Proof Explorer

Theorem srglmhm

Proof