| 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 | . . . . . . 7
⊢ 𝐵 = (Base‘𝑅) | 
| 5 |  | srglmhm.t | . . . . . . 7
⊢  · =
(.r‘𝑅) | 
| 6 | 4, 5 | srgcl 20191 | . . . . . 6
⊢ ((𝑅 ∈ SRing ∧ 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑥 · 𝑋) ∈ 𝐵) | 
| 7 | 6 | 3com23 1126 | . . . . 5
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 𝑋) ∈ 𝐵) | 
| 8 | 7 | 3expa 1118 | . . . 4
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 · 𝑋) ∈ 𝐵) | 
| 9 | 8 | fmpttd 7134 | . . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)):𝐵⟶𝐵) | 
| 10 |  | 3anrot 1099 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ↔ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) | 
| 11 |  | 3anass 1094 | . . . . . . . 8
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ↔ (𝑋 ∈ 𝐵 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) | 
| 12 | 10, 11 | bitr3i 277 | . . . . . . 7
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ↔ (𝑋 ∈ 𝐵 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) | 
| 13 |  | eqid 2736 | . . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 14 | 4, 13, 5 | srgdir 20196 | . . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ((𝑎(+g‘𝑅)𝑏) · 𝑋) = ((𝑎 · 𝑋)(+g‘𝑅)(𝑏 · 𝑋))) | 
| 15 | 12, 14 | sylan2br 595 | . . . . . 6
⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) → ((𝑎(+g‘𝑅)𝑏) · 𝑋) = ((𝑎 · 𝑋)(+g‘𝑅)(𝑏 · 𝑋))) | 
| 16 | 15 | anassrs 467 | . . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(+g‘𝑅)𝑏) · 𝑋) = ((𝑎 · 𝑋)(+g‘𝑅)(𝑏 · 𝑋))) | 
| 17 | 4, 13 | srgacl 20203 | . . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 18 | 17 | 3expb 1120 | . . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 19 | 18 | adantlr 715 | . . . . . 6
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) | 
| 20 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑥 = (𝑎(+g‘𝑅)𝑏) → (𝑥 · 𝑋) = ((𝑎(+g‘𝑅)𝑏) · 𝑋)) | 
| 21 |  | eqid 2736 | . . . . . . 7
⊢ (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) = (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) | 
| 22 |  | ovex 7465 | . . . . . . 7
⊢ ((𝑎(+g‘𝑅)𝑏) · 𝑋) ∈ V | 
| 23 | 20, 21, 22 | fvmpt 7015 | . . . . . 6
⊢ ((𝑎(+g‘𝑅)𝑏) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(𝑎(+g‘𝑅)𝑏)) = ((𝑎(+g‘𝑅)𝑏) · 𝑋)) | 
| 24 | 19, 23 | syl 17 | . . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(𝑎(+g‘𝑅)𝑏)) = ((𝑎(+g‘𝑅)𝑏) · 𝑋)) | 
| 25 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝑥 · 𝑋) = (𝑎 · 𝑋)) | 
| 26 |  | ovex 7465 | . . . . . . . 8
⊢ (𝑎 · 𝑋) ∈ V | 
| 27 | 25, 21, 26 | fvmpt 7015 | . . . . . . 7
⊢ (𝑎 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑎) = (𝑎 · 𝑋)) | 
| 28 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑏 → (𝑥 · 𝑋) = (𝑏 · 𝑋)) | 
| 29 |  | ovex 7465 | . . . . . . . 8
⊢ (𝑏 · 𝑋) ∈ V | 
| 30 | 28, 21, 29 | fvmpt 7015 | . . . . . . 7
⊢ (𝑏 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑏) = (𝑏 · 𝑋)) | 
| 31 | 27, 30 | oveqan12d 7451 | . . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑏)) = ((𝑎 · 𝑋)(+g‘𝑅)(𝑏 · 𝑋))) | 
| 32 | 31 | adantl 481 | . . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑏)) = ((𝑎 · 𝑋)(+g‘𝑅)(𝑏 · 𝑋))) | 
| 33 | 16, 24, 32 | 3eqtr4d 2786 | . . . 4
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑏))) | 
| 34 | 33 | ralrimivva 3201 | . . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑏))) | 
| 35 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 36 | 4, 35 | srg0cl 20198 | . . . . . 6
⊢ (𝑅 ∈ SRing →
(0g‘𝑅)
∈ 𝐵) | 
| 37 | 36 | adantr 480 | . . . . 5
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (0g‘𝑅) ∈ 𝐵) | 
| 38 |  | oveq1 7439 | . . . . . 6
⊢ (𝑥 = (0g‘𝑅) → (𝑥 · 𝑋) = ((0g‘𝑅) · 𝑋)) | 
| 39 |  | ovex 7465 | . . . . . 6
⊢
((0g‘𝑅) · 𝑋) ∈ V | 
| 40 | 38, 21, 39 | fvmpt 7015 | . . . . 5
⊢
((0g‘𝑅) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(0g‘𝑅)) = ((0g‘𝑅) · 𝑋)) | 
| 41 | 37, 40 | syl 17 | . . . 4
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(0g‘𝑅)) = ((0g‘𝑅) · 𝑋)) | 
| 42 | 4, 5, 35 | srglz 20206 | . . . 4
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((0g‘𝑅) · 𝑋) = (0g‘𝑅)) | 
| 43 | 41, 42 | eqtrd 2776 | . . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(0g‘𝑅)) = (0g‘𝑅)) | 
| 44 | 9, 34, 43 | 3jca 1128 | . 2
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)):𝐵⟶𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑏)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(0g‘𝑅)) = (0g‘𝑅))) | 
| 45 | 4, 4, 13, 13, 35, 35 | ismhm 18799 | . 2
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) ∈ (𝑅 MndHom 𝑅) ↔ ((𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)):𝐵⟶𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘𝑏)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋))‘(0g‘𝑅)) = (0g‘𝑅)))) | 
| 46 | 3, 44, 45 | sylanbrc 583 | 1
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) ∈ (𝑅 MndHom 𝑅)) |