Step |
Hyp |
Ref |
Expression |
1 |
|
psrbag.d |
⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
2 |
|
psrbagconf1o.s |
⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } |
3 |
|
gsumbagdiagOLD.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
4 |
|
gsumbagdiagOLD.f |
⊢ ( 𝜑 → 𝐹 ∈ 𝐷 ) |
5 |
|
gsumbagdiagOLD.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
6 |
|
gsumbagdiagOLD.g |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
7 |
|
gsumbagdiagOLD.x |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑋 ∈ 𝐵 ) |
8 |
|
psrass1lemOLD.y |
⊢ ( 𝑘 = ( 𝑛 ∘f − 𝑗 ) → 𝑋 = 𝑌 ) |
9 |
1 2 3 4
|
gsumbagdiaglemOLD |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) ) → ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) |
10 |
7
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑋 ∈ 𝐵 ) |
11 |
10
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ 𝐵 ) |
12 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → 𝐼 ∈ 𝑉 ) |
13 |
2
|
ssrab3 |
⊢ 𝑆 ⊆ 𝐷 |
14 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → 𝐹 ∈ 𝐷 ) |
15 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → 𝑗 ∈ 𝑆 ) |
16 |
1 2
|
psrbagconclOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑗 ) ∈ 𝑆 ) |
17 |
12 14 15 16
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑗 ) ∈ 𝑆 ) |
18 |
13 17
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑗 ) ∈ 𝐷 ) |
19 |
|
eqid |
⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } = { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } |
20 |
1 19
|
psrbagconf1oOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘f − 𝑗 ) ∈ 𝐷 ) → ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } –1-1-onto→ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
21 |
12 18 20
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } –1-1-onto→ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
22 |
|
f1of |
⊢ ( ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } –1-1-onto→ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } → ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
23 |
21 22
|
syl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
24 |
|
fco |
⊢ ( ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ 𝐵 ∧ ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∘ ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ 𝐵 ) |
25 |
11 23 24
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∘ ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ 𝐵 ) |
26 |
12
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝐼 ∈ 𝑉 ) |
27 |
14
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝐹 ∈ 𝐷 ) |
28 |
1
|
psrbagfOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 ) |
29 |
26 27 28
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝐹 : 𝐼 ⟶ ℕ0 ) |
30 |
29
|
ffvelrnda |
⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ0 ) |
31 |
15
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑗 ∈ 𝑆 ) |
32 |
13 31
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑗 ∈ 𝐷 ) |
33 |
1
|
psrbagfOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐷 ) → 𝑗 : 𝐼 ⟶ ℕ0 ) |
34 |
26 32 33
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑗 : 𝐼 ⟶ ℕ0 ) |
35 |
34
|
ffvelrnda |
⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 ) |
36 |
|
ssrab2 |
⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⊆ 𝐷 |
37 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
38 |
36 37
|
sselid |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑚 ∈ 𝐷 ) |
39 |
1
|
psrbagfOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑚 ∈ 𝐷 ) → 𝑚 : 𝐼 ⟶ ℕ0 ) |
40 |
26 38 39
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑚 : 𝐼 ⟶ ℕ0 ) |
41 |
40
|
ffvelrnda |
⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑚 ‘ 𝑧 ) ∈ ℕ0 ) |
42 |
|
nn0cn |
⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ℕ0 → ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) |
43 |
|
nn0cn |
⊢ ( ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑗 ‘ 𝑧 ) ∈ ℂ ) |
44 |
|
nn0cn |
⊢ ( ( 𝑚 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑚 ‘ 𝑧 ) ∈ ℂ ) |
45 |
|
sub32 |
⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑗 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝑚 ‘ 𝑧 ) ∈ ℂ ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( 𝑚 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑚 ‘ 𝑧 ) ) − ( 𝑗 ‘ 𝑧 ) ) ) |
46 |
42 43 44 45
|
syl3an |
⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑗 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑚 ‘ 𝑧 ) ∈ ℕ0 ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( 𝑚 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑚 ‘ 𝑧 ) ) − ( 𝑗 ‘ 𝑧 ) ) ) |
47 |
30 35 41 46
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( 𝑚 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑚 ‘ 𝑧 ) ) − ( 𝑗 ‘ 𝑧 ) ) ) |
48 |
47
|
mpteq2dva |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( 𝑚 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑚 ‘ 𝑧 ) ) − ( 𝑗 ‘ 𝑧 ) ) ) ) |
49 |
|
ovexd |
⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ∈ V ) |
50 |
29
|
feqmptd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝐹 = ( 𝑧 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑧 ) ) ) |
51 |
34
|
feqmptd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑗 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑗 ‘ 𝑧 ) ) ) |
52 |
26 30 35 50 51
|
offval2 |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( 𝐹 ∘f − 𝑗 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) ) ) |
53 |
40
|
feqmptd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑚 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑚 ‘ 𝑧 ) ) ) |
54 |
26 49 41 52 53
|
offval2 |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑗 ‘ 𝑧 ) ) − ( 𝑚 ‘ 𝑧 ) ) ) ) |
55 |
|
ovexd |
⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝑚 ‘ 𝑧 ) ) ∈ V ) |
56 |
26 30 41 50 53
|
offval2 |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( 𝐹 ∘f − 𝑚 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑚 ‘ 𝑧 ) ) ) ) |
57 |
26 55 35 56 51
|
offval2 |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝑚 ‘ 𝑧 ) ) − ( 𝑗 ‘ 𝑧 ) ) ) ) |
58 |
48 54 57
|
3eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) = ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) ) |
59 |
18
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( 𝐹 ∘f − 𝑗 ) ∈ 𝐷 ) |
60 |
1 19
|
psrbagconclOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘f − 𝑗 ) ∈ 𝐷 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
61 |
26 59 37 60
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
62 |
58 61
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
63 |
58
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) = ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) ) ) |
64 |
|
nfcv |
⊢ Ⅎ 𝑛 𝑋 |
65 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑛 / 𝑘 ⦌ 𝑋 |
66 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑛 → 𝑋 = ⦋ 𝑛 / 𝑘 ⦌ 𝑋 ) |
67 |
64 65 66
|
cbvmpt |
⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) = ( 𝑛 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ 𝑛 / 𝑘 ⦌ 𝑋 ) |
68 |
67
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) = ( 𝑛 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ 𝑛 / 𝑘 ⦌ 𝑋 ) ) |
69 |
|
csbeq1 |
⊢ ( 𝑛 = ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) → ⦋ 𝑛 / 𝑘 ⦌ 𝑋 = ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) |
70 |
62 63 68 69
|
fmptco |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∘ ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) ) = ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) |
71 |
70
|
feq1d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∘ ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ 𝐵 ↔ ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ 𝐵 ) ) |
72 |
25 71
|
mpbid |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ⟶ 𝐵 ) |
73 |
72
|
fvmptelrn |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ∈ 𝐵 ) |
74 |
73
|
anasss |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ∈ 𝐵 ) |
75 |
9 74
|
syldan |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) ) → ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ∈ 𝐵 ) |
76 |
1 2 3 4 5 6 75
|
gsumbagdiagOLD |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑚 ∈ 𝑆 , 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝑆 , 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) |
77 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
78 |
1
|
psrbaglefiOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ Fin ) |
79 |
3 4 78
|
syl2anc |
⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ Fin ) |
80 |
2 79
|
eqeltrid |
⊢ ( 𝜑 → 𝑆 ∈ Fin ) |
81 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → 𝐼 ∈ 𝑉 ) |
82 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → 𝐹 ∈ 𝐷 ) |
83 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → 𝑚 ∈ 𝑆 ) |
84 |
1 2
|
psrbagconclOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑚 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑚 ) ∈ 𝑆 ) |
85 |
81 82 83 84
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑚 ) ∈ 𝑆 ) |
86 |
13 85
|
sselid |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑚 ) ∈ 𝐷 ) |
87 |
1
|
psrbaglefiOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘f − 𝑚 ) ∈ 𝐷 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ∈ Fin ) |
88 |
81 86 87
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ∈ Fin ) |
89 |
|
xpfi |
⊢ ( ( 𝑆 ∈ Fin ∧ 𝑆 ∈ Fin ) → ( 𝑆 × 𝑆 ) ∈ Fin ) |
90 |
80 80 89
|
syl2anc |
⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ∈ Fin ) |
91 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) ) → 𝑚 ∈ 𝑆 ) |
92 |
9
|
simpld |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) ) → 𝑗 ∈ 𝑆 ) |
93 |
|
brxp |
⊢ ( 𝑚 ( 𝑆 × 𝑆 ) 𝑗 ↔ ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ 𝑆 ) ) |
94 |
91 92 93
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) ) → 𝑚 ( 𝑆 × 𝑆 ) 𝑗 ) |
95 |
94
|
pm2.24d |
⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) ) → ( ¬ 𝑚 ( 𝑆 × 𝑆 ) 𝑗 → ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 = ( 0g ‘ 𝐺 ) ) ) |
96 |
95
|
impr |
⊢ ( ( 𝜑 ∧ ( ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) ∧ ¬ 𝑚 ( 𝑆 × 𝑆 ) 𝑗 ) ) → ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 = ( 0g ‘ 𝐺 ) ) |
97 |
5 77 6 80 88 75 90 96
|
gsum2d2 |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑚 ∈ 𝑆 , 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) = ( 𝐺 Σg ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) ) |
98 |
1
|
psrbaglefiOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘f − 𝑗 ) ∈ 𝐷 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ Fin ) |
99 |
12 18 98
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ Fin ) |
100 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑗 ∈ 𝑆 ) |
101 |
1 2 3 4
|
gsumbagdiaglemOLD |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) ) |
102 |
101
|
simpld |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑚 ∈ 𝑆 ) |
103 |
|
brxp |
⊢ ( 𝑗 ( 𝑆 × 𝑆 ) 𝑚 ↔ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ 𝑆 ) ) |
104 |
100 102 103
|
sylanbrc |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑗 ( 𝑆 × 𝑆 ) 𝑚 ) |
105 |
104
|
pm2.24d |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → ( ¬ 𝑗 ( 𝑆 × 𝑆 ) 𝑚 → ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 = ( 0g ‘ 𝐺 ) ) ) |
106 |
105
|
impr |
⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ ¬ 𝑗 ( 𝑆 × 𝑆 ) 𝑚 ) ) → ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 = ( 0g ‘ 𝐺 ) ) |
107 |
5 77 6 80 99 74 90 106
|
gsum2d2 |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝑆 , 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) ) |
108 |
76 97 107
|
3eqtr3d |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) ) |
109 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → 𝐺 ∈ CMnd ) |
110 |
75
|
anassrs |
⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) → ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ∈ 𝐵 ) |
111 |
110
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) : { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ⟶ 𝐵 ) |
112 |
|
ovex |
⊢ ( ℕ0 ↑m 𝐼 ) ∈ V |
113 |
1 112
|
rabex2 |
⊢ 𝐷 ∈ V |
114 |
113
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → 𝐷 ∈ V ) |
115 |
|
rabexg |
⊢ ( 𝐷 ∈ V → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ∈ V ) |
116 |
|
mptexg |
⊢ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ∈ V → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ∈ V ) |
117 |
114 115 116
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ∈ V ) |
118 |
|
funmpt |
⊢ Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) |
119 |
118
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → Fun ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) |
120 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ V ) |
121 |
|
suppssdm |
⊢ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ dom ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) |
122 |
|
eqid |
⊢ ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) = ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) |
123 |
122
|
dmmptss |
⊢ dom ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } |
124 |
121 123
|
sstri |
⊢ ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } |
125 |
124
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) |
126 |
|
suppssfifsupp |
⊢ ( ( ( ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘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 ‘ 𝐺 ) ) |
127 |
117 119 120 88 125 126
|
syl32anc |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) ) |
128 |
5 77 109 88 111 127
|
gsumcl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ∈ 𝐵 ) |
129 |
128
|
fmpttd |
⊢ ( 𝜑 → ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) : 𝑆 ⟶ 𝐵 ) |
130 |
1 2
|
psrbagconf1oOLD |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 –1-1-onto→ 𝑆 ) |
131 |
3 4 130
|
syl2anc |
⊢ ( 𝜑 → ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 –1-1-onto→ 𝑆 ) |
132 |
|
f1ocnv |
⊢ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 –1-1-onto→ 𝑆 → ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 –1-1-onto→ 𝑆 ) |
133 |
|
f1of |
⊢ ( ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 –1-1-onto→ 𝑆 → ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 ⟶ 𝑆 ) |
134 |
131 132 133
|
3syl |
⊢ ( 𝜑 → ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 ⟶ 𝑆 ) |
135 |
|
fco |
⊢ ( ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) : 𝑆 ⟶ 𝐵 ∧ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 ⟶ 𝑆 ) → ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) : 𝑆 ⟶ 𝐵 ) |
136 |
129 134 135
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) : 𝑆 ⟶ 𝐵 ) |
137 |
|
coass |
⊢ ( ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) = ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) ) |
138 |
|
f1ococnv2 |
⊢ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) : 𝑆 –1-1-onto→ 𝑆 → ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) = ( I ↾ 𝑆 ) ) |
139 |
131 138
|
syl |
⊢ ( 𝜑 → ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) = ( I ↾ 𝑆 ) ) |
140 |
139
|
coeq2d |
⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) ) = ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( I ↾ 𝑆 ) ) ) |
141 |
137 140
|
syl5eq |
⊢ ( 𝜑 → ( ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) = ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( I ↾ 𝑆 ) ) ) |
142 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) = ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) |
143 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) = ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) |
144 |
|
breq2 |
⊢ ( 𝑛 = ( 𝐹 ∘f − 𝑚 ) → ( 𝑥 ∘r ≤ 𝑛 ↔ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) ) ) |
145 |
144
|
rabbidv |
⊢ ( 𝑛 = ( 𝐹 ∘f − 𝑚 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } = { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ) |
146 |
|
ovex |
⊢ ( 𝑛 ∘f − 𝑗 ) ∈ V |
147 |
146 8
|
csbie |
⊢ ⦋ ( 𝑛 ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 = 𝑌 |
148 |
|
oveq1 |
⊢ ( 𝑛 = ( 𝐹 ∘f − 𝑚 ) → ( 𝑛 ∘f − 𝑗 ) = ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) ) |
149 |
148
|
csbeq1d |
⊢ ( 𝑛 = ( 𝐹 ∘f − 𝑚 ) → ⦋ ( 𝑛 ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 = ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) |
150 |
147 149
|
eqtr3id |
⊢ ( 𝑛 = ( 𝐹 ∘f − 𝑚 ) → 𝑌 = ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) |
151 |
145 150
|
mpteq12dv |
⊢ ( 𝑛 = ( 𝐹 ∘f − 𝑚 ) → ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) = ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) |
152 |
151
|
oveq2d |
⊢ ( 𝑛 = ( 𝐹 ∘f − 𝑚 ) → ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) = ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) |
153 |
85 142 143 152
|
fmptco |
⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) = ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) |
154 |
153
|
coeq1d |
⊢ ( 𝜑 → ( ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) = ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) ) |
155 |
|
coires1 |
⊢ ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( I ↾ 𝑆 ) ) = ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ↾ 𝑆 ) |
156 |
|
ssid |
⊢ 𝑆 ⊆ 𝑆 |
157 |
|
resmpt |
⊢ ( 𝑆 ⊆ 𝑆 → ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ↾ 𝑆 ) = ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) |
158 |
156 157
|
ax-mp |
⊢ ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ↾ 𝑆 ) = ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) |
159 |
155 158
|
eqtri |
⊢ ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( I ↾ 𝑆 ) ) = ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) |
160 |
159
|
a1i |
⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( I ↾ 𝑆 ) ) = ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) |
161 |
141 154 160
|
3eqtr3d |
⊢ ( 𝜑 → ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) = ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) |
162 |
161
|
feq1d |
⊢ ( 𝜑 → ( ( ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ∘ ◡ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) : 𝑆 ⟶ 𝐵 ↔ ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) : 𝑆 ⟶ 𝐵 ) ) |
163 |
136 162
|
mpbid |
⊢ ( 𝜑 → ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) : 𝑆 ⟶ 𝐵 ) |
164 |
|
rabexg |
⊢ ( 𝐷 ∈ V → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ V ) |
165 |
113 164
|
mp1i |
⊢ ( 𝜑 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 } ∈ V ) |
166 |
2 165
|
eqeltrid |
⊢ ( 𝜑 → 𝑆 ∈ V ) |
167 |
166
|
mptexd |
⊢ ( 𝜑 → ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∈ V ) |
168 |
|
funmpt |
⊢ Fun ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) |
169 |
168
|
a1i |
⊢ ( 𝜑 → Fun ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) |
170 |
|
fvexd |
⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V ) |
171 |
|
suppssdm |
⊢ ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) supp ( 0g ‘ 𝐺 ) ) ⊆ dom ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) |
172 |
|
eqid |
⊢ ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) = ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) |
173 |
172
|
dmmptss |
⊢ dom ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ⊆ 𝑆 |
174 |
171 173
|
sstri |
⊢ ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) supp ( 0g ‘ 𝐺 ) ) ⊆ 𝑆 |
175 |
174
|
a1i |
⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) supp ( 0g ‘ 𝐺 ) ) ⊆ 𝑆 ) |
176 |
|
suppssfifsupp |
⊢ ( ( ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∈ V ∧ Fun ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∧ ( 0g ‘ 𝐺 ) ∈ V ) ∧ ( 𝑆 ∈ Fin ∧ ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) supp ( 0g ‘ 𝐺 ) ) ⊆ 𝑆 ) ) → ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) finSupp ( 0g ‘ 𝐺 ) ) |
177 |
167 169 170 80 175 176
|
syl32anc |
⊢ ( 𝜑 → ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) finSupp ( 0g ‘ 𝐺 ) ) |
178 |
5 77 6 80 163 177 131
|
gsumf1o |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) = ( 𝐺 Σg ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) ) ) |
179 |
153
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ∘ ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑚 ) ) ) ) = ( 𝐺 Σg ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) ) |
180 |
178 179
|
eqtrd |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) = ( 𝐺 Σg ( 𝑚 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) ) |
181 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → 𝐺 ∈ CMnd ) |
182 |
113
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → 𝐷 ∈ V ) |
183 |
|
rabexg |
⊢ ( 𝐷 ∈ V → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ V ) |
184 |
|
mptexg |
⊢ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ V → ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∈ V ) |
185 |
182 183 184
|
3syl |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∈ V ) |
186 |
|
funmpt |
⊢ Fun ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) |
187 |
186
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → Fun ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) |
188 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ V ) |
189 |
|
suppssdm |
⊢ ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ dom ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) |
190 |
|
eqid |
⊢ ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) = ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) |
191 |
190
|
dmmptss |
⊢ dom ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } |
192 |
189 191
|
sstri |
⊢ ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } |
193 |
192
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) |
194 |
|
suppssfifsupp |
⊢ ( ( ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∈ V ∧ Fun ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∧ ( 0g ‘ 𝐺 ) ∈ V ) ∧ ( { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ Fin ∧ ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) supp ( 0g ‘ 𝐺 ) ) ⊆ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) ) |
195 |
185 187 188 99 193 194
|
syl32anc |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) ) |
196 |
5 77 181 99 11 195 21
|
gsumf1o |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) = ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∘ ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) ) ) ) |
197 |
70
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐺 Σg ( ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ∘ ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ( ( 𝐹 ∘f − 𝑗 ) ∘f − 𝑚 ) ) ) ) = ( 𝐺 Σg ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) |
198 |
196 197
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) |
199 |
198
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) ) = ( 𝑗 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) |
200 |
199
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) ) ) ) |
201 |
108 180 200
|
3eqtr4d |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) ) ) ) |