gsumhashmul

Description: Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024)

	Ref	Expression
Hypotheses	gsumhashmul.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumhashmul.z	⊢ 0 = ( 0_g ‘ 𝐺 )
	gsumhashmul.x	⊢ · = ( ._g ‘ 𝐺 )
	gsumhashmul.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumhashmul.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	gsumhashmul.1	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	gsumhashmul	⊢ ( 𝜑 → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumhashmul.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumhashmul.z	⊢ 0 = ( 0_g ‘ 𝐺 )
3		gsumhashmul.x	⊢ · = ( ._g ‘ 𝐺 )
4		gsumhashmul.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5		gsumhashmul.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6		gsumhashmul.1	⊢ ( 𝜑 → 𝐹 finSupp 0 )
7		suppssdm	⊢ ( 𝐹 supp 0 ) ⊆ dom 𝐹
8	7 5	fssdm	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
9	5 8	feqresmpt	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
10	9	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) = ( 𝐺 Σ_g ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
11		relfsupp	⊢ Rel finSupp
12	11	brrelex1i	⊢ ( 𝐹 finSupp 0 → 𝐹 ∈ V )
13	6 12	syl	⊢ ( 𝜑 → 𝐹 ∈ V )
14	5	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
15	13 14	fndmexd	⊢ ( 𝜑 → 𝐴 ∈ V )
16		ssidd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
17	1 2 4 15 5 16 6	gsumres	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) = ( 𝐺 Σ_g 𝐹 ) )
18		nfcv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) )
19		fveq2	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) )
20	6	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
21		ssidd	⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
22	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
23	8	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝑥 ∈ 𝐴 )
24	22 23	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
25	5	ffund	⊢ ( 𝜑 → Fun 𝐹 )
26		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
27		reldif	⊢ ( Rel 𝐹 → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
28	25 26 27	3syl	⊢ ( 𝜑 → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
29		1stdm	⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 1^st ‘ 𝑧 ) ∈ dom ( 𝐹 ∖ ( V × { 0 } ) ) )
30	28 29	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 1^st ‘ 𝑧 ) ∈ dom ( 𝐹 ∖ ( V × { 0 } ) ) )
31	2	fvexi	⊢ 0 ∈ V
32	31	a1i	⊢ ( 𝜑 → 0 ∈ V )
33		fressupp	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 ∖ ( V × { 0 } ) ) )
34	25 13 32 33	syl3anc	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 ∖ ( V × { 0 } ) ) )
35	34	dmeqd	⊢ ( 𝜑 → dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = dom ( 𝐹 ∖ ( V × { 0 } ) ) )
36	7	a1i	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ dom 𝐹 )
37		ssdmres	⊢ ( ( 𝐹 supp 0 ) ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) )
38	36 37	sylib	⊢ ( 𝜑 → dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 supp 0 ) )
39	35 38	eqtr3d	⊢ ( 𝜑 → dom ( 𝐹 ∖ ( V × { 0 } ) ) = ( 𝐹 supp 0 ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → dom ( 𝐹 ∖ ( V × { 0 } ) ) = ( 𝐹 supp 0 ) )
41	30 40	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 1^st ‘ 𝑧 ) ∈ ( 𝐹 supp 0 ) )
42	25	funresd	⊢ ( 𝜑 → Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
44	38	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ 𝑥 ∈ ( 𝐹 supp 0 ) ) )
45	44	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝑥 ∈ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
46		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → 𝑥 ∈ ( 𝐹 supp 0 ) )
47	46	fvresd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
48		funopfvb	⊢ ( ( Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) )
49	48	biimpa	⊢ ( ( ( Fun ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) ∧ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
50	43 45 47 49	syl21anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
51	34	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 ∖ ( V × { 0 } ) ) )
52	50 51	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
53		eqeq2	⊢ ( 𝑣 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → ( 𝑧 = 𝑣 ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
54	53	bibi2d	⊢ ( 𝑣 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → ( ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) ↔ ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
55	54	ralbidv	⊢ ( 𝑣 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ → ( ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) ↔ ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
56	55	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑣 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) → ( ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) ↔ ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ) )
57		fvexd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → ( 2^nd ‘ 𝑧 ) ∈ V )
58	28	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
59		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
60		1st2nd	⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
61	58 59 60	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
62		opeq1	⊢ ( 𝑥 = ( 1^st ‘ 𝑧 ) → ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
63	62	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
64	61 63	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝑧 = ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ )
65		difssd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ∖ ( V × { 0 } ) ) ⊆ 𝐹 )
66	65	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → 𝑧 ∈ 𝐹 )
67	66	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝑧 ∈ 𝐹 )
68	64 67	eqeltrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐹 )
69	64 68	jca	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → ( 𝑧 = ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐹 ) )
70		opeq2	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ )
71	70	eqeq2d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ) )
72	70	eleq1d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ↔ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐹 ) )
73	71 72	anbi12d	⊢ ( 𝑦 = ( 2^nd ‘ 𝑧 ) → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) ↔ ( 𝑧 = ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ⟨ 𝑥 , ( 2^nd ‘ 𝑧 ) ⟩ ∈ 𝐹 ) ) )
74	57 69 73	spcedv	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
75		vex	⊢ 𝑥 ∈ V
76	75	elsnres	⊢ ( 𝑧 ∈ ( 𝐹 ↾ { 𝑥 } ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
77	74 76	sylibr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝑧 ∈ ( 𝐹 ↾ { 𝑥 } ) )
78	14	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝐹 Fn 𝐴 )
79	23	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝑥 ∈ 𝐴 )
80		fnressn	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
81	78 79 80	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → ( 𝐹 ↾ { 𝑥 } ) = { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
82	77 81	eleqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝑧 ∈ { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } )
83		elsni	⊢ ( 𝑧 ∈ { ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ } → 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
84	82 83	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑥 = ( 1^st ‘ 𝑧 ) ) → 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
85		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) → 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
86	85	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) → ( 1^st ‘ 𝑧 ) = ( 1^st ‘ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
87		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
88	75 87	op1st	⊢ ( 1^st ‘ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) = 𝑥
89	86 88	eqtr2di	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) → 𝑥 = ( 1^st ‘ 𝑧 ) )
90	84 89	impbida	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
91	90	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
92	52 56 91	rspcedvd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ∃ 𝑣 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) )
93		reu6	⊢ ( ∃! 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) 𝑥 = ( 1^st ‘ 𝑧 ) ↔ ∃ 𝑣 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∀ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ( 𝑥 = ( 1^st ‘ 𝑧 ) ↔ 𝑧 = 𝑣 ) )
94	92 93	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 supp 0 ) ) → ∃! 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) 𝑥 = ( 1^st ‘ 𝑧 ) )
95	18 1 2 19 4 20 21 24 41 94	gsummptf1o	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑥 ∈ ( 𝐹 supp 0 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐺 Σ_g ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ) ) )
96	10 17 95	3eqtr3d	⊢ ( 𝜑 → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ) ) )
97		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
98	97	eldifad	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → 𝑧 ∈ 𝐹 )
99		funfv1st2nd	⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ 𝐹 ) → ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) = ( 2^nd ‘ 𝑧 ) )
100	25 98 99	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) = ( 2^nd ‘ 𝑧 ) )
101	100	mpteq2dva	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 2^nd ‘ 𝑧 ) ) )
102	101	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 𝐹 ‘ ( 1^st ‘ 𝑧 ) ) ) ) = ( 𝐺 Σ_g ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 2^nd ‘ 𝑧 ) ) ) )
103	96 102	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 2^nd ‘ 𝑧 ) ) ) )
104		nfcv	⊢ Ⅎ 𝑧 ( 1^st ‘ 𝑡 )
105		fvex	⊢ ( 2^nd ‘ 𝑡 ) ∈ V
106		fvex	⊢ ( 1^st ‘ 𝑡 ) ∈ V
107	105 106	op2ndd	⊢ ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ → ( 2^nd ‘ 𝑧 ) = ( 1^st ‘ 𝑡 ) )
108		resfnfinfin	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐹 supp 0 ) ∈ Fin ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
109	14 20 108	syl2anc	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
110	34 109	eqeltrrd	⊢ ( 𝜑 → ( 𝐹 ∖ ( V × { 0 } ) ) ∈ Fin )
111	34	rneqd	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ran ( 𝐹 ∖ ( V × { 0 } ) ) )
112		rnresss	⊢ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ⊆ ran 𝐹
113	5	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
114	112 113	sstrid	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ⊆ 𝐵 )
115	111 114	eqsstrrd	⊢ ( 𝜑 → ran ( 𝐹 ∖ ( V × { 0 } ) ) ⊆ 𝐵 )
116		2ndrn	⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 2^nd ‘ 𝑧 ) ∈ ran ( 𝐹 ∖ ( V × { 0 } ) ) )
117	28 116	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ( 2^nd ‘ 𝑧 ) ∈ ran ( 𝐹 ∖ ( V × { 0 } ) ) )
118		relcnv	⊢ Rel ^◡ 𝐹
119		reldif	⊢ ( Rel ^◡ 𝐹 → Rel ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) )
120	118 119	mp1i	⊢ ( 𝜑 → Rel ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) )
121		1st2nd	⊢ ( ( Rel ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) → 𝑡 = ⟨ ( 1^st ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ )
122	120 121	sylan	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) → 𝑡 = ⟨ ( 1^st ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ )
123		cnvdif	⊢ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) = ( ^◡ 𝐹 ∖ ^◡ ( V × { 0 } ) )
124		cnvxp	⊢ ^◡ ( V × { 0 } ) = ( { 0 } × V )
125	124	difeq2i	⊢ ( ^◡ 𝐹 ∖ ^◡ ( V × { 0 } ) ) = ( ^◡ 𝐹 ∖ ( { 0 } × V ) )
126	123 125	eqtri	⊢ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) = ( ^◡ 𝐹 ∖ ( { 0 } × V ) )
127	126	eqimss2i	⊢ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ^◡ ( 𝐹 ∖ ( V × { 0 } ) )
128	127	a1i	⊢ ( 𝜑 → ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
129	128	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) → 𝑡 ∈ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
130	122 129	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) → ⟨ ( 1^st ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ ∈ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
131	106 105	opelcnv	⊢ ( ⟨ ( 1^st ‘ 𝑡 ) , ( 2^nd ‘ 𝑡 ) ⟩ ∈ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) ↔ ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
132	130 131	sylib	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) → ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
133	28	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
134		eqidd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∪ ^◡ { 𝑧 } = ∪ ^◡ { 𝑧 } )
135		cnvf1olem	⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ∪ ^◡ { 𝑧 } = ∪ ^◡ { 𝑧 } ) ) → ( ∪ ^◡ { 𝑧 } ∈ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 = ∪ ^◡ { ∪ ^◡ { 𝑧 } } ) )
136	135	simpld	⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ∪ ^◡ { 𝑧 } = ∪ ^◡ { 𝑧 } ) ) → ∪ ^◡ { 𝑧 } ∈ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
137	133 97 134 136	syl12anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∪ ^◡ { 𝑧 } ∈ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
138	137 126	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∪ ^◡ { 𝑧 } ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) )
139		eqeq2	⊢ ( 𝑢 = ∪ ^◡ { 𝑧 } → ( 𝑡 = 𝑢 ↔ 𝑡 = ∪ ^◡ { 𝑧 } ) )
140	139	bibi2d	⊢ ( 𝑢 = ∪ ^◡ { 𝑧 } → ( ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) ↔ ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ^◡ { 𝑧 } ) ) )
141	140	ralbidv	⊢ ( 𝑢 = ∪ ^◡ { 𝑧 } → ( ∀ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) ↔ ∀ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ^◡ { 𝑧 } ) ) )
142	141	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑢 = ∪ ^◡ { 𝑧 } ) → ( ∀ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) ↔ ∀ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ^◡ { 𝑧 } ) ) )
143	118 119	mp1i	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ) → Rel ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) )
144		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ) → 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) )
145		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ) → 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ )
146		df-rel	⊢ ( Rel ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ↔ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ( V × V ) )
147	120 146	sylib	⊢ ( 𝜑 → ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ( V × V ) )
148	147	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ) → ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ( V × V ) )
149	148 144	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ) → 𝑡 ∈ ( V × V ) )
150		2nd1st	⊢ ( 𝑡 ∈ ( V × V ) → ∪ ^◡ { 𝑡 } = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ )
151	149 150	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ) → ∪ ^◡ { 𝑡 } = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ )
152	145 151	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ) → 𝑧 = ∪ ^◡ { 𝑡 } )
153		cnvf1olem	⊢ ( ( Rel ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ ( 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ 𝑧 = ∪ ^◡ { 𝑡 } ) ) → ( 𝑧 ∈ ^◡ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) )
154	153	simprd	⊢ ( ( Rel ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ ( 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ∧ 𝑧 = ∪ ^◡ { 𝑡 } ) ) → 𝑡 = ∪ ^◡ { 𝑧 } )
155	143 144 152 154	syl12anc	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ) → 𝑡 = ∪ ^◡ { 𝑧 } )
156	28	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → Rel ( 𝐹 ∖ ( V × { 0 } ) ) )
157	97	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) )
158		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → 𝑡 = ∪ ^◡ { 𝑧 } )
159		cnvf1olem	⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) ) → ( 𝑡 ∈ ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑧 = ∪ ^◡ { 𝑡 } ) )
160	159	simprd	⊢ ( ( Rel ( 𝐹 ∖ ( V × { 0 } ) ) ∧ ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) ) → 𝑧 = ∪ ^◡ { 𝑡 } )
161	156 157 158 160	syl12anc	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → 𝑧 = ∪ ^◡ { 𝑡 } )
162	147	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ⊆ ( V × V ) )
163		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) )
164	162 163	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → 𝑡 ∈ ( V × V ) )
165	164 150	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → ∪ ^◡ { 𝑡 } = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ )
166	161 165	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) ∧ 𝑡 = ∪ ^◡ { 𝑧 } ) → 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ )
167	155 166	impbida	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) ∧ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ) → ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ^◡ { 𝑧 } ) )
168	167	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∀ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = ∪ ^◡ { 𝑧 } ) )
169	138 142 168	rspcedvd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∃ 𝑢 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ∀ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) )
170		reu6	⊢ ( ∃! 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ ∃ 𝑢 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ∀ 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ( 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ ↔ 𝑡 = 𝑢 ) )
171	169 170	sylibr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ) → ∃! 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) 𝑧 = ⟨ ( 2^nd ‘ 𝑡 ) , ( 1^st ‘ 𝑡 ) ⟩ )
172	104 1 2 107 4 110 115 117 132 171	gsummptf1o	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑧 ∈ ( 𝐹 ∖ ( V × { 0 } ) ) ↦ ( 2^nd ‘ 𝑧 ) ) ) = ( 𝐺 Σ_g ( 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1^st ‘ 𝑡 ) ) ) )
173		fveq2	⊢ ( 𝑡 = 𝑧 → ( 1^st ‘ 𝑡 ) = ( 1^st ‘ 𝑧 ) )
174	173	cbvmptv	⊢ ( 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1^st ‘ 𝑡 ) ) = ( 𝑧 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1^st ‘ 𝑧 ) )
175	34	cnveqd	⊢ ( 𝜑 → ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ^◡ ( 𝐹 ∖ ( V × { 0 } ) ) )
176	175 126	eqtr2di	⊢ ( 𝜑 → ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) = ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
177	176	mpteq1d	⊢ ( 𝜑 → ( 𝑧 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1^st ‘ 𝑧 ) ) = ( 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1^st ‘ 𝑧 ) ) )
178	174 177	eqtrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1^st ‘ 𝑡 ) ) = ( 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1^st ‘ 𝑧 ) ) )
179	178	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑡 ∈ ( ^◡ 𝐹 ∖ ( { 0 } × V ) ) ↦ ( 1^st ‘ 𝑡 ) ) ) = ( 𝐺 Σ_g ( 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1^st ‘ 𝑧 ) ) ) )
180	103 172 179	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1^st ‘ 𝑧 ) ) ) )
181		nfcv	⊢ Ⅎ 𝑦 ( 1^st ‘ 𝑧 )
182		nfv	⊢ Ⅎ 𝑥 𝜑
183		vex	⊢ 𝑦 ∈ V
184	75 183	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑥 )
185		relcnv	⊢ Rel ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) )
186	185	a1i	⊢ ( 𝜑 → Rel ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
187		cnvfi	⊢ ( ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin → ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
188	109 187	syl	⊢ ( 𝜑 → ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
189	113	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ran 𝐹 ⊆ 𝐵 )
190	185	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → Rel ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
191		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
192		1stdm	⊢ ( ( Rel ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∧ 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1^st ‘ 𝑧 ) ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
193	190 191 192	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1^st ‘ 𝑧 ) ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
194		df-rn	⊢ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) )
195	193 194	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1^st ‘ 𝑧 ) ∈ ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) )
196	112 195	sselid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1^st ‘ 𝑧 ) ∈ ran 𝐹 )
197	189 196	sseldd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 1^st ‘ 𝑧 ) ∈ 𝐵 )
198	181 182 1 184 186 188 4 197	gsummpt2d	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑧 ∈ ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 1^st ‘ 𝑧 ) ) ) = ( 𝐺 Σ_g ( 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 𝐺 Σ_g ( 𝑦 ∈ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) ) ) )
199		df-ima	⊢ ( 𝐹 “ ( 𝐹 supp 0 ) ) = ran ( 𝐹 ↾ ( 𝐹 supp 0 ) )
200		supppreima	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 0 ∈ V ) → ( 𝐹 supp 0 ) = ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
201	25 13 32 200	syl3anc	⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
202	201	imaeq2d	⊢ ( 𝜑 → ( 𝐹 “ ( 𝐹 supp 0 ) ) = ( 𝐹 “ ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) ) )
203	199 202	eqtr3id	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( 𝐹 “ ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) ) )
204		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) ) = ( ( ran 𝐹 ∖ { 0 } ) ∩ ran 𝐹 ) )
205	25 204	syl	⊢ ( 𝜑 → ( 𝐹 “ ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) ) = ( ( ran 𝐹 ∖ { 0 } ) ∩ ran 𝐹 ) )
206		difssd	⊢ ( 𝜑 → ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 )
207		dfss2	⊢ ( ( ran 𝐹 ∖ { 0 } ) ⊆ ran 𝐹 ↔ ( ( ran 𝐹 ∖ { 0 } ) ∩ ran 𝐹 ) = ( ran 𝐹 ∖ { 0 } ) )
208	206 207	sylib	⊢ ( 𝜑 → ( ( ran 𝐹 ∖ { 0 } ) ∩ ran 𝐹 ) = ( ran 𝐹 ∖ { 0 } ) )
209	203 205 208	3eqtrd	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) )
210	194 209	eqtr3id	⊢ ( 𝜑 → dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) = ( ran 𝐹 ∖ { 0 } ) )
211	4	cmnmndd	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
212	211	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → 𝐺 ∈ Mnd )
213	109	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin )
214		imafi2	⊢ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ∈ Fin → ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ∈ Fin )
215	213 187 214	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ∈ Fin )
216	194 114	eqsstrrid	⊢ ( 𝜑 → dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ⊆ 𝐵 )
217	216	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → 𝑥 ∈ 𝐵 )
218	1 3	gsumconst	⊢ ( ( 𝐺 ∈ Mnd ∧ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ∈ Fin ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 Σ_g ( 𝑦 ∈ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) = ( ( ♯ ‘ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ) · 𝑥 ) )
219	212 215 217 218	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σ_g ( 𝑦 ∈ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) = ( ( ♯ ‘ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ) · 𝑥 ) )
220		cnvresima	⊢ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) = ( ( ^◡ 𝐹 “ { 𝑥 } ) ∩ ( 𝐹 supp 0 ) )
221	210	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↔ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) )
222	221	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) )
223	222	snssd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → { 𝑥 } ⊆ ( ran 𝐹 ∖ { 0 } ) )
224		sspreima	⊢ ( ( Fun 𝐹 ∧ { 𝑥 } ⊆ ( ran 𝐹 ∖ { 0 } ) ) → ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
225	25 223 224	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
226	201	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐹 supp 0 ) = ( ^◡ 𝐹 “ ( ran 𝐹 ∖ { 0 } ) ) )
227	225 226	sseqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ( 𝐹 supp 0 ) )
228		dfss2	⊢ ( ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ( 𝐹 supp 0 ) ↔ ( ( ^◡ 𝐹 “ { 𝑥 } ) ∩ ( 𝐹 supp 0 ) ) = ( ^◡ 𝐹 “ { 𝑥 } ) )
229	227 228	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ( ^◡ 𝐹 “ { 𝑥 } ) ∩ ( 𝐹 supp 0 ) ) = ( ^◡ 𝐹 “ { 𝑥 } ) )
230	220 229	eqtr2id	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ^◡ 𝐹 “ { 𝑥 } ) = ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) )
231	230	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ♯ ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) = ( ♯ ‘ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ) )
232	231	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( ( ♯ ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) = ( ( ♯ ‘ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ) · 𝑥 ) )
233	219 232	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ) → ( 𝐺 Σ_g ( 𝑦 ∈ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) = ( ( ♯ ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) )
234	210 233	mpteq12dva	⊢ ( 𝜑 → ( 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 𝐺 Σ_g ( 𝑦 ∈ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) ) = ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) ) )
235	234	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑥 ∈ dom ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) ↦ ( 𝐺 Σ_g ( 𝑦 ∈ ( ^◡ ( 𝐹 ↾ ( 𝐹 supp 0 ) ) “ { 𝑥 } ) ↦ 𝑥 ) ) ) ) = ( 𝐺 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) ) ) )
236	180 198 235	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σ_g 𝐹 ) = ( 𝐺 Σ_g ( 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ↦ ( ( ♯ ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) · 𝑥 ) ) ) )

Metamath Proof Explorer

Theorem gsumhashmul

Proof