Step |
Hyp |
Ref |
Expression |
0 |
|
cmpl |
⊢ mPoly |
1 |
|
vi |
⊢ 𝑖 |
2 |
|
cvv |
⊢ V |
3 |
|
vr |
⊢ 𝑟 |
4 |
1
|
cv |
⊢ 𝑖 |
5 |
|
cmps |
⊢ mPwSer |
6 |
3
|
cv |
⊢ 𝑟 |
7 |
4 6 5
|
co |
⊢ ( 𝑖 mPwSer 𝑟 ) |
8 |
|
vw |
⊢ 𝑤 |
9 |
8
|
cv |
⊢ 𝑤 |
10 |
|
cress |
⊢ ↾s |
11 |
|
vf |
⊢ 𝑓 |
12 |
|
cbs |
⊢ Base |
13 |
9 12
|
cfv |
⊢ ( Base ‘ 𝑤 ) |
14 |
11
|
cv |
⊢ 𝑓 |
15 |
|
cfsupp |
⊢ finSupp |
16 |
|
c0g |
⊢ 0g |
17 |
6 16
|
cfv |
⊢ ( 0g ‘ 𝑟 ) |
18 |
14 17 15
|
wbr |
⊢ 𝑓 finSupp ( 0g ‘ 𝑟 ) |
19 |
18 11 13
|
crab |
⊢ { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } |
20 |
9 19 10
|
co |
⊢ ( 𝑤 ↾s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } ) |
21 |
8 7 20
|
csb |
⊢ ⦋ ( 𝑖 mPwSer 𝑟 ) / 𝑤 ⦌ ( 𝑤 ↾s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } ) |
22 |
1 3 2 2 21
|
cmpo |
⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ ( 𝑖 mPwSer 𝑟 ) / 𝑤 ⦌ ( 𝑤 ↾s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } ) ) |
23 |
0 22
|
wceq |
⊢ mPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ⦋ ( 𝑖 mPwSer 𝑟 ) / 𝑤 ⦌ ( 𝑤 ↾s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑟 ) } ) ) |