This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrass1lem

Description: A group sum commutation used by psrass1 . (Contributed by Mario Carneiro, 5-Jan-2015) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024)

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