Metamath Proof Explorer

Theorem psrass1lem

Description: A group sum commutation used by psrass1 . (Contributed by Mario Carneiro, 5-Jan-2015)

Ref Expression
Hypotheses psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
psrbagconf1o.1 ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
gsumbagdiag.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
gsumbagdiag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
gsumbagdiag.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumbagdiag.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsumbagdiag.x ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑋 ∈ 𝐵 )
psrass1lem.y ⊢ ( 𝑘 = ( 𝑛 ∘f − 𝑗 ) → 𝑋 = 𝑌 )
Assertion psrass1lem ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ 𝑛 } ↦ 𝑌 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ 𝑋 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.1 ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
3 gsumbagdiag.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 gsumbagdiag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
5 gsumbagdiag.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
6 gsumbagdiag.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
7 gsumbagdiag.x ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑘 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑋 ∈ 𝐵 )
8 psrass1lem.y ⊢ ( 𝑘 = ( 𝑛 ∘f − 𝑗 ) → 𝑋 = 𝑌 )
9 1 2 3 4 gsumbagdiaglem ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ 𝑆 ∧ 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘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 psrbagconcl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑗 ) ∈ 𝑆 )
17 12 14 15 16 syl3anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑗 ) ∈ 𝑆 )
18 13 17 sseldi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑗 ) ∈ 𝐷 )
19 eqid ⊢ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } = { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) }
20 1 19 psrbagconf1o ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘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 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
29 26 27 28 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝐹 : 𝐼 ⟶ ℕ0 )
30 29 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ0 )
31 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑗 ∈ 𝑆 )
32 13 31 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑗 ∈ 𝐷 )
33 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑗 ∈ 𝐷 ) → 𝑗 : 𝐼 ⟶ ℕ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 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) → 𝑚 ∈ 𝐷 )
39 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑚 ∈ 𝐷 ) → 𝑚 : 𝐼 ⟶ ℕ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 psrbagconcl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘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 gsumbagdiag ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑚 ∈ 𝑆 , 𝑗 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑚 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) = ( 𝐺 Σg ( 𝑗 ∈ 𝑆 , 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ↦ ⦋ ( ( 𝐹 ∘f − 𝑚 ) ∘f − 𝑗 ) / 𝑘 ⦌ 𝑋 ) ) )
77 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
78 1 psrbaglefi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘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 psrbagconcl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑚 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑚 ) ∈ 𝑆 )
85 81 82 83 84 syl3anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑚 ) ∈ 𝑆 )
86 13 85 sseldi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑚 ) ∈ 𝐷 )
87 1 psrbaglefi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘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 psrbaglefi ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘f − 𝑗 ) ∈ 𝐷 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ Fin )
99 12 18 98 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑆 ) → { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ∈ Fin )
100 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑗 ) } ) ) → 𝑗 ∈ 𝑆 )
101 1 2 3 4 gsumbagdiaglem ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑚 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘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 psrbagconf1o ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝑚 ∈ 𝑆 ↦ ( 𝐹 ∘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 syl5eqr ⊢ ( 𝑛 = ( 𝐹 ∘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 − 𝑗 ) } ↦ 𝑋 ) ) ) ) )