Step | Hyp | Ref
| Expression |
1 | | mnringvald.1 |
. 2
⊢ 𝐹 = (𝑅 MndRing 𝑀) |
2 | | mnringvald.8 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑈) |
3 | 2 | elexd 3443 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
4 | | mnringvald.9 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ 𝑊) |
5 | 4 | elexd 3443 |
. . 3
⊢ (𝜑 → 𝑀 ∈ V) |
6 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑣(𝑟 = 𝑅 ∧ 𝑚 = 𝑀) |
7 | | nfcvd 2908 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) → Ⅎ𝑣(𝑉 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) |
8 | | ovexd 7269 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) → (𝑟 freeLMod (Base‘𝑚)) ∈ V) |
9 | | simpr 488 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → 𝑣 = (𝑟 freeLMod (Base‘𝑚))) |
10 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → 𝑟 = 𝑅) |
11 | | fveq2 6738 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = (Base‘𝑀)) |
12 | | mnringvald.4 |
. . . . . . . . . . 11
⊢ 𝐴 = (Base‘𝑀) |
13 | 11, 12 | eqtr4di 2798 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → (Base‘𝑚) = 𝐴) |
14 | 13 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (Base‘𝑚) = 𝐴) |
15 | 10, 14 | oveq12d 7252 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (𝑟 freeLMod (Base‘𝑚)) = (𝑅 freeLMod 𝐴)) |
16 | 9, 15 | eqtrd 2779 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → 𝑣 = (𝑅 freeLMod 𝐴)) |
17 | | mnringvald.6 |
. . . . . . 7
⊢ 𝑉 = (𝑅 freeLMod 𝐴) |
18 | 16, 17 | eqtr4di 2798 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → 𝑣 = 𝑉) |
19 | 18 | fveq2d 6742 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (Base‘𝑣) = (Base‘𝑉)) |
20 | | mnringvald.7 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑉) |
21 | 19, 20 | eqtr4di 2798 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (Base‘𝑣) = 𝐵) |
22 | | fveq2 6738 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = 𝑀 → (+g‘𝑚) = (+g‘𝑀)) |
23 | | mnringvald.5 |
. . . . . . . . . . . . . . . 16
⊢ + =
(+g‘𝑀) |
24 | 22, 23 | eqtr4di 2798 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑀 → (+g‘𝑚) = + ) |
25 | 24 | oveqd 7251 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑀 → (𝑎(+g‘𝑚)𝑏) = (𝑎 + 𝑏)) |
26 | 25 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (𝑎(+g‘𝑚)𝑏) = (𝑎 + 𝑏)) |
27 | 26 | eqeq2d 2750 |
. . . . . . . . . . . 12
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (𝑖 = (𝑎(+g‘𝑚)𝑏) ↔ 𝑖 = (𝑎 + 𝑏))) |
28 | | fveq2 6738 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
29 | | mnringvald.2 |
. . . . . . . . . . . . . . 15
⊢ · =
(.r‘𝑅) |
30 | 28, 29 | eqtr4di 2798 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = · ) |
31 | 30 | oveqd 7251 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)) = ((𝑥‘𝑎) · (𝑦‘𝑏))) |
32 | 31 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)) = ((𝑥‘𝑎) · (𝑦‘𝑏))) |
33 | | fveq2 6738 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
34 | | mnringvald.3 |
. . . . . . . . . . . . . 14
⊢ 0 =
(0g‘𝑅) |
35 | 33, 34 | eqtr4di 2798 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
36 | 35 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (0g‘𝑟) = 0 ) |
37 | 27, 32, 36 | ifbieq12d 4483 |
. . . . . . . . . . 11
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟)) = if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )) |
38 | 14, 37 | mpteq12dv 5156 |
. . . . . . . . . 10
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))) = (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))) |
39 | 14, 14, 38 | mpoeq123dv 7307 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟)))) = (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))) |
40 | 18, 39 | oveq12d 7252 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))) = (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 ))))) |
41 | 21, 21, 40 | mpoeq123dv 7307 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟)))))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))))) |
42 | 41 | opeq2d 4807 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → 〈(.r‘ndx),
(𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉 =
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉) |
43 | 18, 42 | oveq12d 7252 |
. . . . 5
⊢ (((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) ∧ 𝑣 = (𝑟 freeLMod (Base‘𝑚))) → (𝑣 sSet 〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉) = (𝑉 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) |
44 | 6, 7, 8, 43 | csbiedf 3859 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑚 = 𝑀) → ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet 〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉) = (𝑉 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) |
45 | | df-mnring 41550 |
. . . 4
⊢ MndRing
= (𝑟 ∈ V, 𝑚 ∈ V ↦
⦋(𝑟 freeLMod
(Base‘𝑚)) / 𝑣⦌(𝑣 sSet
〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉)) |
46 | | ovex 7267 |
. . . 4
⊢ (𝑉 sSet
〈(.r‘ndx), (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0 )))))〉) ∈
V |
47 | 44, 45, 46 | ovmpoa 7385 |
. . 3
⊢ ((𝑅 ∈ V ∧ 𝑀 ∈ V) → (𝑅 MndRing 𝑀) = (𝑉 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) |
48 | 3, 5, 47 | syl2anc 587 |
. 2
⊢ (𝜑 → (𝑅 MndRing 𝑀) = (𝑉 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) |
49 | 1, 48 | syl5eq 2792 |
1
⊢ (𝜑 → 𝐹 = (𝑉 sSet 〈(.r‘ndx),
(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑉 Σg (𝑎 ∈ 𝐴, 𝑏 ∈ 𝐴 ↦ (𝑖 ∈ 𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥‘𝑎) · (𝑦‘𝑏)), 0
)))))〉)) |