Metamath Proof Explorer


Theorem psrass1lemOLD

Description: Obsolete version of psrass1lem as of 7-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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 ( ℕ0m 𝐼 ) ∈ 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𝑗 ) } ↦ 𝑋 ) ) ) ) )