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		f1oeq1	⊢ ( ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 2^nd ↾ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ) → ( ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) ↔ ( 2^nd ↾ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) ) )
57	55 56	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) ↔ ( 2^nd ↾ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) ) )
58	52 57	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) : ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑦 } ) )
59	3 9 24 27 43 50 58	gsumf1o	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) = ( 𝑊 Σ_g ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ∘ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ) ) )
60		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) )
61	54	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) = ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) )
62	60 61	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) )
63		xp2nd	⊢ ( 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 “ { 𝑦 } ) )
64	62 63	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 “ { 𝑦 } ) )
65	64	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ∀ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 “ { 𝑦 } ) )
66		fo2nd	⊢ 2^nd : V –onto→ V
67		fofn	⊢ ( 2^nd : V –onto→ V → 2^nd Fn V )
68		dffn5	⊢ ( 2^nd Fn V ↔ 2^nd = ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) )
69	68	biimpi	⊢ ( 2^nd Fn V → 2^nd = ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) )
70	66 67 69	mp2b	⊢ 2^nd = ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) )
71	70	reseq1i	⊢ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) )
72		ssv	⊢ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ⊆ V
73		resmpt	⊢ ( ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ⊆ V → ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ( 2^nd ‘ 𝑥 ) ) )
74	72 73	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ( 2^nd ‘ 𝑥 ) )
75	71 74	eqtri	⊢ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ( 2^nd ‘ 𝑥 ) )
76	75	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ( 2^nd ‘ 𝑥 ) ) )
77		eqidd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) = ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) )
78	65 76 77	fmptcos	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ∘ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ⦋ ( 2^nd ‘ 𝑥 ) / 𝑧 ⦌ 𝐷 ) )
79		nfv	⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) )
80	1	a1i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → Ⅎ 𝑧 𝐶 )
81	62	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) )
82		xp1st	⊢ ( 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) → ( 1^st ‘ 𝑥 ) ∈ { 𝑦 } )
83	81 82	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → ( 1^st ‘ 𝑥 ) ∈ { 𝑦 } )
84		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
85	84	elsn	⊢ ( ( 1^st ‘ 𝑥 ) ∈ { 𝑦 } ↔ ( 1^st ‘ 𝑥 ) = 𝑦 )
86	83 85	sylib	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → ( 1^st ‘ 𝑥 ) = 𝑦 )
87		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝑧 = ( 2^nd ‘ 𝑥 ) )
88	87	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → ( 2^nd ‘ 𝑥 ) = 𝑧 )
89		eqopi	⊢ ( ( 𝑥 ∈ ( { 𝑦 } × ( 𝐴 “ { 𝑦 } ) ) ∧ ( ( 1^st ‘ 𝑥 ) = 𝑦 ∧ ( 2^nd ‘ 𝑥 ) = 𝑧 ) ) → 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ )
90	81 86 88 89	syl12anc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ )
91	90 4	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝐶 = 𝐷 )
92	91	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ∧ 𝑧 = ( 2^nd ‘ 𝑥 ) ) → 𝐷 = 𝐶 )
93	79 80 64 92	csbiedf	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) ∧ 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) → ⦋ ( 2^nd ‘ 𝑥 ) / 𝑧 ⦌ 𝐷 = 𝐶 )
94	93	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ ⦋ ( 2^nd ‘ 𝑥 ) / 𝑧 ⦌ 𝐷 ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) )
95	78 94	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ∘ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ) = ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) )
96	95	oveq2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑊 Σ_g ( ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ∘ ( 2^nd ↾ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ) ) ) = ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) )
97	59 96	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) = ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) )
98	2 97	mpteq2da	⊢ ( 𝜑 → ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) ) = ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) ) )
99	98	oveq2d	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑥 ∈ ( ^◡ ( 1^st ↾ 𝐴 ) “ { 𝑦 } ) ↦ 𝐶 ) ) ) ) = ( 𝑊 Σ_g ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) ) ) )
100	23 99	eqtrd	⊢ ( 𝜑 → ( 𝑊 Σ_g ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑊 Σ_g ( 𝑦 ∈ dom 𝐴 ↦ ( 𝑊 Σ_g ( 𝑧 ∈ ( 𝐴 “ { 𝑦 } ) ↦ 𝐷 ) ) ) ) )

Metamath Proof Explorer

Theorem gsummpt2d

Proof