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 2736 | . . . 4
⊢ (𝑅 freeLMod 𝐴) = (𝑅 freeLMod 𝐴) | 
| 5 |  | mnringmulrd.7 | . . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑈) | 
| 6 |  | mnringmulrd.8 | . . . 4
⊢ (𝜑 → 𝑀 ∈ 𝑊) | 
| 7 | 1, 2, 3, 4, 5, 6 | mnringbaserd 44237 | . . 3
⊢ (𝜑 → 𝐵 = (Base‘(𝑅 freeLMod 𝐴))) | 
| 8 | 3 | fvexi 6919 | . . . . . 6
⊢ 𝐴 ∈ V | 
| 9 | 8, 8 | mpoex 8105 | . . . . 5
⊢ (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))) ∈
V | 
| 10 | 9 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))) ∈
V) | 
| 11 | 1 | ovexi 7466 | . . . . 5
⊢ 𝐹 ∈ V | 
| 12 | 11 | a1i 11 | . . . 4
⊢ (𝜑 → 𝐹 ∈ V) | 
| 13 |  | ovex 7465 | . . . . 5
⊢ (𝑅 freeLMod 𝐴) ∈ V | 
| 14 | 13 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑅 freeLMod 𝐴) ∈ V) | 
| 15 | 2, 7 | eqtr3id 2790 | . . . 4
⊢ (𝜑 → (Base‘𝐹) = (Base‘(𝑅 freeLMod 𝐴))) | 
| 16 | 1, 3, 4, 5, 6 | mnringaddgd 44241 | . . . . 5
⊢ (𝜑 →
(+g‘(𝑅
freeLMod 𝐴)) =
(+g‘𝐹)) | 
| 17 | 16 | eqcomd 2742 | . . . 4
⊢ (𝜑 → (+g‘𝐹) = (+g‘(𝑅 freeLMod 𝐴))) | 
| 18 | 10, 12, 14, 15, 17 | gsumpropd 18692 | . . 3
⊢ (𝜑 → (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))) = ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) | 
| 19 | 7, 7, 18 | mpoeq123dv 7509 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) = (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))))) | 
| 20 |  | fvex 6918 | . . . . 5
⊢
(Base‘(𝑅
freeLMod 𝐴)) ∈
V | 
| 21 | 20, 20 | mpoex 8105 | . . . 4
⊢ (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) ∈
V | 
| 22 |  | mulridx 17339 | . . . . 5
⊢
.r = Slot (.r‘ndx) | 
| 23 | 22 | setsid 17245 | . . . 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 2736 | . . . . 5
⊢
(Base‘(𝑅
freeLMod 𝐴)) =
(Base‘(𝑅 freeLMod
𝐴)) | 
| 29 | 1, 25, 26, 3, 27, 4, 28, 5, 6 | mnringvald 44232 | . . . 4
⊢ (𝜑 → 𝐹 = ((𝑅 freeLMod 𝐴) sSet 〈(.r‘ndx),
(𝑥 ∈
(Base‘(𝑅 freeLMod
𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) | 
| 30 | 29 | fveq2d 6909 | . . 3
⊢ (𝜑 → (.r‘𝐹) = (.r‘((𝑅 freeLMod 𝐴) sSet 〈(.r‘ndx),
(𝑥 ∈
(Base‘(𝑅 freeLMod
𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉))) | 
| 31 | 24, 30 | eqtr4id 2795 | . 2
⊢ (𝜑 → (𝑥 ∈ (Base‘(𝑅 freeLMod 𝐴)), 𝑦 ∈ (Base‘(𝑅 freeLMod 𝐴)) ↦ ((𝑅 freeLMod 𝐴) Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) =
(.r‘𝐹)) | 
| 32 | 19, 31 | eqtrd 2776 | 1
⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝐹 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) =
(.r‘𝐹)) |