Proof of Theorem mnringmulrd
Step | Hyp | Ref
| Expression |
1 | | mnringmulrd.1 |
. . . 4
⊢ 𝐹 = (𝑅 MndRing 𝑀) |
2 | | mnringmulrd.2 |
. . . 4
⊢ 𝐵 = (Base‘𝐹) |
3 | | mnringmulrd.5 |
. . . 4
⊢ 𝐴 = (Base‘𝑀) |
4 | | eqid 2759 |
. . . 4
⊢ (𝑅 freeLMod 𝐴) = (𝑅 freeLMod 𝐴) |
5 | | mnringmulrd.7 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑈) |
6 | | mnringmulrd.8 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ 𝑊) |
7 | 1, 2, 3, 4, 5, 6 | mnringbaserd 41282 |
. . 3
⊢ (𝜑 → 𝐵 = (Base‘(𝑅 freeLMod 𝐴))) |
8 | 3 | fvexi 6665 |
. . . . . 6
⊢ 𝐴 ∈ V |
9 | 8, 8 | mpoex 7775 |
. . . . 5
⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))) ∈
V |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))) ∈
V) |
11 | 1 | ovexi 7177 |
. . . . 5
⊢ 𝐹 ∈ V |
12 | 11 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ V) |
13 | | ovex 7176 |
. . . . 5
⊢ (𝑅 freeLMod 𝐴) ∈ V |
14 | 13 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑅 freeLMod 𝐴) ∈ V) |
15 | 2, 7 | syl5eqr 2808 |
. . . 4
⊢ (𝜑 → (Base‘𝐹) = (Base‘(𝑅 freeLMod 𝐴))) |
16 | 1, 3, 4, 5, 6 | mnringaddgd 41286 |
. . . . 5
⊢ (𝜑 →
(+g‘(𝑅
freeLMod 𝐴)) =
(+g‘𝐹)) |
17 | 16 | eqcomd 2765 |
. . . 4
⊢ (𝜑 → (+g‘𝐹) = (+g‘(𝑅 freeLMod 𝐴))) |
18 | 10, 12, 14, 15, 17 | gsumpropd 17939 |
. . 3
⊢ (𝜑 → (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))) = ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) |
19 | 7, 7, 18 | mpoeq123dv 7216 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) = (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))))) |
20 | | fvex 6664 |
. . . . 5
⊢
(Base‘(𝑅
freeLMod 𝐴)) ∈
V |
21 | 20, 20 | mpoex 7775 |
. . . 4
⊢ (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) ∈
V |
22 | | mulrid 16659 |
. . . . 5
⊢
.r = Slot (.r‘ndx) |
23 | 22 | setsid 16581 |
. . . 4
⊢ (((𝑅 freeLMod 𝐴) ∈ V ∧ (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) ∈ V) →
(𝑥 ∈
(Base‘(𝑅 freeLMod
𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) =
(.r‘((𝑅
freeLMod 𝐴) sSet
〈(.r‘ndx), (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉))) |
24 | 13, 21, 23 | mp2an 692 |
. . 3
⊢ (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) =
(.r‘((𝑅
freeLMod 𝐴) sSet
〈(.r‘ndx), (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) |
25 | | mnringmulrd.3 |
. . . . 5
⊢ · =
(.r‘𝑅) |
26 | | mnringmulrd.4 |
. . . . 5
⊢ 0 =
(0g‘𝑅) |
27 | | mnringmulrd.6 |
. . . . 5
⊢ + =
(+g‘𝑀) |
28 | | eqid 2759 |
. . . . 5
⊢
(Base‘(𝑅
freeLMod 𝐴)) =
(Base‘(𝑅 freeLMod
𝐴)) |
29 | 1, 25, 26, 3, 27, 4, 28, 5, 6 | mnringvald 41279 |
. . . 4
⊢ (𝜑 → 𝐹 = ((𝑅 freeLMod 𝐴) sSet 〈(.r‘ndx),
(𝑥 ∈
(Base‘(𝑅 freeLMod
𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) |
30 | 29 | fveq2d 6655 |
. . 3
⊢ (𝜑 → (.r‘𝐹) = (.r‘((𝑅 freeLMod 𝐴) sSet 〈(.r‘ndx),
(𝑥 ∈
(Base‘(𝑅 freeLMod
𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉))) |
31 | 24, 30 | eqtr4id 2813 |
. 2
⊢ (𝜑 → (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) =
(.r‘𝐹)) |
32 | 19, 31 | eqtrd 2794 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) =
(.r‘𝐹)) |