Detailed syntax breakdown of Definition df-evls
Step | Hyp | Ref
| Expression |
1 | | ces 21280 |
. 2
class
evalSub |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vs |
. . 3
setvar 𝑠 |
4 | | cvv 3432 |
. . 3
class
V |
5 | | ccrg 19784 |
. . 3
class
CRing |
6 | | vb |
. . . 4
setvar 𝑏 |
7 | 3 | cv 1538 |
. . . . 5
class 𝑠 |
8 | | cbs 16912 |
. . . . 5
class
Base |
9 | 7, 8 | cfv 6433 |
. . . 4
class
(Base‘𝑠) |
10 | | vr |
. . . . 5
setvar 𝑟 |
11 | | csubrg 20020 |
. . . . . 6
class
SubRing |
12 | 7, 11 | cfv 6433 |
. . . . 5
class
(SubRing‘𝑠) |
13 | | vw |
. . . . . 6
setvar 𝑤 |
14 | 2 | cv 1538 |
. . . . . . 7
class 𝑖 |
15 | 10 | cv 1538 |
. . . . . . . 8
class 𝑟 |
16 | | cress 16941 |
. . . . . . . 8
class
↾s |
17 | 7, 15, 16 | co 7275 |
. . . . . . 7
class (𝑠 ↾s 𝑟) |
18 | | cmpl 21109 |
. . . . . . 7
class
mPoly |
19 | 14, 17, 18 | co 7275 |
. . . . . 6
class (𝑖 mPoly (𝑠 ↾s 𝑟)) |
20 | | vf |
. . . . . . . . . . 11
setvar 𝑓 |
21 | 20 | cv 1538 |
. . . . . . . . . 10
class 𝑓 |
22 | 13 | cv 1538 |
. . . . . . . . . . 11
class 𝑤 |
23 | | cascl 21059 |
. . . . . . . . . . 11
class
algSc |
24 | 22, 23 | cfv 6433 |
. . . . . . . . . 10
class
(algSc‘𝑤) |
25 | 21, 24 | ccom 5593 |
. . . . . . . . 9
class (𝑓 ∘ (algSc‘𝑤)) |
26 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
27 | 6 | cv 1538 |
. . . . . . . . . . . 12
class 𝑏 |
28 | | cmap 8615 |
. . . . . . . . . . . 12
class
↑m |
29 | 27, 14, 28 | co 7275 |
. . . . . . . . . . 11
class (𝑏 ↑m 𝑖) |
30 | 26 | cv 1538 |
. . . . . . . . . . . 12
class 𝑥 |
31 | 30 | csn 4561 |
. . . . . . . . . . 11
class {𝑥} |
32 | 29, 31 | cxp 5587 |
. . . . . . . . . 10
class ((𝑏 ↑m 𝑖) × {𝑥}) |
33 | 26, 15, 32 | cmpt 5157 |
. . . . . . . . 9
class (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) |
34 | 25, 33 | wceq 1539 |
. . . . . . . 8
wff (𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) |
35 | | cmvr 21108 |
. . . . . . . . . . 11
class
mVar |
36 | 14, 17, 35 | co 7275 |
. . . . . . . . . 10
class (𝑖 mVar (𝑠 ↾s 𝑟)) |
37 | 21, 36 | ccom 5593 |
. . . . . . . . 9
class (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) |
38 | | vg |
. . . . . . . . . . 11
setvar 𝑔 |
39 | 38 | cv 1538 |
. . . . . . . . . . . 12
class 𝑔 |
40 | 30, 39 | cfv 6433 |
. . . . . . . . . . 11
class (𝑔‘𝑥) |
41 | 38, 29, 40 | cmpt 5157 |
. . . . . . . . . 10
class (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)) |
42 | 26, 14, 41 | cmpt 5157 |
. . . . . . . . 9
class (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) |
43 | 37, 42 | wceq 1539 |
. . . . . . . 8
wff (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) |
44 | 34, 43 | wa 396 |
. . . . . . 7
wff ((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))) |
45 | | cpws 17157 |
. . . . . . . . 9
class
↑s |
46 | 7, 29, 45 | co 7275 |
. . . . . . . 8
class (𝑠 ↑s
(𝑏 ↑m 𝑖)) |
47 | | crh 19956 |
. . . . . . . 8
class
RingHom |
48 | 22, 46, 47 | co 7275 |
. . . . . . 7
class (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖))) |
49 | 44, 20, 48 | crio 7231 |
. . . . . 6
class
(℩𝑓
∈ (𝑤 RingHom (𝑠 ↑s
(𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) |
50 | 13, 19, 49 | csb 3832 |
. . . . 5
class
⦋(𝑖
mPoly (𝑠
↾s 𝑟)) /
𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) |
51 | 10, 12, 50 | cmpt 5157 |
. . . 4
class (𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))) |
52 | 6, 9, 51 | csb 3832 |
. . 3
class
⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))) |
53 | 2, 3, 4, 5, 52 | cmpo 7277 |
. 2
class (𝑖 ∈ V, 𝑠 ∈ CRing ↦
⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))))) |
54 | 1, 53 | wceq 1539 |
1
wff evalSub =
(𝑖 ∈ V, 𝑠 ∈ CRing ↦
⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))))) |