gsummpt2d

Description: Express a finite sum over a two-dimensional range as a double sum. See also gsum2d . (Contributed by Thierry Arnoux, 27-Apr-2020)

	Ref	Expression
Hypotheses	gsummpt2d.c	⊢ Ⅎ 𝑧 𝐶
	gsummpt2d.0	⊢ Ⅎ 𝑦 𝜑
	gsummpt2d.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	gsummpt2d.1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → 𝐶 = 𝐷 )
	gsummpt2d.r	⊢ ( 𝜑 → Rel 𝐴 )
	gsummpt2d.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsummpt2d.m	⊢ ( 𝜑 → 𝑊 ∈ CMnd )
	gsummpt2d.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
Assertion	gsummpt2d	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑊 Σ_g ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummpt2d.c	⊢ Ⅎ 𝑧 𝐶
2		gsummpt2d.0	⊢ Ⅎ 𝑦 𝜑
3		gsummpt2d.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
4		gsummpt2d.1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → 𝐶 = 𝐷 )
5		gsummpt2d.r	⊢ ( 𝜑 → Rel 𝐴 )
6		gsummpt2d.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
7		gsummpt2d.m	⊢ ( 𝜑 → 𝑊 ∈ CMnd )
8		gsummpt2d.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
9		eqid	⊢ ( 0_g ‘ 𝑊 ) = ( 0_g ‘ 𝑊 )
10	6	dmexd	⊢ ( 𝜑 → dom 𝐴 ∈ V )
11		1stdm	⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 1^st ‘ 𝑥 ) ∈ dom 𝐴 )
12	5 11	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1^st ‘ 𝑥 ) ∈ dom 𝐴 )
13		fo1st	⊢ 1^st : V –onto→ V
14		fofn	⊢ ( 1^st : V –onto→ V → 1^st Fn V )
15		dffn5	⊢ ( 1^st Fn V ↔ 1^st = ( 𝑥 ∈ V ↦ ( 1^st ‘ 𝑥 ) ) )
16	15	biimpi	⊢ ( 1^st Fn V → 1^st = ( 𝑥 ∈ V ↦ ( 1^st ‘ 𝑥 ) ) )
17	13 14 16	mp2b	⊢ 1^st = ( 𝑥 ∈ V ↦ ( 1^st ‘ 𝑥 ) )
18	17	reseq1i	⊢ ( 1^st ↾ 𝐴 ) = ( ( 𝑥 ∈ V ↦ ( 1^st ‘ 𝑥 ) ) ↾ 𝐴 )
19		ssv	⊢ 𝐴 ⊆ V
20		resmpt	⊢ ( 𝐴 ⊆ V → ( ( 𝑥 ∈ V ↦ ( 1^st ‘ 𝑥 ) ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) ) )
21	19 20	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ( 1^st ‘ 𝑥 ) ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) )
22	18 21	eqtri	⊢ ( 1^st ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 1^st ‘ 𝑥 ) )
23	3 9 7 6 10 8 12 22	gsummpt2co	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑊 Σ_g ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) ) ) )
24	7	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → 𝑊 ∈ CMnd )
25	6	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → 𝐴 ∈ Fin )
26		imaexg	⊢ ( 𝐴 ∈ Fin → ( 𝐴 “ { 𝑦 } ) ∈ V )
27	25 26	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝐴 “ { 𝑦 } ) ∈ V )
28	4	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) → 𝐶 = 𝐷 )
29		simp-4l	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) → 𝜑 )
30		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) → 𝑥 ∈ 𝐴 )
31	29 30 8	syl2anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) → 𝐶 ∈ 𝐵 )
32	28 31	eqeltrrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) → 𝐷 ∈ 𝐵 )
33		vex	⊢ 𝑦 ∈ V
34		vex	⊢ 𝑧 ∈ V
35	33 34	elimasn	⊢ ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 )
36	35	biimpi	⊢ ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 )
37	36	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐴 )
38		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) → 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ )
39	38	eqeq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) → ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ↔ ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑧 ⟩ ) )
40		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑧 ⟩ )
41	37 39 40	rspcedvd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) → ∃ 𝑥 ∈ 𝐴 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ )
42	32 41	r19.29a	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ) → 𝐷 ∈ 𝐵 )
43	42	fmpttd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) : ( 𝐴 “ { 𝑦 } ) ⟶ 𝐵 )
44		eqid	⊢ ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) = ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 )
45		imafi2	⊢ ( 𝐴 ∈ Fin → ( 𝐴 “ { 𝑦 } ) ∈ Fin )
46	6 45	syl	⊢ ( 𝜑 → ( 𝐴 “ { 𝑦 } ) ∈ Fin )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝐴 “ { 𝑦 } ) ∈ Fin )
48		fvex	⊢ ( 0_g ‘ 𝑊 ) ∈ V
49	48	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 0_g ‘ 𝑊 ) ∈ V )
50	44 47 42 49	fsuppmptdm	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) finSupp ( 0_g ‘ 𝑊 ) )
51		2ndconst	⊢ ( 𝑦 ∈ dom 𝐴 → ( 2^nd ↾ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) )
52	51	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 2^nd ↾ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) )
53		1stpreimas	⊢ ( ( Rel 𝐴 ∧ 𝑦 ∈ dom 𝐴 ) → ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) = ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) )
54	5 53	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) = ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) )
55	54	reseq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 2^nd ↾ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ) )
56	55	f1oeq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) ↔ ( 2^nd ↾ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) ) )
57	52 56	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) )
58	3 9 24 27 43 50 57	gsumf1o	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) = ( 𝑊 Σ_g ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ∘ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ) ) )
59		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) )
60	54	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) = ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) )
61	59 60	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) )
62		xp2nd	⊢ ( 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 “ { 𝑦 } ) )
63	61 62	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 “ { 𝑦 } ) )
64	63	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ∀ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 “ { 𝑦 } ) )
65		fo2nd	⊢ 2^nd : V –onto→ V
66		fofn	⊢ ( 2^nd : V –onto→ V → 2^nd Fn V )
67		dffn5	⊢ ( 2^nd Fn V ↔ 2^nd = ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) )
68	67	biimpi	⊢ ( 2^nd Fn V → 2^nd = ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) )
69	65 66 68	mp2b	⊢ 2^nd = ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) )
70	69	reseq1i	⊢ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) )
71		ssv	⊢ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ⊆ V
72		resmpt	⊢ ( ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ⊆ V → ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ( 2^nd ‘ 𝑥 ) ) )
73	71 72	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ( 2^nd ‘ 𝑥 ) )
74	70 73	eqtri	⊢ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ( 2^nd ‘ 𝑥 ) )
75	74	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ( 2^nd ‘ 𝑥 ) ) )
76		eqidd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) = ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) )
77	64 75 76	fmptcos	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ∘ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ⦋ ( 2^nd ‘ 𝑥 ) / 𝑧 ⦌ 𝐷 ) )
78		nfv	⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) )
79	1	a1i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → Ⅎ 𝑧 𝐶 )
80	61	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) )
81		xp1st	⊢ ( 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) → ( 1^st ‘ 𝑥 ) ∈ { 𝑦 } )
82	80 81	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → ( 1^st ‘ 𝑥 ) ∈ { 𝑦 } )
83		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
84	83	elsn	⊢ ( ( 1^st ‘ 𝑥 ) ∈ { 𝑦 } ↔ ( 1^st ‘ 𝑥 ) = 𝑦 )
85	82 84	sylib	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → ( 1^st ‘ 𝑥 ) = 𝑦 )
86		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝑧 = ( 2^nd ‘ 𝑥 ) )
87	86	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → ( 2^nd ‘ 𝑥 ) = 𝑧 )
88		eqopi	⊢ ( ( 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ∧ ( ( 1^st ‘ 𝑥 ) = 𝑦 ∧ ( 2^nd ‘ 𝑥 ) = 𝑧 ) ) → 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ )
89	80 85 87 88	syl12anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ )
90	89 4	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝐶 = 𝐷 )
91	90	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝐷 = 𝐶 )
92	78 79 63 91	csbiedf	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → ⦋ ( 2^nd ‘ 𝑥 ) / 𝑧 ⦌ 𝐷 = 𝐶 )
93	92	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ⦋ ( 2^nd ‘ 𝑥 ) / 𝑧 ⦌ 𝐷 ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) )
94	77 93	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ∘ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) )
95	94	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑊 Σ_g ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ∘ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ) ) = ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) )
96	58 95	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) = ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) )
97	2 96	mpteq2da	⊢ ( 𝜑 → ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) ) = ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) ) )
98	97	oveq2d	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) ) ) = ( 𝑊 Σ_g ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) ) ) )
99	23 98	eqtrd	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑊 Σ_g ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) ) ) )

Metamath Proof Explorer

Theorem gsummpt2d

Proof