Step | Hyp | Ref
| Expression |
1 | | mhpfval.h |
. 2
⊢ 𝐻 = (𝐼 mHomP 𝑅) |
2 | | mhpfval.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
3 | 2 | elexd 3451 |
. . 3
⊢ (𝜑 → 𝐼 ∈ V) |
4 | | mhpfval.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑊) |
5 | 4 | elexd 3451 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
6 | | oveq12 7286 |
. . . . . . . . 9
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPoly 𝑟) = (𝐼 mPoly 𝑅)) |
7 | | mhpfval.p |
. . . . . . . . 9
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPoly 𝑟) = 𝑃) |
9 | 8 | fveq2d 6780 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (Base‘(𝑖 mPoly 𝑟)) = (Base‘𝑃)) |
10 | | mhpfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑃) |
11 | 9, 10 | eqtr4di 2796 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (Base‘(𝑖 mPoly 𝑟)) = 𝐵) |
12 | | fveq2 6776 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
13 | | mhpfval.0 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑅) |
14 | 12, 13 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
15 | 14 | oveq2d 7293 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑓 supp (0g‘𝑟)) = (𝑓 supp 0 )) |
16 | 15 | adantl 482 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑓 supp (0g‘𝑟)) = (𝑓 supp 0 )) |
17 | | oveq2 7285 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (ℕ0
↑m 𝑖) =
(ℕ0 ↑m 𝐼)) |
18 | 17 | rabeqdv 3418 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) |
19 | | mhpfval.d |
. . . . . . . . . 10
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} |
20 | 18, 19 | eqtr4di 2796 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷) |
21 | 20 | rabeqdv 3418 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛} = {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}) |
22 | 21 | adantr 481 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛} = {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}) |
23 | 16, 22 | sseq12d 3955 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → ((𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛} ↔ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛})) |
24 | 11, 23 | rabeqbidv 3419 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛}} = {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}}) |
25 | 24 | mpteq2dv 5178 |
. . . 4
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛}}) = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}})) |
26 | | df-mhp 21321 |
. . . 4
⊢ mHomP =
(𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0
↦ {𝑓 ∈
(Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛}})) |
27 | | nn0ex 12237 |
. . . . 5
⊢
ℕ0 ∈ V |
28 | 27 | mptex 7101 |
. . . 4
⊢ (𝑛 ∈ ℕ0
↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}}) ∈ V |
29 | 25, 26, 28 | ovmpoa 7428 |
. . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V) → (𝐼 mHomP 𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}})) |
30 | 3, 5, 29 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐼 mHomP 𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}})) |
31 | 1, 30 | eqtrid 2790 |
1
⊢ (𝜑 → 𝐻 = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}})) |