tdeglem4OLD

Description: Obsolete version of tdeglem4 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 29-Mar-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	tdeglem.a	$⊢ A = \{m \in ({ℕ_{0}}^{I}) \| m^{-1} [ℕ] \in Fin\}$
	tdeglem.h	$⊢ H = (h \in A ⟼ \sum_{ℂ_{fld}} h)$
Assertion	tdeglem4OLD	$⊢ (I \in V \land 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	ad2antlr	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to H (X) = \sum_{ℂ_{fld}} X$
9	1	psrbagfOLD	$⊢ (I \in V \land X \in A) \to X : I ⟶ ℕ_{0}$
10	9	feqmptd	$⊢ (I \in V \land X \in A) \to X = (y \in I ⟼ X (y))$
11	10	adantr	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to X = (y \in I ⟼ X (y))$
12	11	oveq2d	$⊢ ((I \in V \land 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	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to ℂ_{fld} \in CMnd$
19		simpll	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to I \in V$
20	9	adantr	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to X : I ⟶ ℕ_{0}$
21	20	ffvelrnda	$⊢ (((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \land y \in I) \to X (y) \in ℕ_{0}$
22	21	nn0cnd	$⊢ (((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \land y \in I) \to X (y) \in ℂ$
23	1	psrbagfsuppOLD	$⊢ (X \in A \land I \in V) \to {finSupp}_{0} (X)$
24	23	ancoms	$⊢ (I \in V \land X \in A) \to {finSupp}_{0} (X)$
25	24	adantr	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to {finSupp}_{0} (X)$
26	11 25	eqbrtrrd	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to {finSupp}_{0} ((y \in I ⟼ X (y)))$
27		incom	$⊢ (I ∖ \{x\}) \cap \{x\} = \{x\} \cap (I ∖ \{x\})$
28		disjdif	$⊢ \{x\} \cap (I ∖ \{x\}) = \emptyset$
29	27 28	eqtri	$⊢ (I ∖ \{x\}) \cap \{x\} = \emptyset$
30	29	a1i	$⊢ ((I \in V \land 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	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to I = (I ∖ \{x\}) \cup \{x\}$
34	13 14 15 18 19 22 26 30 33	gsumsplit2	$⊢ ((I \in V \land 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	$⊢ ((I \in V \land 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		difexg	$⊢ I \in V \to I ∖ \{x\} \in V$
37	36	ad2antrr	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to I ∖ \{x\} \in V$
38		nn0subm	$⊢ ℕ_{0} \in SubMnd (ℂ_{fld})$
39	38	a1i	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to ℕ_{0} \in SubMnd (ℂ_{fld})$
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	20 40 41	syl2an	$⊢ (((I \in V \land 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	$⊢ ((I \in V \land 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	$⊢ I \in V \to (y \in (I ∖ \{x\}) ⟼ X (y)) \in V$
45	44	ad2antrr	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to (y \in (I ∖ \{x\}) ⟼ X (y)) \in V$
46		funmpt	$⊢ Fun (y \in (I ∖ \{x\}) ⟼ X (y))$
47	46	a1i	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to Fun (y \in (I ∖ \{x\}) ⟼ X (y))$
48		funmpt	$⊢ Fun (y \in I ⟼ X (y))$
49		difss	$⊢ I ∖ \{x\} \subseteq I$
50		resmpt	$⊢ I ∖ \{x\} \subseteq I \to {(y \in I ⟼ X (y)) ↾}_{(I ∖ \{x\})} = (y \in (I ∖ \{x\}) ⟼ X (y))$
51	49 50	ax-mp	$⊢ {(y \in I ⟼ X (y)) ↾}_{(I ∖ \{x\})} = (y \in (I ∖ \{x\}) ⟼ X (y))$
52		resss	$⊢ {(y \in I ⟼ X (y)) ↾}_{(I ∖ \{x\})} \subseteq (y \in I ⟼ X (y))$
53	51 52	eqsstrri	$⊢ (y \in (I ∖ \{x\}) ⟼ X (y)) \subseteq (y \in I ⟼ X (y))$
54		mptexg	$⊢ I \in V \to (y \in I ⟼ X (y)) \in V$
55	54	ad2antrr	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to (y \in I ⟼ X (y)) \in V$
56		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$
57	48 53 55 56	mp3an12i	$⊢ ((I \in V \land 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$
58		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)))$
59	45 47 26 57 58	syl22anc	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to {finSupp}_{0} ((y \in (I ∖ \{x\}) ⟼ X (y)))$
60	14 18 37 39 43 59	gsumsubmcl	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to \underset{y \in I ∖ \{x\}}{\sum_{ℂ_{fld}}} X (y) \in ℕ_{0}$
61		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
62	16 61	mp1i	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to ℂ_{fld} \in Mnd$
63		simprl	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to x \in I$
64	20 63	ffvelrnd	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℕ_{0}$
65	64	nn0cnd	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℂ$
66		fveq2	$⊢ y = x \to X (y) = X (x)$
67	13 66	gsumsn	$⊢ (ℂ_{fld} \in Mnd \land x \in I \land X (x) \in ℂ) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) = X (x)$
68	62 63 65 67	syl3anc	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) = X (x)$
69		simprr	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to X (x) \neq 0$
70	69 4	sylib	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to \neg X (x) = 0$
71		elnn0	$⊢ X (x) \in ℕ_{0} \leftrightarrow (X (x) \in ℕ \lor X (x) = 0)$
72	64 71	sylib	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to (X (x) \in ℕ \lor X (x) = 0)$
73		orel2	$⊢ \neg X (x) = 0 \to ((X (x) \in ℕ \lor X (x) = 0) \to X (x) \in ℕ)$
74	70 72 73	sylc	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to X (x) \in ℕ$
75	68 74	eqeltrd	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to \underset{y \in \{x\}}{\sum_{ℂ_{fld}}} X (y) \in ℕ$
76		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 ℕ$
77	60 75 76	syl2anc	$⊢ ((I \in V \land 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 ℕ$
78	77	nnne0d	$⊢ ((I \in V \land 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$
79	35 78	eqnetrd	$⊢ ((I \in V \land X \in A) \land (x \in I \land X (x) \neq 0)) \to H (X) \neq 0$
80	79	expr	$⊢ ((I \in V \land X \in A) \land x \in I) \to (X (x) \neq 0 \to H (X) \neq 0)$
81	4 80	syl5bir	$⊢ ((I \in V \land X \in A) \land x \in I) \to (\neg X (x) = 0 \to H (X) \neq 0)$
82	81	rexlimdva	$⊢ (I \in V \land X \in A) \to (\exists x \in I \neg X (x) = 0 \to H (X) \neq 0)$
83	3 82	syl5bir	$⊢ (I \in V \land X \in A) \to (\neg \forall x \in I X (x) = 0 \to H (X) \neq 0)$
84	83	necon4bd	$⊢ (I \in V \land X \in A) \to (H (X) = 0 \to \forall x \in I X (x) = 0)$
85	9	ffnd	$⊢ (I \in V \land X \in A) \to X Fn I$
86		0nn0	$⊢ 0 \in ℕ_{0}$
87		fnconstg	$⊢ 0 \in ℕ_{0} \to (I \times \{0\}) Fn I$
88	86 87	mp1i	$⊢ (I \in V \land X \in A) \to (I \times \{0\}) Fn I$
89		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))$
90	85 88 89	syl2anc	$⊢ (I \in V \land X \in A) \to (X = I \times \{0\} \leftrightarrow \forall x \in I X (x) = (I \times \{0\}) (x))$
91		c0ex	$⊢ 0 \in V$
92	91	fvconst2	$⊢ x \in I \to (I \times \{0\}) (x) = 0$
93	92	eqeq2d	$⊢ x \in I \to (X (x) = (I \times \{0\}) (x) \leftrightarrow X (x) = 0)$
94	93	ralbiia	$⊢ \forall x \in I X (x) = (I \times \{0\}) (x) \leftrightarrow \forall x \in I X (x) = 0$
95	90 94	bitrdi	$⊢ (I \in V \land X \in A) \to (X = I \times \{0\} \leftrightarrow \forall x \in I X (x) = 0)$
96	84 95	sylibrd	$⊢ (I \in V \land X \in A) \to (H (X) = 0 \to X = I \times \{0\})$
97	1	psrbag0	$⊢ I \in V \to I \times \{0\} \in A$
98	97	adantr	$⊢ (I \in V \land X \in A) \to I \times \{0\} \in A$
99		oveq2	$⊢ h = I \times \{0\} \to \sum_{ℂ_{fld}} h = \sum_{ℂ_{fld}} (I \times \{0\})$
100		ovex	$⊢ \sum_{ℂ_{fld}} (I \times \{0\}) \in V$
101	99 2 100	fvmpt	$⊢ I \times \{0\} \in A \to H (I \times \{0\}) = \sum_{ℂ_{fld}} (I \times \{0\})$
102	98 101	syl	$⊢ (I \in V \land X \in A) \to H (I \times \{0\}) = \sum_{ℂ_{fld}} (I \times \{0\})$
103		fconstmpt	$⊢ I \times \{0\} = (x \in I ⟼ 0)$
104	103	oveq2i	$⊢ \sum_{ℂ_{fld}} (I \times \{0\}) = \underset{x \in I}{\sum_{ℂ_{fld}}} 0$
105	16 61	ax-mp	$⊢ ℂ_{fld} \in Mnd$
106	14	gsumz	$⊢ (ℂ_{fld} \in Mnd \land I \in V) \to \underset{x \in I}{\sum_{ℂ_{fld}}} 0 = 0$
107	105 106	mpan	$⊢ I \in V \to \underset{x \in I}{\sum_{ℂ_{fld}}} 0 = 0$
108	107	adantr	$⊢ (I \in V \land X \in A) \to \underset{x \in I}{\sum_{ℂ_{fld}}} 0 = 0$
109	104 108	syl5eq	$⊢ (I \in V \land X \in A) \to \sum_{ℂ_{fld}} (I \times \{0\}) = 0$
110	102 109	eqtrd	$⊢ (I \in V \land X \in A) \to H (I \times \{0\}) = 0$
111		fveqeq2	$⊢ X = I \times \{0\} \to (H (X) = 0 \leftrightarrow H (I \times \{0\}) = 0)$
112	110 111	syl5ibrcom	$⊢ (I \in V \land X \in A) \to (X = I \times \{0\} \to H (X) = 0)$
113	96 112	impbid	$⊢ (I \in V \land X \in A) \to (H (X) = 0 \leftrightarrow X = I \times \{0\})$

Metamath Proof Explorer

Theorem tdeglem4OLD

Proof