| Step | Hyp | Ref
| Expression |
| 1 | | gsumbagdiag.d |
. . . 4
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 2 | | gsumbagdiag.s |
. . . 4
⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} |
| 3 | | gsumbagdiag.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐷) |
| 4 | | gsumbagdiag.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
| 5 | | gsumbagdiag.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) |
| 6 | 1, 2, 3 | gsumbagdiaglem 21950 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) |
| 7 | | gsumbagdiag.x |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑋 ∈ 𝐵) |
| 8 | 7 | anassrs 467 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑋 ∈ 𝐵) |
| 9 | 8 | fmpttd 7135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵) |
| 10 | 2 | ssrab3 4082 |
. . . . . . . . . . . 12
⊢ 𝑆 ⊆ 𝐷 |
| 11 | 1, 2 | psrbagconcl 21947 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆) |
| 12 | 3, 11 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝑆) |
| 13 | 10, 12 | sselid 3981 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘f − 𝑗) ∈ 𝐷) |
| 14 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} |
| 15 | 1, 14 | psrbagconf1o 21949 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘f −
𝑗) ∈ 𝐷 → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 16 | 13, 15 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 17 | | f1of 6848 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 19 | 9, 18 | fcod 6761 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵) |
| 20 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐹 ∈ 𝐷) |
| 21 | 20 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 ∈ 𝐷) |
| 22 | 1 | psrbagf 21938 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ0) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹:𝐼⟶ℕ0) |
| 24 | 23 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈
ℕ0) |
| 25 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝑆) |
| 26 | 10, 25 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 ∈ 𝐷) |
| 27 | 1 | psrbagf 21938 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ 𝐷 → 𝑗:𝐼⟶ℕ0) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗:𝐼⟶ℕ0) |
| 29 | 28 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑗‘𝑧) ∈
ℕ0) |
| 30 | | ssrab2 4080 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ⊆ 𝐷 |
| 31 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 32 | 30, 31 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 ∈ 𝐷) |
| 33 | 1 | psrbagf 21938 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ 𝐷 → 𝑚:𝐼⟶ℕ0) |
| 34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚:𝐼⟶ℕ0) |
| 35 | 34 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑚‘𝑧) ∈
ℕ0) |
| 36 | | nn0cn 12536 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℂ) |
| 37 | | nn0cn 12536 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗‘𝑧) ∈ ℕ0 → (𝑗‘𝑧) ∈ ℂ) |
| 38 | | nn0cn 12536 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚‘𝑧) ∈ ℕ0 → (𝑚‘𝑧) ∈ ℂ) |
| 39 | | sub32 11543 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝑗‘𝑧) ∈ ℂ ∧ (𝑚‘𝑧) ∈ ℂ) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))) |
| 40 | 36, 37, 38, 39 | syl3an 1161 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑧) ∈ ℕ0 ∧ (𝑗‘𝑧) ∈ ℕ0 ∧ (𝑚‘𝑧) ∈ ℕ0) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))) |
| 41 | 24, 29, 35, 40 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))) |
| 42 | 41 | mpteq2dva 5242 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))) |
| 43 | 34 | ffnd 6737 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 Fn 𝐼) |
| 44 | 31, 43 | fndmexd 7926 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐼 ∈ V) |
| 45 | | ovexd 7466 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑗‘𝑧)) ∈ V) |
| 46 | 23 | feqmptd 6977 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝐹 = (𝑧 ∈ 𝐼 ↦ (𝐹‘𝑧))) |
| 47 | 28 | feqmptd 6977 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑗 = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧))) |
| 48 | 44, 24, 29, 46, 47 | offval2 7717 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑗‘𝑧)))) |
| 49 | 34 | feqmptd 6977 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → 𝑚 = (𝑧 ∈ 𝐼 ↦ (𝑚‘𝑧))) |
| 50 | 44, 45, 35, 48, 49 | offval2 7717 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f −
𝑚) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)))) |
| 51 | | ovexd 7466 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑚‘𝑧)) ∈ V) |
| 52 | 44, 24, 35, 46, 49 | offval2 7717 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → (𝐹 ∘f − 𝑚) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑚‘𝑧)))) |
| 53 | 44, 51, 29, 52, 47 | offval2 7717 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f −
𝑗) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))) |
| 54 | 42, 50, 53 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f −
𝑚) = ((𝐹 ∘f − 𝑚) ∘f −
𝑗)) |
| 55 | 1, 14 | psrbagconcl 21947 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∘f −
𝑗) ∈ 𝐷 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f −
𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 56 | 13, 55 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑗) ∘f −
𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 57 | 54, 56 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) → ((𝐹 ∘f − 𝑚) ∘f −
𝑗) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 58 | 54 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚)) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑚) ∘f −
𝑗))) |
| 59 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛𝑋 |
| 60 | | nfcsb1v 3923 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝑋 |
| 61 | | csbeq1a 3913 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → 𝑋 = ⦋𝑛 / 𝑘⦌𝑋) |
| 62 | 59, 60, 61 | cbvmpt 5253 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋) |
| 63 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ⦋𝑛 / 𝑘⦌𝑋)) |
| 64 | | csbeq1 3902 |
. . . . . . . . . 10
⊢ (𝑛 = ((𝐹 ∘f − 𝑚) ∘f −
𝑗) →
⦋𝑛 / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f −
𝑗) / 𝑘⦌𝑋) |
| 65 | 57, 58, 63, 64 | fmptco 7149 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚))) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) |
| 66 | 65 | feq1d 6720 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵)) |
| 67 | 19, 66 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}⟶𝐵) |
| 68 | 67 | fvmptelcdm 7133 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) →
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
| 69 | 68 | anasss 466 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) →
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
| 70 | 6, 69 | syldan 591 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) →
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
| 71 | 1, 2, 3, 4, 5, 70 | gsumbagdiag 21951 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) |
| 72 | | eqid 2737 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 73 | 1 | psrbaglefi 21946 |
. . . . . 6
⊢ (𝐹 ∈ 𝐷 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin) |
| 74 | 3, 73 | syl 17 |
. . . . 5
⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ Fin) |
| 75 | 2, 74 | eqeltrid 2845 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Fin) |
| 76 | 1, 2 | psrbagconcl 21947 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆) |
| 77 | 3, 76 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝑆) |
| 78 | 10, 77 | sselid 3981 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘f − 𝑚) ∈ 𝐷) |
| 79 | 1 | psrbaglefi 21946 |
. . . . 5
⊢ ((𝐹 ∘f −
𝑚) ∈ 𝐷 → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin) |
| 80 | 78, 79 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin) |
| 81 | | xpfi 9358 |
. . . . 5
⊢ ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin) |
| 82 | 75, 75, 81 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑆 × 𝑆) ∈ Fin) |
| 83 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚 ∈ 𝑆) |
| 84 | 6 | simpld 494 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑗 ∈ 𝑆) |
| 85 | | brxp 5734 |
. . . . . . 7
⊢ (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ 𝑆)) |
| 86 | 83, 84, 85 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗) |
| 87 | 86 | pm2.24d 151 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (¬ 𝑚(𝑆 × 𝑆)𝑗 → ⦋((𝐹 ∘f − 𝑚) ∘f −
𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))) |
| 88 | 87 | impr 454 |
. . . 4
⊢ ((𝜑 ∧ ((𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) ∧ ¬ 𝑚(𝑆 × 𝑆)𝑗)) → ⦋((𝐹 ∘f − 𝑚) ∘f −
𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)) |
| 89 | 4, 72, 5, 75, 80, 70, 82, 88 | gsum2d2 19992 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))) |
| 90 | 1 | psrbaglefi 21946 |
. . . . 5
⊢ ((𝐹 ∘f −
𝑗) ∈ 𝐷 → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin) |
| 91 | 13, 90 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin) |
| 92 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗 ∈ 𝑆) |
| 93 | 1, 2, 3 | gsumbagdiaglem 21950 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) |
| 94 | 93 | simpld 494 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑚 ∈ 𝑆) |
| 95 | | brxp 5734 |
. . . . . . 7
⊢ (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ 𝑆)) |
| 96 | 92, 94, 95 | sylanbrc 583 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚) |
| 97 | 96 | pm2.24d 151 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (¬ 𝑗(𝑆 × 𝑆)𝑚 → ⦋((𝐹 ∘f − 𝑚) ∘f −
𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))) |
| 98 | 97 | impr 454 |
. . . 4
⊢ ((𝜑 ∧ ((𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) ∧ ¬ 𝑗(𝑆 × 𝑆)𝑚)) → ⦋((𝐹 ∘f − 𝑚) ∘f −
𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)) |
| 99 | 4, 72, 5, 75, 91, 69, 82, 98 | gsum2d2 19992 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))) |
| 100 | 71, 89, 99 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))) |
| 101 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐺 ∈ CMnd) |
| 102 | 70 | anassrs 467 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ 𝑆) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) →
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
| 103 | 102 | fmpttd 7135 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}⟶𝐵) |
| 104 | | ovex 7464 |
. . . . . . . . . . . 12
⊢
(ℕ0 ↑m 𝐼) ∈ V |
| 105 | 1, 104 | rabex2 5341 |
. . . . . . . . . . 11
⊢ 𝐷 ∈ V |
| 106 | 105 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐷 ∈ V) |
| 107 | | rabexg 5337 |
. . . . . . . . . 10
⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V) |
| 108 | | mptexg 7241 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ V → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V) |
| 109 | 106, 107,
108 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V) |
| 110 | | funmpt 6604 |
. . . . . . . . . 10
⊢ Fun
(𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) |
| 111 | 110 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) |
| 112 | | fvexd 6921 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (0g‘𝐺) ∈ V) |
| 113 | | suppssdm 8202 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) |
| 114 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) |
| 115 | 114 | dmmptss 6261 |
. . . . . . . . . . 11
⊢ dom
(𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} |
| 116 | 113, 115 | sstri 3993 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} |
| 117 | 116 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) |
| 118 | | suppssfifsupp 9420 |
. . . . . . . . 9
⊢ ((((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∈ V ∧ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) ∧ (0g‘𝐺) ∈ V) ∧ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ∈ Fin ∧ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)})) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) finSupp (0g‘𝐺)) |
| 119 | 109, 111,
112, 80, 117, 118 | syl32anc 1380 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋) finSupp (0g‘𝐺)) |
| 120 | 4, 72, 101, 80, 103, 119 | gsumcl 19933 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) ∈ 𝐵) |
| 121 | 120 | fmpttd 7135 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵) |
| 122 | 1, 2 | psrbagconf1o 21949 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐷 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆) |
| 123 | 3, 122 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆) |
| 124 | | f1ocnv 6860 |
. . . . . . 7
⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆) |
| 125 | | f1of 6848 |
. . . . . . 7
⊢ (◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆) |
| 126 | 123, 124,
125 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆⟶𝑆) |
| 127 | 121, 126 | fcod 6761 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵) |
| 128 | | coass 6285 |
. . . . . . . 8
⊢ (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) |
| 129 | | f1ococnv2 6875 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)):𝑆–1-1-onto→𝑆 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆)) |
| 130 | 123, 129 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ( I ↾ 𝑆)) |
| 131 | 130 | coeq2d 5873 |
. . . . . . . 8
⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆))) |
| 132 | 128, 131 | eqtrid 2789 |
. . . . . . 7
⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆))) |
| 133 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)) = (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) |
| 134 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) |
| 135 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑥 ∘r ≤ 𝑛 ↔ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚))) |
| 136 | 135 | rabbidv 3444 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝐹 ∘f − 𝑚) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)}) |
| 137 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∘f −
𝑗) ∈
V |
| 138 | | psrass1lem.y |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 ∘f − 𝑗) → 𝑋 = 𝑌) |
| 139 | 137, 138 | csbie 3934 |
. . . . . . . . . . . 12
⊢
⦋(𝑛
∘f − 𝑗) / 𝑘⦌𝑋 = 𝑌 |
| 140 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑛 ∘f − 𝑗) = ((𝐹 ∘f − 𝑚) ∘f −
𝑗)) |
| 141 | 140 | csbeq1d 3903 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝐹 ∘f − 𝑚) → ⦋(𝑛 ∘f −
𝑗) / 𝑘⦌𝑋 = ⦋((𝐹 ∘f − 𝑚) ∘f −
𝑗) / 𝑘⦌𝑋) |
| 142 | 139, 141 | eqtr3id 2791 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝐹 ∘f − 𝑚) → 𝑌 = ⦋((𝐹 ∘f − 𝑚) ∘f −
𝑗) / 𝑘⦌𝑋) |
| 143 | 136, 142 | mpteq12dv 5233 |
. . . . . . . . . 10
⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)) |
| 144 | 143 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑛 = (𝐹 ∘f − 𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) |
| 145 | 77, 133, 134, 144 | fmptco 7149 |
. . . . . . . 8
⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))) |
| 146 | 145 | coeq1d 5872 |
. . . . . . 7
⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) |
| 147 | | coires1 6284 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) |
| 148 | | ssid 4006 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ 𝑆 |
| 149 | | resmpt 6055 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑆 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) |
| 150 | 148, 149 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) |
| 151 | 147, 150 | eqtri 2765 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) |
| 152 | 151 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) |
| 153 | 132, 146,
152 | 3eqtr3d 2785 |
. . . . . 6
⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) |
| 154 | 153 | feq1d 6720 |
. . . . 5
⊢ (𝜑 → (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))):𝑆⟶𝐵 ↔ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵)) |
| 155 | 127, 154 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵) |
| 156 | | rabexg 5337 |
. . . . . . . 8
⊢ (𝐷 ∈ V → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V) |
| 157 | 105, 156 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} ∈ V) |
| 158 | 2, 157 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ V) |
| 159 | 158 | mptexd 7244 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∈ V) |
| 160 | | funmpt 6604 |
. . . . . 6
⊢ Fun
(𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) |
| 161 | 160 | a1i 11 |
. . . . 5
⊢ (𝜑 → Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) |
| 162 | | fvexd 6921 |
. . . . 5
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
| 163 | | suppssdm 8202 |
. . . . . . 7
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) |
| 164 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) |
| 165 | 164 | dmmptss 6261 |
. . . . . . 7
⊢ dom
(𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ⊆ 𝑆 |
| 166 | 163, 165 | sstri 3993 |
. . . . . 6
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆 |
| 167 | 166 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆) |
| 168 | | suppssfifsupp 9420 |
. . . . 5
⊢ ((((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∈ V ∧ Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∧ (0g‘𝐺) ∈ V) ∧ (𝑆 ∈ Fin ∧ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆)) → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺)) |
| 169 | 159, 161,
162, 75, 167, 168 | syl32anc 1380 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺)) |
| 170 | 4, 72, 5, 75, 155, 169, 123 | gsumf1o 19934 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚))))) |
| 171 | 145 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑚)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))) |
| 172 | 170, 171 | eqtrd 2777 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑚)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))) |
| 173 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺 ∈ CMnd) |
| 174 | 105 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐷 ∈ V) |
| 175 | | rabexg 5337 |
. . . . . . . 8
⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V) |
| 176 | | mptexg 7241 |
. . . . . . . 8
⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ V → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V) |
| 177 | 174, 175,
176 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V) |
| 178 | | funmpt 6604 |
. . . . . . . 8
⊢ Fun
(𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) |
| 179 | 178 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) |
| 180 | | fvexd 6921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (0g‘𝐺) ∈ V) |
| 181 | | suppssdm 8202 |
. . . . . . . . 9
⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ dom (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) |
| 182 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) |
| 183 | 182 | dmmptss 6261 |
. . . . . . . . 9
⊢ dom
(𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} |
| 184 | 181, 183 | sstri 3993 |
. . . . . . . 8
⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} |
| 185 | 184 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)}) |
| 186 | | suppssfifsupp 9420 |
. . . . . . 7
⊢ ((((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∈ V ∧ Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∧ (0g‘𝐺) ∈ V) ∧ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ∈ Fin ∧ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)})) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) finSupp (0g‘𝐺)) |
| 187 | 177, 179,
180, 91, 185, 186 | syl32anc 1380 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) finSupp (0g‘𝐺)) |
| 188 | 4, 72, 173, 91, 9, 187, 16 | gsumf1o 19934 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚))))) |
| 189 | 65 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ ((𝐹 ∘f − 𝑗) ∘f −
𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) |
| 190 | 188, 189 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))) |
| 191 | 190 | mpteq2dva 5242 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))) = (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋)))) |
| 192 | 191 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦
⦋((𝐹
∘f − 𝑚) ∘f − 𝑗) / 𝑘⦌𝑋))))) |
| 193 | 100, 172,
192 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑗)} ↦ 𝑋))))) |