tdeglem3OLD

Description: Obsolete version of tdeglem3 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 26-Mar-2015) (Proof shortened by AV, 27-Jul-2019) (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	tdeglem3OLD	$⊢ (I \in V \land X \in A \land Y \in A) \to H (X +_{f} Y) = H (X) + H (Y)$

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		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
4		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
5		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
6		cnring	$⊢ ℂ_{fld} \in Ring$
7		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
8	6 7	mp1i	$⊢ (I \in V \land X \in A \land Y \in A) \to ℂ_{fld} \in CMnd$
9		simp1	$⊢ (I \in V \land X \in A \land Y \in A) \to I \in V$
10	1	psrbagfOLD	$⊢ (I \in V \land X \in A) \to X : I ⟶ ℕ_{0}$
11		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
12		fss	$⊢ (X : I ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℂ) \to X : I ⟶ ℂ$
13	10 11 12	sylancl	$⊢ (I \in V \land X \in A) \to X : I ⟶ ℂ$
14	13	3adant3	$⊢ (I \in V \land X \in A \land Y \in A) \to X : I ⟶ ℂ$
15	1	psrbagfOLD	$⊢ (I \in V \land Y \in A) \to Y : I ⟶ ℕ_{0}$
16		fss	$⊢ (Y : I ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℂ) \to Y : I ⟶ ℂ$
17	15 11 16	sylancl	$⊢ (I \in V \land Y \in A) \to Y : I ⟶ ℂ$
18	17	3adant2	$⊢ (I \in V \land X \in A \land Y \in A) \to Y : I ⟶ ℂ$
19	1	psrbagfsuppOLD	$⊢ (X \in A \land I \in V) \to {finSupp}_{0} (X)$
20	19	ancoms	$⊢ (I \in V \land X \in A) \to {finSupp}_{0} (X)$
21	20	3adant3	$⊢ (I \in V \land X \in A \land Y \in A) \to {finSupp}_{0} (X)$
22	1	psrbagfsuppOLD	$⊢ (Y \in A \land I \in V) \to {finSupp}_{0} (Y)$
23	22	ancoms	$⊢ (I \in V \land Y \in A) \to {finSupp}_{0} (Y)$
24	23	3adant2	$⊢ (I \in V \land X \in A \land Y \in A) \to {finSupp}_{0} (Y)$
25	3 4 5 8 9 14 18 21 24	gsumadd	$⊢ (I \in V \land X \in A \land Y \in A) \to \sum_{ℂ_{fld}} (X +_{f} Y) = (\sum_{ℂ_{fld}}, X) + (\sum_{ℂ_{fld}}, Y)$
26	1	psrbagaddclOLD	$⊢ (I \in V \land X \in A \land Y \in A) \to X +_{f} Y \in A$
27		oveq2	$⊢ h = X +_{f} Y \to \sum_{ℂ_{fld}} h = \sum_{ℂ_{fld}} (X +_{f} Y)$
28		ovex	$⊢ \sum_{ℂ_{fld}} (X +_{f} Y) \in V$
29	27 2 28	fvmpt	$⊢ X +_{f} Y \in A \to H (X +_{f} Y) = \sum_{ℂ_{fld}} (X +_{f} Y)$
30	26 29	syl	$⊢ (I \in V \land X \in A \land Y \in A) \to H (X +_{f} Y) = \sum_{ℂ_{fld}} (X +_{f} Y)$
31		oveq2	$⊢ h = X \to \sum_{ℂ_{fld}} h = \sum_{ℂ_{fld}} X$
32		ovex	$⊢ \sum_{ℂ_{fld}} X \in V$
33	31 2 32	fvmpt	$⊢ X \in A \to H (X) = \sum_{ℂ_{fld}} X$
34		oveq2	$⊢ h = Y \to \sum_{ℂ_{fld}} h = \sum_{ℂ_{fld}} Y$
35		ovex	$⊢ \sum_{ℂ_{fld}} Y \in V$
36	34 2 35	fvmpt	$⊢ Y \in A \to H (Y) = \sum_{ℂ_{fld}} Y$
37	33 36	oveqan12d	$⊢ (X \in A \land Y \in A) \to H (X) + H (Y) = (\sum_{ℂ_{fld}}, X) + (\sum_{ℂ_{fld}}, Y)$
38	37	3adant1	$⊢ (I \in V \land X \in A \land Y \in A) \to H (X) + H (Y) = (\sum_{ℂ_{fld}}, X) + (\sum_{ℂ_{fld}}, Y)$
39	25 30 38	3eqtr4d	$⊢ (I \in V \land X \in A \land Y \in A) \to H (X +_{f} Y) = H (X) + H (Y)$

Metamath Proof Explorer

Theorem tdeglem3OLD

Proof