gsumhashmul

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

	Ref	Expression
Hypotheses	gsumhashmul.b	$⊢ B = {Base}_{G}$
	gsumhashmul.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsumhashmul.x	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	gsumhashmul.g	$⊢ φ \to G \in CMnd$
	gsumhashmul.f	$⊢ φ \to F : A ⟶ B$
	gsumhashmul.1	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
Assertion	gsumhashmul	$⊢ φ \to \sum_{G} F = \underset{x \in ran F ∖ \{\underset{˙}{0}\}}{\sum_{G}} (\|F^{-1} [\{x\}]\| \underset{˙}{\cdot} x)$

Proof

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

Metamath Proof Explorer

Theorem gsumhashmul

Proof