Step | Hyp | Ref
| Expression |
1 | | psrbag.d |
. . . 4
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
2 | | psrbagconf1o.1 |
. . . 4
⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} |
3 | | gsumbagdiag.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
4 | | gsumbagdiag.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐷) |
5 | | gsumbagdiag.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
6 | | gsumbagdiag.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) |
7 | 1, 2, 3, 4 | gsumbagdiaglem 19196 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)})) → (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) |
8 | | gsumbagdiag.x |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) → 𝑋 ∈ 𝐵) |
9 | 8 | anassrs 678 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑋 ∈ 𝐵) |
10 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) = (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) |
11 | 9, 10 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶𝐵) |
12 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐼 ∈ 𝑉) |
13 | | ssrab2 3650 |
. . . . . . . . . . . . . 14
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ⊆ 𝐷 |
14 | 2, 13 | eqsstri 3598 |
. . . . . . . . . . . . 13
⊢ 𝑆 ⊆ 𝐷 |
15 | 4 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐹 ∈ 𝐷) |
16 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝑗 ∈ 𝑆) |
17 | 1, 2 | psrbagconcl 19194 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑗) ∈ 𝑆) |
18 | 12, 15, 16, 17 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑗) ∈ 𝑆) |
19 | 14, 18 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑗) ∈ 𝐷) |
20 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} |
21 | 1, 20 | psrbagconf1o 19195 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘𝑓 − 𝑗) ∈ 𝐷) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
22 | 12, 19, 21 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
23 | | f1of 6050 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}–1-1-onto→{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
25 | | fco 5971 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶𝐵 ∧ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚)):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶𝐵) |
26 | 11, 24, 25 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶𝐵) |
27 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝐼 ∈ 𝑉) |
28 | 15 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝐹 ∈ 𝐷) |
29 | 1 | psrbagf 19186 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) |
30 | 27, 28, 29 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝐹:𝐼⟶ℕ0) |
31 | 30 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈
ℕ0) |
32 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑗 ∈ 𝑆) |
33 | 14, 32 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑗 ∈ 𝐷) |
34 | 1 | psrbagf 19186 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐷) → 𝑗:𝐼⟶ℕ0) |
35 | 27, 33, 34 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑗:𝐼⟶ℕ0) |
36 | 35 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑗‘𝑧) ∈
ℕ0) |
37 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ⊆ 𝐷 |
38 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
39 | 37, 38 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑚 ∈ 𝐷) |
40 | 1 | psrbagf 19186 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑚 ∈ 𝐷) → 𝑚:𝐼⟶ℕ0) |
41 | 27, 39, 40 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑚:𝐼⟶ℕ0) |
42 | 41 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (𝑚‘𝑧) ∈
ℕ0) |
43 | | nn0cn 11179 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℂ) |
44 | | nn0cn 11179 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗‘𝑧) ∈ ℕ0 → (𝑗‘𝑧) ∈ ℂ) |
45 | | nn0cn 11179 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚‘𝑧) ∈ ℕ0 → (𝑚‘𝑧) ∈ ℂ) |
46 | | sub32 10194 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝑧) ∈ ℂ ∧ (𝑗‘𝑧) ∈ ℂ ∧ (𝑚‘𝑧) ∈ ℂ) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))) |
47 | 43, 44, 45, 46 | syl3an 1360 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑧) ∈ ℕ0 ∧ (𝑗‘𝑧) ∈ ℕ0 ∧ (𝑚‘𝑧) ∈ ℕ0) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))) |
48 | 31, 36, 42, 47 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) ∧ 𝑧 ∈ 𝐼) → (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)) = (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧))) |
49 | 48 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧))) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))) |
50 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑧) − (𝑗‘𝑧)) ∈ V |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑗‘𝑧)) ∈ V) |
52 | 30 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝐹 = (𝑧 ∈ 𝐼 ↦ (𝐹‘𝑧))) |
53 | 35 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑗 = (𝑧 ∈ 𝐼 ↦ (𝑗‘𝑧))) |
54 | 27, 31, 36, 52, 53 | offval2 6812 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → (𝐹 ∘𝑓
− 𝑗) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑗‘𝑧)))) |
55 | 41 | feqmptd 6159 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → 𝑚 = (𝑧 ∈ 𝐼 ↦ (𝑚‘𝑧))) |
56 | 27, 51, 42, 54, 55 | offval2 6812 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑗‘𝑧)) − (𝑚‘𝑧)))) |
57 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑧) − (𝑚‘𝑧)) ∈ V |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑚‘𝑧)) ∈ V) |
59 | 27, 31, 42, 52, 55 | offval2 6812 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → (𝐹 ∘𝑓
− 𝑚) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑚‘𝑧)))) |
60 | 27, 58, 36, 59, 53 | offval2 6812 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → ((𝐹 ∘𝑓
− 𝑚)
∘𝑓 − 𝑗) = (𝑧 ∈ 𝐼 ↦ (((𝐹‘𝑧) − (𝑚‘𝑧)) − (𝑗‘𝑧)))) |
61 | 49, 56, 60 | 3eqtr4d 2654 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚) = ((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗)) |
62 | 19 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → (𝐹 ∘𝑓
− 𝑗) ∈ 𝐷) |
63 | 1, 20 | psrbagconcl 19194 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘𝑓 − 𝑗) ∈ 𝐷 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
64 | 27, 62, 38, 63 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
65 | 61, 64 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) → ((𝐹 ∘𝑓
− 𝑚)
∘𝑓 − 𝑗) ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
66 | 61 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚)) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑚)
∘𝑓 − 𝑗))) |
67 | | nfcv 2751 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛𝑋 |
68 | | nfcsb1v 3515 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘⦋𝑛 / 𝑘⦌𝑋 |
69 | | csbeq1a 3508 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → 𝑋 = ⦋𝑛 / 𝑘⦌𝑋) |
70 | 67, 68, 69 | cbvmpt 4677 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋𝑛 / 𝑘⦌𝑋) |
71 | 70 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) = (𝑛 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋𝑛 / 𝑘⦌𝑋)) |
72 | | csbeq1 3502 |
. . . . . . . . . . 11
⊢ (𝑛 = ((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) →
⦋𝑛 / 𝑘⦌𝑋 = ⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋) |
73 | 65, 66, 71, 72 | fmptco 6303 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚))) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)) |
74 | 73 | feq1d 5943 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚))):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶𝐵 ↔ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶𝐵)) |
75 | 26, 74 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶𝐵) |
76 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) = (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) |
77 | 76 | fmpt 6289 |
. . . . . . . 8
⊢
(∀𝑚 ∈
{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋 ∈ 𝐵 ↔ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⟶𝐵) |
78 | 75, 77 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ∀𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
79 | 78 | r19.21bi 2916 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑆) ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) →
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
80 | 79 | anasss 677 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) →
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
81 | 7, 80 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)})) →
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
82 | 1, 2, 3, 4, 5, 6, 81 | gsumbagdiag 19197 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) |
83 | | eqid 2610 |
. . . 4
⊢
(0g‘𝐺) = (0g‘𝐺) |
84 | 1 | psrbaglefi 19193 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ∈ Fin) |
85 | 3, 4, 84 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ∈ Fin) |
86 | 2, 85 | syl5eqel 2692 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ Fin) |
87 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐼 ∈ 𝑉) |
88 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐹 ∈ 𝐷) |
89 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝑚 ∈ 𝑆) |
90 | 1, 2 | psrbagconcl 19194 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑚) ∈ 𝑆) |
91 | 87, 88, 89, 90 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑚) ∈ 𝑆) |
92 | 14, 91 | sseldi 3566 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑚) ∈ 𝐷) |
93 | 1 | psrbaglefi 19193 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘𝑓 − 𝑚) ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ∈
Fin) |
94 | 87, 92, 93 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ∈
Fin) |
95 | | xpfi 8116 |
. . . . 5
⊢ ((𝑆 ∈ Fin ∧ 𝑆 ∈ Fin) → (𝑆 × 𝑆) ∈ Fin) |
96 | 86, 86, 95 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑆 × 𝑆) ∈ Fin) |
97 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)})) → 𝑚 ∈ 𝑆) |
98 | 7 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)})) → 𝑗 ∈ 𝑆) |
99 | | brxp 5071 |
. . . . . . 7
⊢ (𝑚(𝑆 × 𝑆)𝑗 ↔ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ 𝑆)) |
100 | 97, 98, 99 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)})) → 𝑚(𝑆 × 𝑆)𝑗) |
101 | 100 | pm2.24d 146 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)})) → (¬
𝑚(𝑆 × 𝑆)𝑗 → ⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))) |
102 | 101 | impr 647 |
. . . 4
⊢ ((𝜑 ∧ ((𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)}) ∧ ¬
𝑚(𝑆 × 𝑆)𝑗)) → ⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)) |
103 | 5, 83, 6, 86, 94, 81, 96, 102 | gsum2d2 18196 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆, 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))))) |
104 | 1 | psrbaglefi 19193 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘𝑓 − 𝑗) ∈ 𝐷) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ∈
Fin) |
105 | 12, 19, 104 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ∈
Fin) |
106 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) → 𝑗 ∈ 𝑆) |
107 | 1, 2, 3, 4 | gsumbagdiaglem 19196 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) → (𝑚 ∈ 𝑆 ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)})) |
108 | 107 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) → 𝑚 ∈ 𝑆) |
109 | | brxp 5071 |
. . . . . . 7
⊢ (𝑗(𝑆 × 𝑆)𝑚 ↔ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ 𝑆)) |
110 | 106, 108,
109 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) → 𝑗(𝑆 × 𝑆)𝑚) |
111 | 110 | pm2.24d 146 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) → (¬
𝑗(𝑆 × 𝑆)𝑚 → ⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺))) |
112 | 111 | impr 647 |
. . . 4
⊢ ((𝜑 ∧ ((𝑗 ∈ 𝑆 ∧ 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) ∧ ¬
𝑗(𝑆 × 𝑆)𝑚)) → ⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋 = (0g‘𝐺)) |
113 | 5, 83, 6, 86, 105, 80, 96, 112 | gsum2d2 18196 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆, 𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))))) |
114 | 82, 103, 113 | 3eqtr3d 2652 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))))) |
115 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐺 ∈ CMnd) |
116 | 81 | anassrs 678 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ 𝑆) ∧ 𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)}) →
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋 ∈ 𝐵) |
117 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) |
118 | 116, 117 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋):{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)}⟶𝐵) |
119 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
120 | 1, 119 | rabex2 4742 |
. . . . . . . . . . 11
⊢ 𝐷 ∈ V |
121 | 120 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → 𝐷 ∈ V) |
122 | | rabexg 4739 |
. . . . . . . . . 10
⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ∈
V) |
123 | | mptexg 6389 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ∈ V →
(𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) ∈ V) |
124 | 121, 122,
123 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) ∈ V) |
125 | | funmpt 5840 |
. . . . . . . . . 10
⊢ Fun
(𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) |
126 | 125 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)) |
127 | | fvex 6113 |
. . . . . . . . . 10
⊢
(0g‘𝐺) ∈ V |
128 | 127 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (0g‘𝐺) ∈ V) |
129 | | suppssdm 7195 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ dom (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) |
130 | 117 | dmmptss 5548 |
. . . . . . . . . . 11
⊢ dom
(𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} |
131 | 129, 130 | sstri 3577 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} |
132 | 131 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)}) |
133 | | suppssfifsupp 8173 |
. . . . . . . . 9
⊢ ((((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) ∈ V ∧ Fun (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) ∧ (0g‘𝐺) ∈ V) ∧ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ∈ Fin
∧ ((𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) supp (0g‘𝐺)) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)})) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) finSupp (0g‘𝐺)) |
134 | 124, 126,
128, 94, 132, 133 | syl32anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋) finSupp (0g‘𝐺)) |
135 | 5, 83, 115, 94, 118, 134 | gsumcl 18139 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑆) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)) ∈ 𝐵) |
136 | | eqid 2610 |
. . . . . . 7
⊢ (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) = (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) |
137 | 135, 136 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵) |
138 | 1, 2 | psrbagconf1o 19195 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆–1-1-onto→𝑆) |
139 | 3, 4, 138 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆–1-1-onto→𝑆) |
140 | | f1ocnv 6062 |
. . . . . . 7
⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆–1-1-onto→𝑆) |
141 | | f1of 6050 |
. . . . . . 7
⊢ (◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆–1-1-onto→𝑆 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆⟶𝑆) |
142 | 139, 140,
141 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆⟶𝑆) |
143 | | fco 5971 |
. . . . . 6
⊢ (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))):𝑆⟶𝐵 ∧ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆⟶𝑆) → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))):𝑆⟶𝐵) |
144 | 137, 142,
143 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))):𝑆⟶𝐵) |
145 | | coass 5571 |
. . . . . . . 8
⊢ (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)))) |
146 | | f1ococnv2 6076 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)):𝑆–1-1-onto→𝑆 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) = ( I ↾ 𝑆)) |
147 | 139, 146 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) = ( I ↾ 𝑆)) |
148 | 147 | coeq2d 5206 |
. . . . . . . 8
⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ ((𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆))) |
149 | 145, 148 | syl5eq 2656 |
. . . . . . 7
⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆))) |
150 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)) = (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) |
151 | | eqidd 2611 |
. . . . . . . . 9
⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) |
152 | | breq2 4587 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝐹 ∘𝑓 − 𝑚) → (𝑥 ∘𝑟 ≤ 𝑛 ↔ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚))) |
153 | 152 | rabbidv 3164 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝐹 ∘𝑓 − 𝑚) → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} = {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)}) |
154 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∘𝑓
− 𝑗) ∈
V |
155 | | psrass1lem.y |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 ∘𝑓 − 𝑗) → 𝑋 = 𝑌) |
156 | 154, 155 | csbie 3525 |
. . . . . . . . . . . 12
⊢
⦋(𝑛
∘𝑓 − 𝑗) / 𝑘⦌𝑋 = 𝑌 |
157 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑛 = (𝐹 ∘𝑓 − 𝑚) → (𝑛 ∘𝑓 − 𝑗) = ((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗)) |
158 | 157 | csbeq1d 3506 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝐹 ∘𝑓 − 𝑚) → ⦋(𝑛 ∘𝑓
− 𝑗) / 𝑘⦌𝑋 = ⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋) |
159 | 156, 158 | syl5eqr 2658 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝐹 ∘𝑓 − 𝑚) → 𝑌 = ⦋((𝐹 ∘𝑓 − 𝑚) ∘𝑓
− 𝑗) / 𝑘⦌𝑋) |
160 | 153, 159 | mpteq12dv 4663 |
. . . . . . . . . 10
⊢ (𝑛 = (𝐹 ∘𝑓 − 𝑚) → (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌) = (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)) |
161 | 160 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑛 = (𝐹 ∘𝑓 − 𝑚) → (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)) = (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) |
162 | 91, 150, 151, 161 | fmptco 6303 |
. . . . . . . 8
⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) = (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)))) |
163 | 162 | coeq1d 5205 |
. . . . . . 7
⊢ (𝜑 → (((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) = ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)))) |
164 | | coires1 5570 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) |
165 | | ssid 3587 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ 𝑆 |
166 | | resmpt 5369 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ 𝑆 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) |
167 | 165, 166 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ↾ 𝑆) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) |
168 | 164, 167 | eqtri 2632 |
. . . . . . . 8
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) |
169 | 168 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ ( I ↾ 𝑆)) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) |
170 | 149, 163,
169 | 3eqtr3d 2652 |
. . . . . 6
⊢ (𝜑 → ((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) |
171 | 170 | feq1d 5943 |
. . . . 5
⊢ (𝜑 → (((𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) ∘ ◡(𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))):𝑆⟶𝐵 ↔ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵)) |
172 | 144, 171 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))):𝑆⟶𝐵) |
173 | | rabexg 4739 |
. . . . . . . 8
⊢ (𝐷 ∈ V → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ∈ V) |
174 | 120, 173 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ∈ V) |
175 | 2, 174 | syl5eqel 2692 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ V) |
176 | | mptexg 6389 |
. . . . . 6
⊢ (𝑆 ∈ V → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∈ V) |
177 | 175, 176 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∈ V) |
178 | | funmpt 5840 |
. . . . . 6
⊢ Fun
(𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) |
179 | 178 | a1i 11 |
. . . . 5
⊢ (𝜑 → Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) |
180 | 127 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0g‘𝐺) ∈ V) |
181 | | suppssdm 7195 |
. . . . . . 7
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ dom (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) |
182 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) = (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) |
183 | 182 | dmmptss 5548 |
. . . . . . 7
⊢ dom
(𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ⊆ 𝑆 |
184 | 181, 183 | sstri 3577 |
. . . . . 6
⊢ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆 |
185 | 184 | a1i 11 |
. . . . 5
⊢ (𝜑 → ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆) |
186 | | suppssfifsupp 8173 |
. . . . 5
⊢ ((((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∈ V ∧ Fun (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∧ (0g‘𝐺) ∈ V) ∧ (𝑆 ∈ Fin ∧ ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) supp (0g‘𝐺)) ⊆ 𝑆)) → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺)) |
187 | 177, 179,
180, 86, 185, 186 | syl32anc 1326 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) finSupp (0g‘𝐺)) |
188 | 5, 83, 6, 86, 172, 187, 139 | gsumf1o 18140 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚))))) |
189 | 162 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (𝐺 Σg ((𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌))) ∘ (𝑚 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑚)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))))) |
190 | 188, 189 | eqtrd 2644 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑚 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑚)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))))) |
191 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐺 ∈ CMnd) |
192 | 120 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → 𝐷 ∈ V) |
193 | | rabexg 4739 |
. . . . . . . 8
⊢ (𝐷 ∈ V → {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ∈
V) |
194 | | mptexg 6389 |
. . . . . . . 8
⊢ ({𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ∈ V →
(𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∈ V) |
195 | 192, 193,
194 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∈ V) |
196 | | funmpt 5840 |
. . . . . . . 8
⊢ Fun
(𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) |
197 | 196 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋)) |
198 | 127 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (0g‘𝐺) ∈ V) |
199 | | suppssdm 7195 |
. . . . . . . . 9
⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) supp
(0g‘𝐺))
⊆ dom (𝑘 ∈
{𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) |
200 | 10 | dmmptss 5548 |
. . . . . . . . 9
⊢ dom
(𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} |
201 | 199, 200 | sstri 3577 |
. . . . . . . 8
⊢ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) supp
(0g‘𝐺))
⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} |
202 | 201 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) supp
(0g‘𝐺))
⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)}) |
203 | | suppssfifsupp 8173 |
. . . . . . 7
⊢ ((((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∈ V ∧ Fun (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∧
(0g‘𝐺)
∈ V) ∧ ({𝑥 ∈
𝐷 ∣ 𝑥 ∘𝑟
≤ (𝐹
∘𝑓 − 𝑗)} ∈ Fin ∧ ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) supp
(0g‘𝐺))
⊆ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)})) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) finSupp
(0g‘𝐺)) |
204 | 195, 197,
198, 105, 202, 203 | syl32anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) finSupp
(0g‘𝐺)) |
205 | 5, 83, 191, 105, 11, 204, 22 | gsumf1o 18140 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋)) = (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚))))) |
206 | 73 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg ((𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋) ∘ (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ ((𝐹 ∘𝑓
− 𝑗)
∘𝑓 − 𝑚)))) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) |
207 | 205, 206 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑆) → (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))) |
208 | 207 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋))) = (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋)))) |
209 | 208 | oveq2d 6565 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑚 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦
⦋((𝐹
∘𝑓 − 𝑚) ∘𝑓 − 𝑗) / 𝑘⦌𝑋))))) |
210 | 114, 190,
209 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (𝐺 Σg (𝑛 ∈ 𝑆 ↦ (𝐺 Σg (𝑗 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ 𝑛} ↦ 𝑌)))) = (𝐺 Σg (𝑗 ∈ 𝑆 ↦ (𝐺 Σg (𝑘 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘𝑟 ≤ (𝐹 ∘𝑓
− 𝑗)} ↦ 𝑋))))) |