dmdprdsplitlem

Description: Lemma for dmdprdsplit . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 14-Jul-2019)

	Ref	Expression
Hypotheses	dmdprdsplitlem.0	$⊢ \underset{˙}{0} = 0_{G}$
	dmdprdsplitlem.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
	dmdprdsplitlem.1	$⊢ φ \to G dom DProd S$
	dmdprdsplitlem.2	$⊢ φ \to dom S = I$
	dmdprdsplitlem.3	$⊢ φ \to A \subseteq I$
	dmdprdsplitlem.4	$⊢ φ \to F \in W$
	dmdprdsplitlem.5	$⊢ φ \to \sum_{G} F \in (G DProd ({S ↾}_{A}))$
Assertion	dmdprdsplitlem	$⊢ (φ \land X \in (I ∖ A)) \to F (X) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		dmdprdsplitlem.0	$⊢ \underset{˙}{0} = 0_{G}$
2		dmdprdsplitlem.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
3		dmdprdsplitlem.1	$⊢ φ \to G dom DProd S$
4		dmdprdsplitlem.2	$⊢ φ \to dom S = I$
5		dmdprdsplitlem.3	$⊢ φ \to A \subseteq I$
6		dmdprdsplitlem.4	$⊢ φ \to F \in W$
7		dmdprdsplitlem.5	$⊢ φ \to \sum_{G} F \in (G DProd ({S ↾}_{A}))$
8	3 4	dprdf2	$⊢ φ \to S : I ⟶ SubGrp (G)$
9	8 5	fssresd	$⊢ φ \to ({S ↾}_{A}) : A ⟶ SubGrp (G)$
10		fdm	$⊢ ({S ↾}_{A}) : A ⟶ SubGrp (G) \to dom ({S ↾}_{A}) = A$
11		eqid	$⊢ \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} = \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
12	1 11	eldprd	$⊢ dom ({S ↾}_{A}) = A \to (\sum_{G} F \in (G DProd ({S ↾}_{A})) \leftrightarrow (G dom DProd ({S ↾}_{A}) \land \exists f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \sum_{G} F = \sum_{G} f))$
13	9 10 12	3syl	$⊢ φ \to (\sum_{G} F \in (G DProd ({S ↾}_{A})) \leftrightarrow (G dom DProd ({S ↾}_{A}) \land \exists f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \sum_{G} F = \sum_{G} f))$
14	7 13	mpbid	$⊢ φ \to (G dom DProd ({S ↾}_{A}) \land \exists f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \sum_{G} F = \sum_{G} f)$
15	14	simprd	$⊢ φ \to \exists f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \sum_{G} F = \sum_{G} f$
16	15	adantr	$⊢ (φ \land X \in (I ∖ A)) \to \exists f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \sum_{G} F = \sum_{G} f$
17		simprr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to \sum_{G} F = \sum_{G} f$
18	14	simpld	$⊢ φ \to G dom DProd ({S ↾}_{A})$
19	18	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to G dom DProd ({S ↾}_{A})$
20	9 10	syl	$⊢ φ \to dom ({S ↾}_{A}) = A$
21	20	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to dom ({S ↾}_{A}) = A$
22		simprl	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
23		eqid	$⊢ {Base}_{G} = {Base}_{G}$
24	11 19 21 22 23	dprdff	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to f : A ⟶ {Base}_{G}$
25	24	feqmptd	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to f = (n \in A ⟼ f (n))$
26	5	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to A \subseteq I$
27	26	resmptd	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to {(n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) ↾}_{A} = (n \in A ⟼ if (n \in A, f (n), \underset{˙}{0}))$
28		iftrue	$⊢ n \in A \to if (n \in A, f (n), \underset{˙}{0}) = f (n)$
29	28	mpteq2ia	$⊢ (n \in A ⟼ if (n \in A, f (n), \underset{˙}{0})) = (n \in A ⟼ f (n))$
30	27 29	eqtrdi	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to {(n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) ↾}_{A} = (n \in A ⟼ f (n))$
31	25 30	eqtr4d	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to f = {(n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) ↾}_{A}$
32	31	oveq2d	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to \sum_{G} f = \sum_{G} ({(n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) ↾}_{A})$
33		eqid	$⊢ Cntz (G) = Cntz (G)$
34	3	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to G dom DProd S$
35		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
36		grpmnd	$⊢ G \in Grp \to G \in Mnd$
37	34 35 36	3syl	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to G \in Mnd$
38	3 4	dprddomcld	$⊢ φ \to I \in V$
39	38	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to I \in V$
40	4	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to dom S = I$
41	19	adantr	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \to G dom DProd ({S ↾}_{A})$
42	21	adantr	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \to dom ({S ↾}_{A}) = A$
43		simplrl	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \to f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
44	11 41 42 43	dprdfcl	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \land n \in A) \to f (n) \in ({S ↾}_{A}) (n)$
45		fvres	$⊢ n \in A \to ({S ↾}_{A}) (n) = S (n)$
46	45	adantl	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \land n \in A) \to ({S ↾}_{A}) (n) = S (n)$
47	44 46	eleqtrd	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \land n \in A) \to f (n) \in S (n)$
48	8	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to S : I ⟶ SubGrp (G)$
49	48	ffvelcdmda	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \to S (n) \in SubGrp (G)$
50	1	subg0cl	$⊢ S (n) \in SubGrp (G) \to \underset{˙}{0} \in S (n)$
51	49 50	syl	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \to \underset{˙}{0} \in S (n)$
52	51	adantr	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \land \neg n \in A) \to \underset{˙}{0} \in S (n)$
53	47 52	ifclda	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in I) \to if (n \in A, f (n), \underset{˙}{0}) \in S (n)$
54	38	mptexd	$⊢ φ \to (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) \in V$
55	54	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) \in V$
56		funmpt	$⊢ Fun (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0}))$
57	56	a1i	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to Fun (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0}))$
58	11 19 21 22	dprdffsupp	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to {finSupp}_{\underset{˙}{0}} (f)$
59		simpr	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \land n \in A) \to n \in A$
60		eldifn	$⊢ n \in (I ∖ {supp}_{\underset{˙}{0}} (f)) \to \neg n \in {supp}_{\underset{˙}{0}} (f)$
61	60	ad2antlr	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \land n \in A) \to \neg n \in {supp}_{\underset{˙}{0}} (f)$
62	59 61	eldifd	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \land n \in A) \to n \in (A ∖ {supp}_{\underset{˙}{0}} (f))$
63		ssidd	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to f supp \underset{˙}{0} \subseteq f supp \underset{˙}{0}$
64	38 5	ssexd	$⊢ φ \to A \in V$
65	64	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to A \in V$
66	1	fvexi	$⊢ \underset{˙}{0} \in V$
67	66	a1i	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to \underset{˙}{0} \in V$
68	24 63 65 67	suppssr	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (A ∖ {supp}_{\underset{˙}{0}} (f))) \to f (n) = \underset{˙}{0}$
69	68	adantlr	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \land n \in (A ∖ {supp}_{\underset{˙}{0}} (f))) \to f (n) = \underset{˙}{0}$
70	62 69	syldan	$⊢ ((((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \land n \in A) \to f (n) = \underset{˙}{0}$
71	70	ifeq1da	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to if (n \in A, f (n), \underset{˙}{0}) = if (n \in A, \underset{˙}{0}, \underset{˙}{0})$
72		ifid	$⊢ if (n \in A, \underset{˙}{0}, \underset{˙}{0}) = \underset{˙}{0}$
73	71 72	eqtrdi	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ {supp}_{\underset{˙}{0}} (f))) \to if (n \in A, f (n), \underset{˙}{0}) = \underset{˙}{0}$
74	73 39	suppss2	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) supp \underset{˙}{0} \subseteq f supp \underset{˙}{0}$
75		fsuppsssupp	$⊢ (((n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) \in V \land Fun (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0}))) \land ({finSupp}_{\underset{˙}{0}} (f) \land (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) supp \underset{˙}{0} \subseteq f supp \underset{˙}{0})) \to {finSupp}_{\underset{˙}{0}} ((n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})))$
76	55 57 58 74 75	syl22anc	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to {finSupp}_{\underset{˙}{0}} ((n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})))$
77	2 34 40 53 76	dprdwd	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) \in W$
78	2 34 40 77 23	dprdff	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) : I ⟶ {Base}_{G}$
79	2 34 40 77 33	dprdfcntz	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to ran (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) \subseteq Cntz (G) (ran (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})))$
80		eldifn	$⊢ n \in (I ∖ A) \to \neg n \in A$
81	80	adantl	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ A)) \to \neg n \in A$
82	81	iffalsed	$⊢ (((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \land n \in (I ∖ A)) \to if (n \in A, f (n), \underset{˙}{0}) = \underset{˙}{0}$
83	82 39	suppss2	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) supp \underset{˙}{0} \subseteq A$
84	23 1 33 37 39 78 79 83 76	gsumzres	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to \sum_{G} ({(n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) ↾}_{A}) = \underset{n \in I}{\sum_{G}} if (n \in A, f (n), \underset{˙}{0})$
85	17 32 84	3eqtrd	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to \sum_{G} F = \underset{n \in I}{\sum_{G}} if (n \in A, f (n), \underset{˙}{0})$
86	6	ad2antrr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to F \in W$
87	1 2 34 40 86 77	dprdf11	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to (\sum_{G} F = \underset{n \in I}{\sum_{G}} if (n \in A, f (n), \underset{˙}{0}) \leftrightarrow F = (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})))$
88	85 87	mpbid	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to F = (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0}))$
89	88	fveq1d	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to F (X) = (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) (X)$
90		eldifi	$⊢ X \in (I ∖ A) \to X \in I$
91	90	ad2antlr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to X \in I$
92		eleq1	$⊢ n = X \to (n \in A \leftrightarrow X \in A)$
93		fveq2	$⊢ n = X \to f (n) = f (X)$
94	92 93	ifbieq1d	$⊢ n = X \to if (n \in A, f (n), \underset{˙}{0}) = if (X \in A, f (X), \underset{˙}{0})$
95		eqid	$⊢ (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) = (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0}))$
96		fvex	$⊢ f (n) \in V$
97	96 66	ifex	$⊢ if (n \in A, f (n), \underset{˙}{0}) \in V$
98	94 95 97	fvmpt3i	$⊢ X \in I \to (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) (X) = if (X \in A, f (X), \underset{˙}{0})$
99	91 98	syl	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to (n \in I ⟼ if (n \in A, f (n), \underset{˙}{0})) (X) = if (X \in A, f (X), \underset{˙}{0})$
100		eldifn	$⊢ X \in (I ∖ A) \to \neg X \in A$
101	100	ad2antlr	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to \neg X \in A$
102	101	iffalsed	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to if (X \in A, f (X), \underset{˙}{0}) = \underset{˙}{0}$
103	89 99 102	3eqtrd	$⊢ ((φ \land X \in (I ∖ A)) \land (f \in \{h \in \underset{i \in A}{⨉} ({S ↾}_{A}) (i) \| {finSupp}_{\underset{˙}{0}} (h)\} \land \sum_{G} F = \sum_{G} f)) \to F (X) = \underset{˙}{0}$
104	16 103	rexlimddv	$⊢ (φ \land X \in (I ∖ A)) \to F (X) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem dmdprdsplitlem

Proof