Theorem 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	srglmhm.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	srgrmhm	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		srglmhm.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		srglmhm.t	⊢ · = ( .r ‘ 𝑅 )
3		srgmnd	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
4	3 3	jca	⊢ ( 𝑅 ∈ SRing → ( 𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd ) )
5	4	adantr	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd ) )
6	1 2	srgcl	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 · 𝑋 ) ∈ 𝐵 )
7	6	3com23	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 𝑋 ) ∈ 𝐵 )
8	7	3expa	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 · 𝑋 ) ∈ 𝐵 )
9	8	fmpttd	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) : 𝐵 ⟶ 𝐵 )
10		3anrot	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ↔ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
11		3anass	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) )
12	10 11	bitr3i	⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) )
13		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
14	1 13 2	srgdir	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) · 𝑋 ) = ( ( 𝑎 · 𝑋 ) ( +g ‘ 𝑅 ) ( 𝑏 · 𝑋 ) ) )
15	12 14	sylan2br	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) · 𝑋 ) = ( ( 𝑎 · 𝑋 ) ( +g ‘ 𝑅 ) ( 𝑏 · 𝑋 ) ) )
16	15	anassrs	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) · 𝑋 ) = ( ( 𝑎 · 𝑋 ) ( +g ‘ 𝑅 ) ( 𝑏 · 𝑋 ) ) )
17	1 13	srgacl	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
18	17	3expb	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
19	18	adantlr	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
20		oveq1	⊢ ( 𝑥 = ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) → ( 𝑥 · 𝑋 ) = ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) · 𝑋 ) )
21		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) )
22		ovex	⊢ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) · 𝑋 ) ∈ V
23	20 21 22	fvmpt	⊢ ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) · 𝑋 ) )
24	19 23	syl	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) · 𝑋 ) )
25		oveq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 · 𝑋 ) = ( 𝑎 · 𝑋 ) )
26		ovex	⊢ ( 𝑎 · 𝑋 ) ∈ V
27	25 21 26	fvmpt	⊢ ( 𝑎 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑎 ) = ( 𝑎 · 𝑋 ) )
28		oveq1	⊢ ( 𝑥 = 𝑏 → ( 𝑥 · 𝑋 ) = ( 𝑏 · 𝑋 ) )
29		ovex	⊢ ( 𝑏 · 𝑋 ) ∈ V
30	28 21 29	fvmpt	⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑏 ) = ( 𝑏 · 𝑋 ) )
31	27 30	oveqan12d	⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑎 ) ( +g ‘ 𝑅 ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑏 ) ) = ( ( 𝑎 · 𝑋 ) ( +g ‘ 𝑅 ) ( 𝑏 · 𝑋 ) ) )
32	31	adantl	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑎 ) ( +g ‘ 𝑅 ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑏 ) ) = ( ( 𝑎 · 𝑋 ) ( +g ‘ 𝑅 ) ( 𝑏 · 𝑋 ) ) )
33	16 24 32	3eqtr4d	⊢ ( ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑎 ) ( +g ‘ 𝑅 ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑏 ) ) )
34	33	ralrimivva	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑎 ) ( +g ‘ 𝑅 ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑏 ) ) )
35		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
36	1 35	srg0cl	⊢ ( 𝑅 ∈ SRing → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
37	36	adantr	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( 0g ‘ 𝑅 ) ∈ 𝐵 )
38		oveq1	⊢ ( 𝑥 = ( 0g ‘ 𝑅 ) → ( 𝑥 · 𝑋 ) = ( ( 0g ‘ 𝑅 ) · 𝑋 ) )
39		ovex	⊢ ( ( 0g ‘ 𝑅 ) · 𝑋 ) ∈ V
40	38 21 39	fvmpt	⊢ ( ( 0g ‘ 𝑅 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 0g ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) · 𝑋 ) )
41	37 40	syl	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 0g ‘ 𝑅 ) ) = ( ( 0g ‘ 𝑅 ) · 𝑋 ) )
42	1 2 35	srglz	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 0g ‘ 𝑅 ) · 𝑋 ) = ( 0g ‘ 𝑅 ) )
43	41 42	eqtrd	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
44	9 34 43	3jca	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑎 ) ( +g ‘ 𝑅 ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑏 ) ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) )
45	1 1 13 13 35 35	ismhm	⊢ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ∈ ( 𝑅 MndHom 𝑅 ) ↔ ( ( 𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) : 𝐵 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑎 ) ( +g ‘ 𝑅 ) ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ 𝑏 ) ) ∧ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) ) )
46	5 44 45	sylanbrc	⊢ ( ( 𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 · 𝑋 ) ) ∈ ( 𝑅 MndHom 𝑅 ) )