Step | Hyp | Ref
| Expression |
1 | | cmnring 42578 |
. 2
class
MndRing |
2 | | vr |
. . 3
setvar π |
3 | | vm |
. . 3
setvar π |
4 | | cvv 3447 |
. . 3
class
V |
5 | | vv |
. . . 4
setvar π£ |
6 | 2 | cv 1541 |
. . . . 5
class π |
7 | 3 | cv 1541 |
. . . . . 6
class π |
8 | | cbs 17091 |
. . . . . 6
class
Base |
9 | 7, 8 | cfv 6500 |
. . . . 5
class
(Baseβπ) |
10 | | cfrlm 21175 |
. . . . 5
class
freeLMod |
11 | 6, 9, 10 | co 7361 |
. . . 4
class (π freeLMod (Baseβπ)) |
12 | 5 | cv 1541 |
. . . . 5
class π£ |
13 | | cnx 17073 |
. . . . . . 7
class
ndx |
14 | | cmulr 17142 |
. . . . . . 7
class
.r |
15 | 13, 14 | cfv 6500 |
. . . . . 6
class
(.rβndx) |
16 | | vx |
. . . . . . 7
setvar π₯ |
17 | | vy |
. . . . . . 7
setvar π¦ |
18 | 12, 8 | cfv 6500 |
. . . . . . 7
class
(Baseβπ£) |
19 | | va |
. . . . . . . . 9
setvar π |
20 | | vb |
. . . . . . . . 9
setvar π |
21 | | vi |
. . . . . . . . . 10
setvar π |
22 | 21 | cv 1541 |
. . . . . . . . . . . 12
class π |
23 | 19 | cv 1541 |
. . . . . . . . . . . . 13
class π |
24 | 20 | cv 1541 |
. . . . . . . . . . . . 13
class π |
25 | | cplusg 17141 |
. . . . . . . . . . . . . 14
class
+g |
26 | 7, 25 | cfv 6500 |
. . . . . . . . . . . . 13
class
(+gβπ) |
27 | 23, 24, 26 | co 7361 |
. . . . . . . . . . . 12
class (π(+gβπ)π) |
28 | 22, 27 | wceq 1542 |
. . . . . . . . . . 11
wff π = (π(+gβπ)π) |
29 | 16 | cv 1541 |
. . . . . . . . . . . . 13
class π₯ |
30 | 23, 29 | cfv 6500 |
. . . . . . . . . . . 12
class (π₯βπ) |
31 | 17 | cv 1541 |
. . . . . . . . . . . . 13
class π¦ |
32 | 24, 31 | cfv 6500 |
. . . . . . . . . . . 12
class (π¦βπ) |
33 | 6, 14 | cfv 6500 |
. . . . . . . . . . . 12
class
(.rβπ) |
34 | 30, 32, 33 | co 7361 |
. . . . . . . . . . 11
class ((π₯βπ)(.rβπ)(π¦βπ)) |
35 | | c0g 17329 |
. . . . . . . . . . . 12
class
0g |
36 | 6, 35 | cfv 6500 |
. . . . . . . . . . 11
class
(0gβπ) |
37 | 28, 34, 36 | cif 4490 |
. . . . . . . . . 10
class if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ)) |
38 | 21, 9, 37 | cmpt 5192 |
. . . . . . . . 9
class (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ))) |
39 | 19, 20, 9, 9, 38 | cmpo 7363 |
. . . . . . . 8
class (π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ)))) |
40 | | cgsu 17330 |
. . . . . . . 8
class
Ξ£g |
41 | 12, 39, 40 | co 7361 |
. . . . . . 7
class (π£ Ξ£g
(π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ))))) |
42 | 16, 17, 18, 18, 41 | cmpo 7363 |
. . . . . 6
class (π₯ β (Baseβπ£), π¦ β (Baseβπ£) β¦ (π£ Ξ£g (π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ)))))) |
43 | 15, 42 | cop 4596 |
. . . . 5
class
β¨(.rβndx), (π₯ β (Baseβπ£), π¦ β (Baseβπ£) β¦ (π£ Ξ£g (π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ))))))β© |
44 | | csts 17043 |
. . . . 5
class
sSet |
45 | 12, 43, 44 | co 7361 |
. . . 4
class (π£ sSet
β¨(.rβndx), (π₯ β (Baseβπ£), π¦ β (Baseβπ£) β¦ (π£ Ξ£g (π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ))))))β©) |
46 | 5, 11, 45 | csb 3859 |
. . 3
class
β¦(π
freeLMod (Baseβπ)) /
π£β¦(π£ sSet
β¨(.rβndx), (π₯ β (Baseβπ£), π¦ β (Baseβπ£) β¦ (π£ Ξ£g (π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ))))))β©) |
47 | 2, 3, 4, 4, 46 | cmpo 7363 |
. 2
class (π β V, π β V β¦ β¦(π freeLMod (Baseβπ)) / π£β¦(π£ sSet β¨(.rβndx), (π₯ β (Baseβπ£), π¦ β (Baseβπ£) β¦ (π£ Ξ£g (π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ))))))β©)) |
48 | 1, 47 | wceq 1542 |
1
wff MndRing =
(π β V, π β V β¦
β¦(π freeLMod
(Baseβπ)) / π£β¦(π£ sSet
β¨(.rβndx), (π₯ β (Baseβπ£), π¦ β (Baseβπ£) β¦ (π£ Ξ£g (π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ))))))β©)) |