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		incom	$⊢ (I ∖ \{x\}) \cap \{x\} = \{x\} \cap (I ∖ \{x\})$
30		disjdif	$⊢ \{x\} \cap (I ∖ \{x\}) = \emptyset$
31	29 30	eqtri	$⊢ (I ∖ \{x\}) \cap \{x\} = \emptyset$
32	31	a1i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (I ∖ \{x\}) \cap \{x\} = \emptyset$
33		difsnid	$⊢ x \in I \to (I ∖ \{x\}) \cup \{x\} = I$
34	33	eqcomd	$⊢ x \in I \to I = (I ∖ \{x\}) \cup \{x\}$
35	34	ad2antrl	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to I = (I ∖ \{x\}) \cup \{x\}$
36	13 14 15 18 22 25 28 32 35	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))$
37	8 12 36	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))$
38		difexg	$⊢ I \in V \to I ∖ \{x\} \in V$
39	22 38	syl	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to I ∖ \{x\} \in V$
40		nn0subm	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld})$
41	40	a1i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to ℕ_{0} \in SubMnd (ℂ_{fld})$
42	9	adantr	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X : I ⟶ ℕ_{0}$
43		eldifi	$⊢ y \in (I ∖ \{x\}) \to y \in I$
44		ffvelrn	$⊢ (X : I ⟶ ℕ_{0} \land y \in I) \to X (y) \in ℕ_{0}$
45	42 43 44	syl2an	$⊢ ((X \in A \land (x \in I \land X (x) \neq 0)) \land y \in (I ∖ \{x\})) \to X (y) \in ℕ_{0}$
46	45	fmpttd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (y \in (I ∖ \{x\}) ⟼ X (y)) : I ∖ \{x\} ⟶ ℕ_{0}$
47	39	mptexd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (y \in (I ∖ \{x\}) ⟼ X (y)) \in V$
48		funmpt	$⊢ Fun (y \in (I ∖ \{x\}) ⟼ X (y))$
49	48	a1i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to Fun (y \in (I ∖ \{x\}) ⟼ X (y))$
50		funmpt	$⊢ Fun (y \in I ⟼ X (y))$
51		difss	$⊢ I ∖ \{x\} \subseteq I$
52		mptss	$⊢ I ∖ \{x\} \subseteq I \to (y \in (I ∖ \{x\}) ⟼ X (y)) \subseteq (y \in I ⟼ X (y))$
53	51 52	ax-mp	$⊢ (y \in (I ∖ \{x\}) ⟼ X (y)) \subseteq (y \in I ⟼ X (y))$
54	22	mptexd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (y \in I ⟼ X (y)) \in V$
55		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$
56	50 53 54 55	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$
57		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)))$
58	47 49 28 56 57	syl22anc	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to {finSupp}_{0} ((y \in (I ∖ \{x\}) ⟼ X (y)))$
59	14 18 39 41 46 58	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}$
60		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
61	16 60	ax-mp	$⊢ ℂ_{fld} \in Mnd$
62		simprl	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to x \in I$
63	42 62	ffvelrnd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℕ_{0}$
64	63	nn0cnd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℂ$
65		fveq2	$⊢ y = x \to X (y) = X (x)$
66	13 65	gsumsn	$⊢ (ℂ_{fld} \in Mnd \land x \in I \land X (x) \in ℂ) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) = X (x)$
67	61 62 64 66	mp3an2i	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) = X (x)$
68		elnn0	$⊢ X (x) \in ℕ_{0} \leftrightarrow (X (x) \in ℕ \lor X (x) = 0)$
69	63 68	sylib	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to (X (x) \in ℕ \lor X (x) = 0)$
70		neneq	$⊢ X (x) \neq 0 \to \neg X (x) = 0$
71	70	ad2antll	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \neg X (x) = 0$
72	69 71	olcnd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℕ$
73	67 72	eqeltrd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) \in ℕ$
74		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 ℕ$
75	59 73 74	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 ℕ$
76	75	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$
77	37 76	eqnetrd	$⊢ (X \in A \land (x \in I \land X (x) \neq 0)) \to H (X) \neq 0$
78	77	expr	$⊢ (X \in A \land x \in I) \to (X (x) \neq 0 \to H (X) \neq 0)$
79	4 78	syl5bir	$⊢ (X \in A \land x \in I) \to (\neg X (x) = 0 \to H (X) \neq 0)$
80	79	rexlimdva	$⊢ X \in A \to (\exists x \in I \neg X (x) = 0 \to H (X) \neq 0)$
81	3 80	syl5bir	$⊢ X \in A \to (\neg \forall x \in I X (x) = 0 \to H (X) \neq 0)$
82	81	necon4bd	$⊢ X \in A \to (H (X) = 0 \to \forall x \in I X (x) = 0)$
83		c0ex	$⊢ 0 \in V$
84		fnconstg	$⊢ 0 \in V \to (I \times \{0\}) Fn I$
85	83 84	mp1i	$⊢ X \in A \to (I \times \{0\}) Fn I$
86		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))$
87	20 85 86	syl2anc	$⊢ X \in A \to (X = I \times \{0\} \leftrightarrow \forall x \in I X (x) = (I \times \{0\}) (x))$
88	83	fvconst2	$⊢ x \in I \to (I \times \{0\}) (x) = 0$
89	88	eqeq2d	$⊢ x \in I \to (X (x) = (I \times \{0\}) (x) \leftrightarrow X (x) = 0)$
90	89	ralbiia	$⊢ \forall x \in I X (x) = (I \times \{0\}) (x) \leftrightarrow \forall x \in I X (x) = 0$
91	87 90	bitrdi	$⊢ X \in A \to (X = I \times \{0\} \leftrightarrow \forall x \in I X (x) = 0)$
92	82 91	sylibrd	$⊢ X \in A \to (H (X) = 0 \to X = I \times \{0\})$
93	1	psrbag0	$⊢ I \in V \to I \times \{0\} \in A$
94		oveq2	$⊢ h = I \times \{0\} \to \sum_{ℂ_{fld}} h = \sum_{ℂ_{fld}} (I \times \{0\})$
95		ovex	$⊢ \sum_{ℂ_{fld}} (I \times \{0\}) \in V$
96	94 2 95	fvmpt	$⊢ I \times \{0\} \in A \to H (I \times \{0\}) = \sum_{ℂ_{fld}} (I \times \{0\})$
97	21 93 96	3syl	$⊢ X \in A \to H (I \times \{0\}) = \sum_{ℂ_{fld}} (I \times \{0\})$
98		fconstmpt	$⊢ I \times \{0\} = (x \in I ⟼ 0)$
99	98	oveq2i	$⊢ \sum_{ℂ_{fld}} (I \times \{0\}) = \underset{x \in I}{\sum_{ℂ_{fld}}} 0$
100	14	gsumz	$⊢ (ℂ_{fld} \in Mnd \land I \in V) \to \underset{x \in I}{\sum_{ℂ_{fld}}} 0 = 0$
101	61 21 100	sylancr	$⊢ X \in A \to \underset{x \in I}{\sum_{ℂ_{fld}}} 0 = 0$
102	99 101	syl5eq	$⊢ X \in A \to \sum_{ℂ_{fld}} (I \times \{0\}) = 0$
103	97 102	eqtrd	$⊢ X \in A \to H (I \times \{0\}) = 0$
104		fveqeq2	$⊢ X = I \times \{0\} \to (H (X) = 0 \leftrightarrow H (I \times \{0\}) = 0)$
105	103 104	syl5ibrcom	$⊢ X \in A \to (X = I \times \{0\} \to H (X) = 0)$
106	92 105	impbid	$⊢ X \in A \to (H (X) = 0 \leftrightarrow X = I \times \{0\})$

Metamath Proof Explorer

Theorem tdeglem4

Proof