tdeglem4

Description: There is only one multi-index with total degree 0. (Contributed by Stefan O'Rear, 29-Mar-2015) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024)

	Ref	Expression
Hypotheses	tdeglem.a	$⊢ A = \{m \in ({ℕ_{0}}^{I}) \| m^{-1} [ℕ] \in Fin\}$
	tdeglem.h	$⊢ H = (h \in A ⟼ \sum_{ℂ_{fld}} h)$
Assertion	tdeglem4	$⊢ X \in A \to (H (X) = 0 \leftrightarrow X = I \times \{0\})$

Proof

Step	Hyp	Ref	Expression
1		tdeglem.a	$⊢ A = \{m \in ({ℕ_{0}}^{I}) \| m^{-1} [ℕ] \in Fin\}$
2		tdeglem.h	$⊢ H = (h \in A ⟼ \sum_{ℂ_{fld}} h)$
3		rexnal	$⊢ \exists x \in I \neg X (x) = 0 \leftrightarrow \neg \forall x \in I X (x) = 0$
4		df-ne	$⊢ X (x) \neq 0 \leftrightarrow \neg X (x) = 0$
5		oveq2	$⊢ h = X \to \sum_{ℂ_{fld}} h = \sum_{ℂ_{fld}} X$
6		ovex	$⊢ \sum_{ℂ_{fld}} X \in V$
7	5 2 6	fvmpt	$⊢ X \in A \to H (X) = \sum_{ℂ_{fld}} X$
8	7	adantr	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to H (X) = \sum_{ℂ_{fld}} X$
9	1	psrbagf	$⊢ X \in A \to X : I ⟶ ℕ_{0}$
10	9	feqmptd	$⊢ X \in A \to X = (y \in I ⟼ X (y))$
11	10	adantr	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X = (y \in I ⟼ X (y))$
12	11	oveq2d	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \sum_{ℂ_{fld}} X = \underset{y \in I}{\sum_{ℂ_{fld}}} X (y)$
13		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
14		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
15		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
16		cnring	$⊢ ℂ_{fld} \in Ring$
17		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
18	16 17	mp1i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to ℂ_{fld} \in CMnd$
19		id	$⊢ X \in A \to X \in A$
20	9	ffnd	$⊢ X \in A \to X Fn I$
21	19 20	fndmexd	$⊢ X \in A \to I \in V$
22	21	adantr	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to I \in V$
23	9	ffvelrnda	$⊢ (X \in A \land y \in I) \to X (y) \in ℕ_{0}$
24	23	nn0cnd	$⊢ (X \in A \land y \in I) \to X (y) \in ℂ$
25	24	adantlr	$⊢ ((X \in A \land (x \in I \land X (x) \neq 0)) \land y \in I) \to X (y) \in ℂ$
26	1	psrbagfsupp	$⊢ X \in A \to {finSupp}_{0} (X)$
27	10 26	eqbrtrrd	$⊢ X \in A \to {finSupp}_{0} ((y \in I ⟼ X (y)))$
28	27	adantr	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to {finSupp}_{0} ((y \in I ⟼ X (y)))$
29		disjdifr	$⊢ (I ∖ \{x\}) \cap \{x\} = \emptyset$
30	29	a1i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (I ∖ \{x\}) \cap \{x\} = \emptyset$
31		difsnid	$⊢ x \in I \to (I ∖ \{x\}) \cup \{x\} = I$
32	31	eqcomd	$⊢ x \in I \to I = (I ∖ \{x\}) \cup \{x\}$
33	32	ad2antrl	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to I = (I ∖ \{x\}) \cup \{x\}$
34	13 14 15 18 22 25 28 30 33	gsumsplit2	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \underset{y \in I}{\sum_{ℂ_{fld}}} X (y) = (\underset{y \in I ∖ \{x\}}{\sum_{ℂ_{fld}}}, X (y)) + (\underset{y \in \{x\}}{\sum_{ℂ_{fld}}}, X (y))$
35	8 12 34	3eqtrd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to H (X) = (\underset{y \in I ∖ \{x\}}{\sum_{ℂ_{fld}}}, X (y)) + (\underset{y \in \{x\}}{\sum_{ℂ_{fld}}}, X (y))$
36	22	difexd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to I ∖ \{x\} \in V$
37		nn0subm	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld})$
38	37	a1i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to ℕ_{0} \in SubMnd (ℂ_{fld})$
39	9	adantr	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X : I ⟶ ℕ_{0}$
40		eldifi	$⊢ y \in (I ∖ \{x\}) \to y \in I$
41		ffvelrn	$⊢ (X : I ⟶ ℕ_{0} \land y \in I) \to X (y) \in ℕ_{0}$
42	39 40 41	syl2an	$⊢ ((X \in A \land (x \in I \land X (x) \neq 0)) \land y \in (I ∖ \{x\})) \to X (y) \in ℕ_{0}$
43	42	fmpttd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (y \in (I ∖ \{x\}) ⟼ X (y)) : I ∖ \{x\} ⟶ ℕ_{0}$
44	36	mptexd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (y \in (I ∖ \{x\}) ⟼ X (y)) \in V$
45		funmpt	$⊢ Fun (y \in (I ∖ \{x\}) ⟼ X (y))$
46	45	a1i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to Fun (y \in (I ∖ \{x\}) ⟼ X (y))$
47		funmpt	$⊢ Fun (y \in I ⟼ X (y))$
48		difss	$⊢ I ∖ \{x\} \subseteq I$
49		mptss	$⊢ I ∖ \{x\} \subseteq I \to (y \in (I ∖ \{x\}) ⟼ X (y)) \subseteq (y \in I ⟼ X (y))$
50	48 49	ax-mp	$⊢ (y \in (I ∖ \{x\}) ⟼ X (y)) \subseteq (y \in I ⟼ X (y))$
51	22	mptexd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (y \in I ⟼ X (y)) \in V$
52		funsssuppss	$⊢ (Fun (y \in I ⟼ X (y)) \land (y \in (I ∖ \{x\}) ⟼ X (y)) \subseteq (y \in I ⟼ X (y)) \land (y \in I ⟼ X (y)) \in V) \to (y \in (I ∖ \{x\}) ⟼ X (y)) supp 0 \subseteq (y \in I ⟼ X (y)) supp 0$
53	47 50 51 52	mp3an12i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (y \in (I ∖ \{x\}) ⟼ X (y)) supp 0 \subseteq (y \in I ⟼ X (y)) supp 0$
54		fsuppsssupp	$⊢ (((y \in (I ∖ \{x\}) ⟼ X (y)) \in V \land Fun (y \in (I ∖ \{x\}) ⟼ X (y))) \land ({finSupp}_{0} ((y \in I ⟼ X (y))) \land (y \in (I ∖ \{x\}) ⟼ X (y)) supp 0 \subseteq (y \in I ⟼ X (y)) supp 0)) \to {finSupp}_{0} ((y \in (I ∖ \{x\}) ⟼ X (y)))$
55	44 46 28 53 54	syl22anc	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to {finSupp}_{0} ((y \in (I ∖ \{x\}) ⟼ X (y)))$
56	14 18 36 38 43 55	gsumsubmcl	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \underset{y \in I ∖ \{x\}}{\sum_{ℂ_{fld}}} X (y) \in ℕ_{0}$
57		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
58	16 57	ax-mp	$⊢ ℂ_{fld} \in Mnd$
59		simprl	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to x \in I$
60	39 59	ffvelrnd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℕ_{0}$
61	60	nn0cnd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℂ$
62		fveq2	$⊢ y = x \to X (y) = X (x)$
63	13 62	gsumsn	$⊢ (ℂ_{fld} \in Mnd \land x \in I \land X (x) \in ℂ) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) = X (x)$
64	58 59 61 63	mp3an2i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) = X (x)$
65		elnn0	$⊢ X (x) \in ℕ_{0} \leftrightarrow (X (x) \in ℕ \lor X (x) = 0)$
66	60 65	sylib	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (X (x) \in ℕ \lor X (x) = 0)$
67		neneq	$⊢ X (x) \neq 0 \to \neg X (x) = 0$
68	67	ad2antll	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \neg X (x) = 0$
69	66 68	olcnd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℕ$
70	64 69	eqeltrd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) \in ℕ$
71		nn0nnaddcl	$⊢ (\underset{y \in I ∖ \{x\}}{\sum_{ℂ_{fld}}} X (y) \in ℕ_{0} \land \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) \in ℕ) \to (\underset{y \in I ∖ \{x\}}{\sum_{ℂ_{fld}}}, X (y)) + (\underset{y \in \{x\}}{\sum_{ℂ_{fld}}}, X (y)) \in ℕ$
72	56 70 71	syl2anc	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (\underset{y \in I ∖ \{x\}}{\sum_{ℂ_{fld}}}, X (y)) + (\underset{y \in \{x\}}{\sum_{ℂ_{fld}}}, X (y)) \in ℕ$
73	72	nnne0d	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (\underset{y \in I ∖ \{x\}}{\sum_{ℂ_{fld}}}, X (y)) + (\underset{y \in \{x\}}{\sum_{ℂ_{fld}}}, X (y)) \neq 0$
74	35 73	eqnetrd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to H (X) \neq 0$
75	74	expr	$⊢ (X \in A \land x \in I) \to (X (x) \neq 0 \to H (X) \neq 0)$
76	4 75	syl5bir	$⊢ (X \in A \land x \in I) \to (\neg X (x) = 0 \to H (X) \neq 0)$
77	76	rexlimdva	$⊢ X \in A \to (\exists x \in I \neg X (x) = 0 \to H (X) \neq 0)$
78	3 77	syl5bir	$⊢ X \in A \to (\neg \forall x \in I X (x) = 0 \to H (X) \neq 0)$
79	78	necon4bd	$⊢ X \in A \to (H (X) = 0 \to \forall x \in I X (x) = 0)$
80		c0ex	$⊢ 0 \in V$
81		fnconstg	$⊢ 0 \in V \to (I \times \{0\}) Fn I$
82	80 81	mp1i	$⊢ X \in A \to (I \times \{0\}) Fn I$
83		eqfnfv	$⊢ (X Fn I \land (I \times \{0\}) Fn I) \to (X = I \times \{0\} \leftrightarrow \forall x \in I X (x) = (I \times \{0\}) (x))$
84	20 82 83	syl2anc	$⊢ X \in A \to (X = I \times \{0\} \leftrightarrow \forall x \in I X (x) = (I \times \{0\}) (x))$
85	80	fvconst2	$⊢ x \in I \to (I \times \{0\}) (x) = 0$
86	85	eqeq2d	$⊢ x \in I \to (X (x) = (I \times \{0\}) (x) \leftrightarrow X (x) = 0)$
87	86	ralbiia	$⊢ \forall x \in I X (x) = (I \times \{0\}) (x) \leftrightarrow \forall x \in I X (x) = 0$
88	84 87	bitrdi	$⊢ X \in A \to (X = I \times \{0\} \leftrightarrow \forall x \in I X (x) = 0)$
89	79 88	sylibrd	$⊢ X \in A \to (H (X) = 0 \to X = I \times \{0\})$
90	1	psrbag0	$⊢ I \in V \to I \times \{0\} \in A$
91		oveq2	$⊢ h = I \times \{0\} \to \sum_{ℂ_{fld}} h = \sum_{ℂ_{fld}} (I \times \{0\})$
92		ovex	$⊢ \sum_{ℂ_{fld}} (I \times \{0\}) \in V$
93	91 2 92	fvmpt	$⊢ I \times \{0\} \in A \to H (I \times \{0\}) = \sum_{ℂ_{fld}} (I \times \{0\})$
94	21 90 93	3syl	$⊢ X \in A \to H (I \times \{0\}) = \sum_{ℂ_{fld}} (I \times \{0\})$
95		fconstmpt	$⊢ I \times \{0\} = (x \in I ⟼ 0)$
96	95	oveq2i	$⊢ \sum_{ℂ_{fld}} (I \times \{0\}) = \underset{x \in I}{\sum_{ℂ_{fld}}} 0$
97	14	gsumz	$⊢ (ℂ_{fld} \in Mnd \land I \in V) \to \underset{x \in I}{\sum_{ℂ_{fld}}} 0 = 0$
98	58 21 97	sylancr	$⊢ X \in A \to \underset{x \in I}{\sum_{ℂ_{fld}}} 0 = 0$
99	96 98	syl5eq	$⊢ X \in A \to \sum_{ℂ_{fld}} (I \times \{0\}) = 0$
100	94 99	eqtrd	$⊢ X \in A \to H (I \times \{0\}) = 0$
101		fveqeq2	$⊢ X = I \times \{0\} \to (H (X) = 0 \leftrightarrow H (I \times \{0\}) = 0)$
102	100 101	syl5ibrcom	$⊢ X \in A \to (X = I \times \{0\} \to H (X) = 0)$
103	89 102	impbid	$⊢ X \in A \to (H (X) = 0 \leftrightarrow X = I \times \{0\})$

Metamath Proof Explorer

Theorem tdeglem4

Proof