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	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_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	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_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	⊢ ( 0_g ‘ 𝑆 ) = ( 0_g ‘ 𝑆 )
41	40	gsum0	⊢ ( 𝑆 Σ_g ∅ ) = ( 0_g ‘ 𝑆 )
42	41	a1i	⊢ ( 𝜑 → ( 𝑆 Σ_g ∅ ) = ( 0_g ‘ 𝑆 ) )
43		fconstmpt	⊢ ( 𝐷 × { ( 0_g ‘ 𝑅 ) } ) = ( 𝑦 ∈ 𝐷 ↦ ( 0_g ‘ 𝑅 ) )
44	3	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
45	5	psrbasfsupp	⊢ 𝐷 = { ℎ ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
46		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
47	1 4 44 45 46 40	psr0	⊢ ( 𝜑 → ( 0_g ‘ 𝑆 ) = ( 𝐷 × { ( 0_g ‘ 𝑅 ) } ) )
48		mpt0	⊢ ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) = ∅
49	48	oveq2i	⊢ ( 𝑅 Σ_g ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 𝑅 Σ_g ∅ )
50	46	gsum0	⊢ ( 𝑅 Σ_g ∅ ) = ( 0_g ‘ 𝑅 )
51	49 50	eqtri	⊢ ( 𝑅 Σ_g ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 0_g ‘ 𝑅 )
52	51	a1i	⊢ ( 𝜑 → ( 𝑅 Σ_g ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) = ( 0_g ‘ 𝑅 ) )
53	52	mpteq2dv	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 0_g ‘ 𝑅 ) ) )
54	43 47 53	3eqtr4a	⊢ ( 𝜑 → ( 0_g ‘ 𝑆 ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
55	39 42 54	3eqtrd	⊢ ( 𝜑 → ( 𝑆 Σ_g ( 𝑘 ∈ ∅ ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ ∅ ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
56		ovex	⊢ ( ℕ₀ ↑_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 ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 0_g ‘ 𝑆 ) ∈ V )
89	87 74 77 88	fsuppmptdm	⊢ ( ( ( ( 𝜑 ∧ 𝑏 ⊆ 𝐴 ) ∧ 𝑓 ∈ ( 𝐴 ∖ 𝑏 ) ) ∧ ( 𝑆 Σ_g ( 𝑘 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σ_g ( 𝑘 ∈ 𝑏 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) ) → ( 𝑙 ∈ 𝑏 ↦ ( 𝐹 ‘ 𝑙 ) ) finSupp ( 0_g ‘ 𝑆 ) )
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 ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )

Metamath Proof Explorer

Theorem psrgsum

Proof