| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mhpfval.h | . 2
⊢ 𝐻 = (𝐼 mHomP 𝑅) | 
| 2 |  | mhpfval.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 3 | 2 | elexd 3504 | . . 3
⊢ (𝜑 → 𝐼 ∈ V) | 
| 4 |  | mhpfval.r | . . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑊) | 
| 5 | 4 | elexd 3504 | . . 3
⊢ (𝜑 → 𝑅 ∈ V) | 
| 6 |  | oveq12 7440 | . . . . . . . . 9
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPoly 𝑟) = (𝐼 mPoly 𝑅)) | 
| 7 |  | mhpfval.p | . . . . . . . . 9
⊢ 𝑃 = (𝐼 mPoly 𝑅) | 
| 8 | 6, 7 | eqtr4di 2795 | . . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑖 mPoly 𝑟) = 𝑃) | 
| 9 | 8 | fveq2d 6910 | . . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (Base‘(𝑖 mPoly 𝑟)) = (Base‘𝑃)) | 
| 10 |  | mhpfval.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑃) | 
| 11 | 9, 10 | eqtr4di 2795 | . . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (Base‘(𝑖 mPoly 𝑟)) = 𝐵) | 
| 12 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) | 
| 13 |  | mhpfval.0 | . . . . . . . . . 10
⊢  0 =
(0g‘𝑅) | 
| 14 | 12, 13 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) | 
| 15 | 14 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑓 supp (0g‘𝑟)) = (𝑓 supp 0 )) | 
| 16 | 15 | adantl 481 | . . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑓 supp (0g‘𝑟)) = (𝑓 supp 0 )) | 
| 17 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (ℕ0
↑m 𝑖) =
(ℕ0 ↑m 𝐼)) | 
| 18 | 17 | rabeqdv 3452 | . . . . . . . . . 10
⊢ (𝑖 = 𝐼 → {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈
Fin}) | 
| 19 |  | mhpfval.d | . . . . . . . . . 10
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑m 𝐼)
∣ (◡ℎ “ ℕ) ∈ Fin} | 
| 20 | 18, 19 | eqtr4di 2795 | . . . . . . . . 9
⊢ (𝑖 = 𝐼 → {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷) | 
| 21 | 20 | rabeqdv 3452 | . . . . . . . 8
⊢ (𝑖 = 𝐼 → {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛} = {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}) | 
| 22 | 21 | adantr 480 | . . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛} = {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}) | 
| 23 | 16, 22 | sseq12d 4017 | . . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → ((𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛} ↔ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛})) | 
| 24 | 11, 23 | rabeqbidv 3455 | . . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛}} = {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}}) | 
| 25 | 24 | mpteq2dv 5244 | . . . 4
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ (Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛}}) = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}})) | 
| 26 |  | df-mhp 22140 | . . . 4
⊢  mHomP =
(𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑛 ∈ ℕ0
↦ {𝑓 ∈
(Base‘(𝑖 mPoly 𝑟)) ∣ (𝑓 supp (0g‘𝑟)) ⊆ {𝑔 ∈ {ℎ ∈ (ℕ0
↑m 𝑖)
∣ (◡ℎ “ ℕ) ∈ Fin} ∣
((ℂfld ↾s ℕ0)
Σg 𝑔) = 𝑛}})) | 
| 27 |  | nn0ex 12532 | . . . . 5
⊢
ℕ0 ∈ V | 
| 28 | 27 | mptex 7243 | . . . 4
⊢ (𝑛 ∈ ℕ0
↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}}) ∈ V | 
| 29 | 25, 26, 28 | ovmpoa 7588 | . . 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 2789 | 1
⊢ (𝜑 → 𝐻 = (𝑛 ∈ ℕ0 ↦ {𝑓 ∈ 𝐵 ∣ (𝑓 supp 0 ) ⊆ {𝑔 ∈ 𝐷 ∣ ((ℂfld
↾s ℕ0) Σg 𝑔) = 𝑛}})) |