Step | Hyp | Ref
| Expression |
1 | | cedring-rN 39220 |
. 2
class
EDRingR |
2 | | vk |
. . 3
setvar π |
3 | | cvv 3446 |
. . 3
class
V |
4 | | vw |
. . . 4
setvar π€ |
5 | 2 | cv 1541 |
. . . . 5
class π |
6 | | clh 38450 |
. . . . 5
class
LHyp |
7 | 5, 6 | cfv 6497 |
. . . 4
class
(LHypβπ) |
8 | | cnx 17066 |
. . . . . . 7
class
ndx |
9 | | cbs 17084 |
. . . . . . 7
class
Base |
10 | 8, 9 | cfv 6497 |
. . . . . 6
class
(Baseβndx) |
11 | 4 | cv 1541 |
. . . . . . 7
class π€ |
12 | | ctendo 39218 |
. . . . . . . 8
class
TEndo |
13 | 5, 12 | cfv 6497 |
. . . . . . 7
class
(TEndoβπ) |
14 | 11, 13 | cfv 6497 |
. . . . . 6
class
((TEndoβπ)βπ€) |
15 | 10, 14 | cop 4593 |
. . . . 5
class
β¨(Baseβndx), ((TEndoβπ)βπ€)β© |
16 | | cplusg 17134 |
. . . . . . 7
class
+g |
17 | 8, 16 | cfv 6497 |
. . . . . 6
class
(+gβndx) |
18 | | vs |
. . . . . . 7
setvar π |
19 | | vt |
. . . . . . 7
setvar π‘ |
20 | | vf |
. . . . . . . 8
setvar π |
21 | | cltrn 38567 |
. . . . . . . . . 10
class
LTrn |
22 | 5, 21 | cfv 6497 |
. . . . . . . . 9
class
(LTrnβπ) |
23 | 11, 22 | cfv 6497 |
. . . . . . . 8
class
((LTrnβπ)βπ€) |
24 | 20 | cv 1541 |
. . . . . . . . . 10
class π |
25 | 18 | cv 1541 |
. . . . . . . . . 10
class π |
26 | 24, 25 | cfv 6497 |
. . . . . . . . 9
class (π βπ) |
27 | 19 | cv 1541 |
. . . . . . . . . 10
class π‘ |
28 | 24, 27 | cfv 6497 |
. . . . . . . . 9
class (π‘βπ) |
29 | 26, 28 | ccom 5638 |
. . . . . . . 8
class ((π βπ) β (π‘βπ)) |
30 | 20, 23, 29 | cmpt 5189 |
. . . . . . 7
class (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))) |
31 | 18, 19, 14, 14, 30 | cmpo 7360 |
. . . . . 6
class (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ)))) |
32 | 17, 31 | cop 4593 |
. . . . 5
class
β¨(+gβndx), (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β© |
33 | | cmulr 17135 |
. . . . . . 7
class
.r |
34 | 8, 33 | cfv 6497 |
. . . . . 6
class
(.rβndx) |
35 | 27, 25 | ccom 5638 |
. . . . . . 7
class (π‘ β π ) |
36 | 18, 19, 14, 14, 35 | cmpo 7360 |
. . . . . 6
class (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π )) |
37 | 34, 36 | cop 4593 |
. . . . 5
class
β¨(.rβndx), (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β© |
38 | 15, 32, 37 | ctp 4591 |
. . . 4
class
{β¨(Baseβndx), ((TEndoβπ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β©} |
39 | 4, 7, 38 | cmpt 5189 |
. . 3
class (π€ β (LHypβπ) β¦
{β¨(Baseβndx), ((TEndoβπ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β©}) |
40 | 2, 3, 39 | cmpt 5189 |
. 2
class (π β V β¦ (π€ β (LHypβπ) β¦
{β¨(Baseβndx), ((TEndoβπ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β©})) |
41 | 1, 40 | wceq 1542 |
1
wff
EDRingR = (π β V β¦ (π€ β (LHypβπ) β¦ {β¨(Baseβndx),
((TEndoβπ)βπ€)β©, β¨(+gβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx),
(π β
((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β©})) |