Detailed syntax breakdown of Definition df-mnring
Step | Hyp | Ref
| Expression |
1 | | cmnring 41277 |
. 2
class
MndRing |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | vm |
. . 3
setvar 𝑚 |
4 | | cvv 3407 |
. . 3
class
V |
5 | | vv |
. . . 4
setvar 𝑣 |
6 | 2 | cv 1538 |
. . . . 5
class 𝑟 |
7 | 3 | cv 1538 |
. . . . . 6
class 𝑚 |
8 | | cbs 16526 |
. . . . . 6
class
Base |
9 | 7, 8 | cfv 6328 |
. . . . 5
class
(Base‘𝑚) |
10 | | cfrlm 20496 |
. . . . 5
class
freeLMod |
11 | 6, 9, 10 | co 7143 |
. . . 4
class (𝑟 freeLMod (Base‘𝑚)) |
12 | 5 | cv 1538 |
. . . . 5
class 𝑣 |
13 | | cnx 16523 |
. . . . . . 7
class
ndx |
14 | | cmulr 16609 |
. . . . . . 7
class
.r |
15 | 13, 14 | cfv 6328 |
. . . . . 6
class
(.r‘ndx) |
16 | | vx |
. . . . . . 7
setvar 𝑥 |
17 | | vy |
. . . . . . 7
setvar 𝑦 |
18 | 12, 8 | cfv 6328 |
. . . . . . 7
class
(Base‘𝑣) |
19 | | va |
. . . . . . . . 9
setvar 𝑎 |
20 | | vb |
. . . . . . . . 9
setvar 𝑏 |
21 | | vi |
. . . . . . . . . 10
setvar 𝑖 |
22 | 21 | cv 1538 |
. . . . . . . . . . . 12
class 𝑖 |
23 | 19 | cv 1538 |
. . . . . . . . . . . . 13
class 𝑎 |
24 | 20 | cv 1538 |
. . . . . . . . . . . . 13
class 𝑏 |
25 | | cplusg 16608 |
. . . . . . . . . . . . . 14
class
+g |
26 | 7, 25 | cfv 6328 |
. . . . . . . . . . . . 13
class
(+g‘𝑚) |
27 | 23, 24, 26 | co 7143 |
. . . . . . . . . . . 12
class (𝑎(+g‘𝑚)𝑏) |
28 | 22, 27 | wceq 1539 |
. . . . . . . . . . 11
wff 𝑖 = (𝑎(+g‘𝑚)𝑏) |
29 | 16 | cv 1538 |
. . . . . . . . . . . . 13
class 𝑥 |
30 | 23, 29 | cfv 6328 |
. . . . . . . . . . . 12
class (𝑥‘𝑎) |
31 | 17 | cv 1538 |
. . . . . . . . . . . . 13
class 𝑦 |
32 | 24, 31 | cfv 6328 |
. . . . . . . . . . . 12
class (𝑦‘𝑏) |
33 | 6, 14 | cfv 6328 |
. . . . . . . . . . . 12
class
(.r‘𝑟) |
34 | 30, 32, 33 | co 7143 |
. . . . . . . . . . 11
class ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)) |
35 | | c0g 16756 |
. . . . . . . . . . . 12
class
0g |
36 | 6, 35 | cfv 6328 |
. . . . . . . . . . 11
class
(0g‘𝑟) |
37 | 28, 34, 36 | cif 4413 |
. . . . . . . . . 10
class if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟)) |
38 | 21, 9, 37 | cmpt 5105 |
. . . . . . . . 9
class (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))) |
39 | 19, 20, 9, 9, 38 | cmpo 7145 |
. . . . . . . 8
class (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟)))) |
40 | | cgsu 16757 |
. . . . . . . 8
class
Σg |
41 | 12, 39, 40 | co 7143 |
. . . . . . 7
class (𝑣 Σg
(𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))) |
42 | 16, 17, 18, 18, 41 | cmpo 7145 |
. . . . . 6
class (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟)))))) |
43 | 15, 42 | cop 4521 |
. . . . 5
class
〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉 |
44 | | csts 16524 |
. . . . 5
class
sSet |
45 | 12, 43, 44 | co 7143 |
. . . 4
class (𝑣 sSet
〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉) |
46 | 5, 11, 45 | csb 3801 |
. . 3
class
⦋(𝑟
freeLMod (Base‘𝑚)) /
𝑣⦌(𝑣 sSet
〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉) |
47 | 2, 3, 4, 4, 46 | cmpo 7145 |
. 2
class (𝑟 ∈ V, 𝑚 ∈ V ↦ ⦋(𝑟 freeLMod (Base‘𝑚)) / 𝑣⦌(𝑣 sSet 〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉)) |
48 | 1, 47 | wceq 1539 |
1
wff MndRing =
(𝑟 ∈ V, 𝑚 ∈ V ↦
⦋(𝑟 freeLMod
(Base‘𝑚)) / 𝑣⦌(𝑣 sSet
〈(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g‘𝑚)𝑏), ((𝑥‘𝑎)(.r‘𝑟)(𝑦‘𝑏)), (0g‘𝑟))))))〉)) |