| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | srgmnd 20188 | . . . 4
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) | 
| 2 | 1, 1 | jca 511 | . . 3
⊢ (𝑅 ∈ SRing → (𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd)) | 
| 3 | 2 | adantr 480 | . 2
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd)) | 
| 4 |  | srglmhm.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑅) | 
| 5 |  | srglmhm.t | . . . . . 6
⊢  · =
(.r‘𝑅) | 
| 6 | 4, 5 | srgcl 20191 | . . . . 5
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑋 · 𝑥) ∈ 𝐵) | 
| 7 | 6 | 3expa 1118 | . . . 4
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑋 · 𝑥) ∈ 𝐵) | 
| 8 | 7 | fmpttd 7134 | . . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)):𝐵⟶𝐵) | 
| 9 |  | 3anass 1094 | . . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ↔ (𝑋 ∈ 𝐵 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) | 
| 10 |  | eqid 2736 | . . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 11 | 4, 10, 5 | srgdi 20195 | . . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑋 · (𝑎(+g‘𝑅)𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) | 
| 12 | 9, 11 | sylan2br 595 | . . . . . 6
⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) → (𝑋 · (𝑎(+g‘𝑅)𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) | 
| 13 | 12 | anassrs 467 | . . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑋 · (𝑎(+g‘𝑅)𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) | 
| 14 | 4, 10 | srgacl 20203 | . . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 15 | 14 | 3expb 1120 | . . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 16 | 15 | adantlr 715 | . . . . . 6
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 17 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = (𝑎(+g‘𝑅)𝑏) → (𝑋 · 𝑥) = (𝑋 · (𝑎(+g‘𝑅)𝑏))) | 
| 18 |  | eqid 2736 | . . . . . . 7
⊢ (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) | 
| 19 |  | ovex 7465 | . . . . . . 7
⊢ (𝑋 · (𝑎(+g‘𝑅)𝑏)) ∈ V | 
| 20 | 17, 18, 19 | fvmpt 7015 | . . . . . 6
⊢ ((𝑎(+g‘𝑅)𝑏) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (𝑋 · (𝑎(+g‘𝑅)𝑏))) | 
| 21 | 16, 20 | syl 17 | . . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (𝑋 · (𝑎(+g‘𝑅)𝑏))) | 
| 22 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝑋 · 𝑥) = (𝑋 · 𝑎)) | 
| 23 |  | ovex 7465 | . . . . . . . 8
⊢ (𝑋 · 𝑎) ∈ V | 
| 24 | 22, 18, 23 | fvmpt 7015 | . . . . . . 7
⊢ (𝑎 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎) = (𝑋 · 𝑎)) | 
| 25 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑥 = 𝑏 → (𝑋 · 𝑥) = (𝑋 · 𝑏)) | 
| 26 |  | ovex 7465 | . . . . . . . 8
⊢ (𝑋 · 𝑏) ∈ V | 
| 27 | 25, 18, 26 | fvmpt 7015 | . . . . . . 7
⊢ (𝑏 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏) = (𝑋 · 𝑏)) | 
| 28 | 24, 27 | oveqan12d 7451 | . . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) | 
| 29 | 28 | adantl 481 | . . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) | 
| 30 | 13, 21, 29 | 3eqtr4d 2786 | . . . 4
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏))) | 
| 31 | 30 | ralrimivva 3201 | . . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏))) | 
| 32 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 33 | 4, 32 | srg0cl 20198 | . . . . . 6
⊢ (𝑅 ∈ SRing →
(0g‘𝑅)
∈ 𝐵) | 
| 34 | 33 | adantr 480 | . . . . 5
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (0g‘𝑅) ∈ 𝐵) | 
| 35 |  | oveq2 7440 | . . . . . 6
⊢ (𝑥 = (0g‘𝑅) → (𝑋 · 𝑥) = (𝑋 ·
(0g‘𝑅))) | 
| 36 |  | ovex 7465 | . . . . . 6
⊢ (𝑋 ·
(0g‘𝑅))
∈ V | 
| 37 | 35, 18, 36 | fvmpt 7015 | . . . . 5
⊢
((0g‘𝑅) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (𝑋 ·
(0g‘𝑅))) | 
| 38 | 34, 37 | syl 17 | . . . 4
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (𝑋 ·
(0g‘𝑅))) | 
| 39 | 4, 5, 32 | srgrz 20205 | . . . 4
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑋 ·
(0g‘𝑅)) =
(0g‘𝑅)) | 
| 40 | 38, 39 | eqtrd 2776 | . . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (0g‘𝑅)) | 
| 41 | 8, 31, 40 | 3jca 1128 | . 2
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)):𝐵⟶𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (0g‘𝑅))) | 
| 42 | 4, 4, 10, 10, 32, 32 | ismhm 18799 | . 2
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 MndHom 𝑅) ↔ ((𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)):𝐵⟶𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (0g‘𝑅)))) | 
| 43 | 3, 41, 42 | sylanbrc 583 | 1
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 MndHom 𝑅)) |