Step | Hyp | Ref
| Expression |
1 | | mplval.p |
. 2
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
2 | | ovex 6577 |
. . . . . 6
⊢ (𝑖 mPwSer 𝑟) ∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPwSer 𝑟) ∈ V) |
4 | | id 22 |
. . . . . . . 8
⊢ (𝑠 = (𝑖 mPwSer 𝑟) → 𝑠 = (𝑖 mPwSer 𝑟)) |
5 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPwSer 𝑟) = (𝐼 mPwSer 𝑅)) |
6 | 4, 5 | sylan9eqr 2666 |
. . . . . . 7
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → 𝑠 = (𝐼 mPwSer 𝑅)) |
7 | | mplval.s |
. . . . . . 7
⊢ 𝑆 = (𝐼 mPwSer 𝑅) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . 6
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → 𝑠 = 𝑆) |
9 | 8 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → (Base‘𝑠) = (Base‘𝑆)) |
10 | | mplval.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑆) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . . 8
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → (Base‘𝑠) = 𝐵) |
12 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → 𝑟 = 𝑅) |
13 | 12 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → (0g‘𝑟) = (0g‘𝑅)) |
14 | | mplval.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑅) |
15 | 13, 14 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → (0g‘𝑟) = 0 ) |
16 | 15 | breq2d 4595 |
. . . . . . . 8
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → (𝑓 finSupp (0g‘𝑟) ↔ 𝑓 finSupp 0 )) |
17 | 11, 16 | rabeqbidv 3168 |
. . . . . . 7
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → {𝑓 ∈ (Base‘𝑠) ∣ 𝑓 finSupp (0g‘𝑟)} = {𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }) |
18 | | mplval.u |
. . . . . . 7
⊢ 𝑈 = {𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } |
19 | 17, 18 | syl6eqr 2662 |
. . . . . 6
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → {𝑓 ∈ (Base‘𝑠) ∣ 𝑓 finSupp (0g‘𝑟)} = 𝑈) |
20 | 8, 19 | oveq12d 6567 |
. . . . 5
⊢ (((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) ∧ 𝑠 = (𝑖 mPwSer 𝑟)) → (𝑠 ↾s {𝑓 ∈ (Base‘𝑠) ∣ 𝑓 finSupp (0g‘𝑟)}) = (𝑆 ↾s 𝑈)) |
21 | 3, 20 | csbied 3526 |
. . . 4
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → ⦋(𝑖 mPwSer 𝑟) / 𝑠⦌(𝑠 ↾s {𝑓 ∈ (Base‘𝑠) ∣ 𝑓 finSupp (0g‘𝑟)}) = (𝑆 ↾s 𝑈)) |
22 | | df-mpl 19179 |
. . . 4
⊢ mPoly =
(𝑖 ∈ V, 𝑟 ∈ V ↦
⦋(𝑖 mPwSer
𝑟) / 𝑠⦌(𝑠 ↾s {𝑓 ∈ (Base‘𝑠) ∣ 𝑓 finSupp (0g‘𝑟)})) |
23 | | ovex 6577 |
. . . 4
⊢ (𝑆 ↾s 𝑈) ∈ V |
24 | 21, 22, 23 | ovmpt2a 6689 |
. . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPoly 𝑅) = (𝑆 ↾s 𝑈)) |
25 | | reldmmpl 19248 |
. . . . . 6
⊢ Rel dom
mPoly |
26 | 25 | ovprc 6581 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPoly 𝑅) = ∅) |
27 | | ress0 15761 |
. . . . 5
⊢ (∅
↾s 𝑈) =
∅ |
28 | 26, 27 | syl6eqr 2662 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPoly 𝑅) = (∅ ↾s 𝑈)) |
29 | | reldmpsr 19182 |
. . . . . . 7
⊢ Rel dom
mPwSer |
30 | 29 | ovprc 6581 |
. . . . . 6
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPwSer 𝑅) = ∅) |
31 | 7, 30 | syl5eq 2656 |
. . . . 5
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → 𝑆 = ∅) |
32 | 31 | oveq1d 6564 |
. . . 4
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝑆 ↾s 𝑈) = (∅ ↾s
𝑈)) |
33 | 28, 32 | eqtr4d 2647 |
. . 3
⊢ (¬
(𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mPoly 𝑅) = (𝑆 ↾s 𝑈)) |
34 | 24, 33 | pm2.61i 175 |
. 2
⊢ (𝐼 mPoly 𝑅) = (𝑆 ↾s 𝑈) |
35 | 1, 34 | eqtri 2632 |
1
⊢ 𝑃 = (𝑆 ↾s 𝑈) |