Metamath Proof Explorer

Theorem psrgsum

Description: Finite commutative sums of power series are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses psrgsum.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrgsum.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
psrgsum.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
psrgsum.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrgsum.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
psrgsum.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
psrgsum.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion psrgsum ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 psrgsum.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrgsum.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 psrgsum.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 psrgsum.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 psrgsum.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6 psrgsum.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
7 psrgsum.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 7 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
9 8 oveq2d ⊢ ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
10 mpteq1 ⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) )
11 10 oveq2d ⊢ ( 𝑎 = ∅ → ( 𝑆 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑆 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
12 mpteq1 ⊢ ( 𝑎 = ∅ → ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) = ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) )
13 12 oveq2d ⊢ ( 𝑎 = ∅ → ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) )
14 13 mpteq2dv ⊢ ( 𝑎 = ∅ → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
15 11 14 eqeq12d ⊢ ( 𝑎 = ∅ → ( ( 𝑆 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ↔ ( 𝑆 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) )
16 mpteq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) )
17 16 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑆 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
18 mpteq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) = ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) )
19 18 oveq2d ⊢ ( 𝑎 = 𝑏 → ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) )
20 19 mpteq2dv ⊢ ( 𝑎 = 𝑏 → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
21 17 20 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑆 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ↔ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) )
22 mpteq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) )
23 fveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑙 ) )
24 23 cbvmptv ⊢ ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) )
25 22 24 eqtrdi ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) ) )
26 25 oveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑆 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑆 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) ) ) )
27 mpteq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) = ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) )
28 27 oveq2d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) )
29 28 mpteq2dv ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
30 26 29 eqeq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑓 } ) → ( ( 𝑆 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ↔ ( 𝑆 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) )
31 mpteq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
32 31 oveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑆 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
33 mpteq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) )
34 33 oveq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) )
35 34 mpteq2dv ⊢ ( 𝑎 = 𝐴 → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
36 32 35 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑆 Σg ( 𝑘 ∈ 𝑎 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑎 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ↔ ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) )
37 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) = ∅
38 37 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) = ∅ )
39 38 oveq2d ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑆 Σg ∅ ) )
40 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
41 40 gsum0 ⊢ ( 𝑆 Σg ∅ ) = ( 0g ‘ 𝑆 )
42 41 a1i ⊢ ( 𝜑 → ( 𝑆 Σg ∅ ) = ( 0g ‘ 𝑆 ) )
43 fconstmpt ⊢ ( 𝐷 × { ( 0g ‘ 𝑅 ) } ) = ( 𝑦 ∈ 𝐷 ↦ ( 0g ‘ 𝑅 ) )
44 3 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
45 5 psrbasfsupp ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
46 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
47 1 4 44 45 46 40 psr0 ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 𝐷 × { ( 0g ‘ 𝑅 ) } ) )
48 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) = ∅
49 48 oveq2i ⊢ ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 𝑅 Σg ∅ )
50 46 gsum0 ⊢ ( 𝑅 Σg ∅ ) = ( 0g ‘ 𝑅 )
51 49 50 eqtri ⊢ ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 0g ‘ 𝑅 )
52 51 a1i ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 0g ‘ 𝑅 ) )
53 52 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 0g ‘ 𝑅 ) ) )
54 43 47 53 3eqtr4a ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
55 39 42 54 3eqtrd ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
56 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
57 5 56 rabex2 ⊢ 𝐷 ∈ V
58 nfv ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) )
59 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ∈ V )
60 eqid ⊢ ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) )
61 58 59 60 fnmptd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) Fn 𝐷 )
62 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ∈ V )
63 eqid ⊢ ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) )
64 58 62 63 fnmptd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) Fn 𝐷 )
65 ofmpteq ⊢ ( ( 𝐷 ∈ V ∧ ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) Fn 𝐷 ∧ ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) Fn 𝐷 ) → ( ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) )
66 57 61 64 65 mp3an2i ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) )
67 66 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) )
68 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
69 1 4 3 psrring ⊢ ( 𝜑 → 𝑆 ∈ Ring )
70 69 ringcmnd ⊢ ( 𝜑 → 𝑆 ∈ CMnd )
71 70 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → 𝑆 ∈ CMnd )
72 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → 𝐴 ∈ Fin )
73 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → 𝑏 ⊆ 𝐴 )
74 72 73 ssfid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → 𝑏 ∈ Fin )
75 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) ∧ 𝑙 ∈ 𝑏 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
76 73 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) ∧ 𝑙 ∈ 𝑏 ) → 𝑙 ∈ 𝐴 )
77 75 76 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) ∧ 𝑙 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑙 ) ∈ 𝐵 )
78 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) )
79 78 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ¬ 𝑓 ∈ 𝑏 )
80 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
81 78 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → 𝑓 ∈ 𝐴 )
82 80 81 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑓 ) ∈ 𝐵 )
83 fveq2 ⊢ ( 𝑙 = 𝑓 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑓 ) )
84 2 68 71 74 77 78 79 82 83 gsumunsn ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑆 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) ) ) = ( ( 𝑆 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑓 ) ) )
85 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
86 77 fmpttd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) : 𝑏 ⟶ 𝐵 )
87 eqid ⊢ ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) = ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) )
88 fvexd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 0g ‘ 𝑆 ) ∈ V )
89 87 74 77 88 fsuppmptdm ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) finSupp ( 0g ‘ 𝑆 ) )
90 2 40 71 74 86 89 gsumcl ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑆 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) ) ∈ 𝐵 )
91 1 2 85 68 90 82 psradd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( ( 𝑆 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑓 ) ) = ( ( 𝑆 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑓 ) ) )
92 23 cbvmptv ⊢ ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) )
93 92 oveq2i ⊢ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑆 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) )
94 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
95 93 94 eqtr3id ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑆 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
96 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
97 1 96 45 2 82 psrelbas ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑓 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
98 97 feqmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝐹 ‘ 𝑓 ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) )
99 95 98 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( ( 𝑆 Σg ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑓 ) ) = ( ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) )
100 84 91 99 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑆 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ∘f ( +g ‘ 𝑅 ) ( 𝑦 ∈ 𝐷 ↦ ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) )
101 3 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
102 101 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑅 ∈ CMnd )
103 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝐴 ∈ Fin )
104 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑏 ⊆ 𝐴 )
105 103 104 ssfid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑏 ∈ Fin )
106 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑘 ∈ 𝑏 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
107 104 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑘 ∈ 𝑏 ) → 𝑘 ∈ 𝐴 )
108 106 107 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑘 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
109 1 96 45 2 108 psrelbas ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑘 ∈ 𝑏 ) → ( 𝐹 ‘ 𝑘 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
110 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑘 ∈ 𝑏 ) → 𝑦 ∈ 𝐷 )
111 109 110 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑘 ∈ 𝑏 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
112 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) )
113 112 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → ¬ 𝑓 ∈ 𝑏 )
114 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
115 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) )
116 115 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → 𝑓 ∈ 𝐴 )
117 114 116 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝐹 ‘ 𝑓 ) ∈ 𝐵 )
118 1 96 45 2 117 psrelbas ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝐹 ‘ 𝑓 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
119 118 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
120 fveq2 ⊢ ( 𝑘 = 𝑓 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑓 ) )
121 120 fveq1d ⊢ ( 𝑘 = 𝑓 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) = ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) )
122 96 85 102 105 111 112 113 119 121 gsumunsn ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ 𝑦 ∈ 𝐷 ) → ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) )
123 122 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) )
124 123 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ( +g ‘ 𝑅 ) ( ( 𝐹 ‘ 𝑓 ) ‘ 𝑦 ) ) ) )
125 67 100 124 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑆 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
126 125 ex ⊢ ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) → ( ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) → ( 𝑆 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) )
127 126 anasss ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ( 𝑆 Σg ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) → ( 𝑆 Σg ( 𝑙 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( 𝐹 ‘ 𝑙 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ ( 𝑏 ∪ { 𝑓 } ) ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) )
128 15 21 30 36 55 127 6 findcard2d ⊢ ( 𝜑 → ( 𝑆 Σg ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
129 9 128 eqtrd ⊢ ( 𝜑 → ( 𝑆 Σg 𝐹 ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )