Step | Hyp | Ref
| Expression |
1 | | ces 21632 |
. 2
class
evalSub |
2 | | vi |
. . 3
setvar π |
3 | | vs |
. . 3
setvar π |
4 | | cvv 3474 |
. . 3
class
V |
5 | | ccrg 20056 |
. . 3
class
CRing |
6 | | vb |
. . . 4
setvar π |
7 | 3 | cv 1540 |
. . . . 5
class π |
8 | | cbs 17143 |
. . . . 5
class
Base |
9 | 7, 8 | cfv 6543 |
. . . 4
class
(Baseβπ ) |
10 | | vr |
. . . . 5
setvar π |
11 | | csubrg 20314 |
. . . . . 6
class
SubRing |
12 | 7, 11 | cfv 6543 |
. . . . 5
class
(SubRingβπ ) |
13 | | vw |
. . . . . 6
setvar π€ |
14 | 2 | cv 1540 |
. . . . . . 7
class π |
15 | 10 | cv 1540 |
. . . . . . . 8
class π |
16 | | cress 17172 |
. . . . . . . 8
class
βΎs |
17 | 7, 15, 16 | co 7408 |
. . . . . . 7
class (π βΎs π) |
18 | | cmpl 21458 |
. . . . . . 7
class
mPoly |
19 | 14, 17, 18 | co 7408 |
. . . . . 6
class (π mPoly (π βΎs π)) |
20 | | vf |
. . . . . . . . . . 11
setvar π |
21 | 20 | cv 1540 |
. . . . . . . . . 10
class π |
22 | 13 | cv 1540 |
. . . . . . . . . . 11
class π€ |
23 | | cascl 21406 |
. . . . . . . . . . 11
class
algSc |
24 | 22, 23 | cfv 6543 |
. . . . . . . . . 10
class
(algScβπ€) |
25 | 21, 24 | ccom 5680 |
. . . . . . . . 9
class (π β (algScβπ€)) |
26 | | vx |
. . . . . . . . . 10
setvar π₯ |
27 | 6 | cv 1540 |
. . . . . . . . . . . 12
class π |
28 | | cmap 8819 |
. . . . . . . . . . . 12
class
βm |
29 | 27, 14, 28 | co 7408 |
. . . . . . . . . . 11
class (π βm π) |
30 | 26 | cv 1540 |
. . . . . . . . . . . 12
class π₯ |
31 | 30 | csn 4628 |
. . . . . . . . . . 11
class {π₯} |
32 | 29, 31 | cxp 5674 |
. . . . . . . . . 10
class ((π βm π) Γ {π₯}) |
33 | 26, 15, 32 | cmpt 5231 |
. . . . . . . . 9
class (π₯ β π β¦ ((π βm π) Γ {π₯})) |
34 | 25, 33 | wceq 1541 |
. . . . . . . 8
wff (π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) |
35 | | cmvr 21457 |
. . . . . . . . . . 11
class
mVar |
36 | 14, 17, 35 | co 7408 |
. . . . . . . . . 10
class (π mVar (π βΎs π)) |
37 | 21, 36 | ccom 5680 |
. . . . . . . . 9
class (π β (π mVar (π βΎs π))) |
38 | | vg |
. . . . . . . . . . 11
setvar π |
39 | 38 | cv 1540 |
. . . . . . . . . . . 12
class π |
40 | 30, 39 | cfv 6543 |
. . . . . . . . . . 11
class (πβπ₯) |
41 | 38, 29, 40 | cmpt 5231 |
. . . . . . . . . 10
class (π β (π βm π) β¦ (πβπ₯)) |
42 | 26, 14, 41 | cmpt 5231 |
. . . . . . . . 9
class (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))) |
43 | 37, 42 | wceq 1541 |
. . . . . . . 8
wff (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))) |
44 | 34, 43 | wa 396 |
. . . . . . 7
wff ((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))) |
45 | | cpws 17391 |
. . . . . . . . 9
class
βs |
46 | 7, 29, 45 | co 7408 |
. . . . . . . 8
class (π βs
(π βm π)) |
47 | | crh 20247 |
. . . . . . . 8
class
RingHom |
48 | 22, 46, 47 | co 7408 |
. . . . . . 7
class (π€ RingHom (π βs (π βm π))) |
49 | 44, 20, 48 | crio 7363 |
. . . . . 6
class
(β©π
β (π€ RingHom (π βs
(π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) |
50 | 13, 19, 49 | csb 3893 |
. . . . 5
class
β¦(π
mPoly (π
βΎs π)) /
π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))) |
51 | 10, 12, 50 | cmpt 5231 |
. . . 4
class (π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) |
52 | 6, 9, 51 | csb 3893 |
. . 3
class
β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯)))))) |
53 | 2, 3, 4, 5, 52 | cmpo 7410 |
. 2
class (π β V, π β CRing β¦
β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))))) |
54 | 1, 53 | wceq 1541 |
1
wff evalSub =
(π β V, π β CRing β¦
β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))))) |