Step | Hyp | Ref
| Expression |
1 | | srgmnd 18509 |
. . . 4
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
2 | 1, 1 | jca 554 |
. . 3
⊢ (𝑅 ∈ SRing → (𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd)) |
3 | 2 | adantr 481 |
. 2
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd)) |
4 | | srglmhm.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
5 | | srglmhm.t |
. . . . . 6
⊢ · =
(.r‘𝑅) |
6 | 4, 5 | srgcl 18512 |
. . . . 5
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑋 · 𝑥) ∈ 𝐵) |
7 | 6 | 3expa 1265 |
. . . 4
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑋 · 𝑥) ∈ 𝐵) |
8 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) |
9 | 7, 8 | fmptd 6385 |
. . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)):𝐵⟶𝐵) |
10 | | 3anass 1042 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ↔ (𝑋 ∈ 𝐵 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) |
11 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘𝑅) = (+g‘𝑅) |
12 | 4, 11, 5 | srgdi 18516 |
. . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑋 · (𝑎(+g‘𝑅)𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) |
13 | 10, 12 | sylan2br 493 |
. . . . . 6
⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵))) → (𝑋 · (𝑎(+g‘𝑅)𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) |
14 | 13 | anassrs 680 |
. . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑋 · (𝑎(+g‘𝑅)𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) |
15 | 4, 11 | srgacl 18524 |
. . . . . . . 8
⊢ ((𝑅 ∈ SRing ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
16 | 15 | 3expb 1266 |
. . . . . . 7
⊢ ((𝑅 ∈ SRing ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
17 | 16 | adantlr 751 |
. . . . . 6
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(+g‘𝑅)𝑏) ∈ 𝐵) |
18 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = (𝑎(+g‘𝑅)𝑏) → (𝑋 · 𝑥) = (𝑋 · (𝑎(+g‘𝑅)𝑏))) |
19 | | ovex 6678 |
. . . . . . 7
⊢ (𝑋 · (𝑎(+g‘𝑅)𝑏)) ∈ V |
20 | 18, 8, 19 | fvmpt 6282 |
. . . . . 6
⊢ ((𝑎(+g‘𝑅)𝑏) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (𝑋 · (𝑎(+g‘𝑅)𝑏))) |
21 | 17, 20 | syl 17 |
. . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (𝑋 · (𝑎(+g‘𝑅)𝑏))) |
22 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (𝑋 · 𝑥) = (𝑋 · 𝑎)) |
23 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑋 · 𝑎) ∈ V |
24 | 22, 8, 23 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎) = (𝑋 · 𝑎)) |
25 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑥 = 𝑏 → (𝑋 · 𝑥) = (𝑋 · 𝑏)) |
26 | | ovex 6678 |
. . . . . . . 8
⊢ (𝑋 · 𝑏) ∈ V |
27 | 25, 8, 26 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑏 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏) = (𝑋 · 𝑏)) |
28 | 24, 27 | oveqan12d 6669 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) |
29 | 28 | adantl 482 |
. . . . 5
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏)) = ((𝑋 · 𝑎)(+g‘𝑅)(𝑋 · 𝑏))) |
30 | 14, 21, 29 | 3eqtr4d 2666 |
. . . 4
⊢ (((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏))) |
31 | 30 | ralrimivva 2971 |
. . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏))) |
32 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
33 | 4, 32 | srg0cl 18519 |
. . . . . 6
⊢ (𝑅 ∈ SRing →
(0g‘𝑅)
∈ 𝐵) |
34 | 33 | adantr 481 |
. . . . 5
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (0g‘𝑅) ∈ 𝐵) |
35 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = (0g‘𝑅) → (𝑋 · 𝑥) = (𝑋 ·
(0g‘𝑅))) |
36 | | ovex 6678 |
. . . . . 6
⊢ (𝑋 ·
(0g‘𝑅))
∈ V |
37 | 35, 8, 36 | fvmpt 6282 |
. . . . 5
⊢
((0g‘𝑅) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (𝑋 ·
(0g‘𝑅))) |
38 | 34, 37 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (𝑋 ·
(0g‘𝑅))) |
39 | 4, 5, 32 | srgrz 18526 |
. . . 4
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑋 ·
(0g‘𝑅)) =
(0g‘𝑅)) |
40 | 38, 39 | eqtrd 2656 |
. . 3
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (0g‘𝑅)) |
41 | 9, 31, 40 | 3jca 1242 |
. 2
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)):𝐵⟶𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (0g‘𝑅))) |
42 | 4, 4, 11, 11, 32, 32 | ismhm 17337 |
. 2
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 MndHom 𝑅) ↔ ((𝑅 ∈ Mnd ∧ 𝑅 ∈ Mnd) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)):𝐵⟶𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(𝑎(+g‘𝑅)𝑏)) = (((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑎)(+g‘𝑅)((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘𝑏)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥))‘(0g‘𝑅)) = (0g‘𝑅)))) |
43 | 3, 41, 42 | sylanbrc 698 |
1
⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 MndHom 𝑅)) |