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 − 𝑗 ) } ↦ 𝑋 ) ) ) ) )