Theorem 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=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	tdeglem.h	$$⊢H=\left(h\in A⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
Assertion	tdeglem3OLD	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to H\left(X{+}_{f}Y\right)=H\left(X\right)+H\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		tdeglem.a	$$⊢A=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		tdeglem.h	$$⊢H=\left(h\in A⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
3		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
4		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
5		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
6		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
7		ringcmn	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
8	6 7	mp1i	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
9		simp1	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to I\in V$$
10	1	psrbagfOLD	$$⊢\left(I\in V\wedge X\in A\right)\to X:I⟶{\mathbb{N}}_0$$
11		nn0sscn	$$⊢{\mathbb{N}}_0\subseteq ℂ$$
12		fss	$$⊢\left(X:I⟶{\mathbb{N}}_0\wedge {\mathbb{N}}_0\subseteq ℂ\right)\to X:I⟶ℂ$$
13	10 11 12	sylancl	$$⊢\left(I\in V\wedge X\in A\right)\to X:I⟶ℂ$$
14	13	3adant3	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to X:I⟶ℂ$$
15	1	psrbagfOLD	$$⊢\left(I\in V\wedge Y\in A\right)\to Y:I⟶{\mathbb{N}}_0$$
16		fss	$$⊢\left(Y:I⟶{\mathbb{N}}_0\wedge {\mathbb{N}}_0\subseteq ℂ\right)\to Y:I⟶ℂ$$
17	15 11 16	sylancl	$$⊢\left(I\in V\wedge Y\in A\right)\to Y:I⟶ℂ$$
18	17	3adant2	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to Y:I⟶ℂ$$
19	1	psrbagfsuppOLD	$$⊢\left(X\in A\wedge I\in V\right)\to {finSupp}_0\left(X\right)$$
20	19	ancoms	$$⊢\left(I\in V\wedge X\in A\right)\to {finSupp}_0\left(X\right)$$
21	20	3adant3	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to {finSupp}_0\left(X\right)$$
22	1	psrbagfsuppOLD	$$⊢\left(Y\in A\wedge I\in V\right)\to {finSupp}_0\left(Y\right)$$
23	22	ancoms	$$⊢\left(I\in V\wedge Y\in A\right)\to {finSupp}_0\left(Y\right)$$
24	23	3adant2	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to {finSupp}_0\left(Y\right)$$
25	3 4 5 8 9 14 18 21 24	gsumadd	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left(X{+}_{f}Y\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},X\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}},Y\right)$$
26	1	psrbagaddclOLD	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to X{+}_{f}Y\in A$$
27		oveq2	$$⊢h=X{+}_{f}Y\to {\sum }_{{ℂ}_{\mathrm{fld}}}h={\sum }_{{ℂ}_{\mathrm{fld}}}\left(X{+}_{f}Y\right)$$
28		ovex	$$⊢{\sum }_{{ℂ}_{\mathrm{fld}}}\left(X{+}_{f}Y\right)\in \mathrm{V}$$
29	27 2 28	fvmpt	$$⊢X{+}_{f}Y\in A\to H\left(X{+}_{f}Y\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left(X{+}_{f}Y\right)$$
30	26 29	syl	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to H\left(X{+}_{f}Y\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left(X{+}_{f}Y\right)$$
31		oveq2	$$⊢h=X\to {\sum }_{{ℂ}_{\mathrm{fld}}}h={\sum }_{{ℂ}_{\mathrm{fld}}}X$$
32		ovex	$$⊢{\sum }_{{ℂ}_{\mathrm{fld}}}X\in \mathrm{V}$$
33	31 2 32	fvmpt	$$⊢X\in A\to H\left(X\right)={\sum }_{{ℂ}_{\mathrm{fld}}}X$$
34		oveq2	$$⊢h=Y\to {\sum }_{{ℂ}_{\mathrm{fld}}}h={\sum }_{{ℂ}_{\mathrm{fld}}}Y$$
35		ovex	$$⊢{\sum }_{{ℂ}_{\mathrm{fld}}}Y\in \mathrm{V}$$
36	34 2 35	fvmpt	$$⊢Y\in A\to H\left(Y\right)={\sum }_{{ℂ}_{\mathrm{fld}}}Y$$
37	33 36	oveqan12d	$$⊢\left(X\in A\wedge Y\in A\right)\to H\left(X\right)+H\left(Y\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},X\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}},Y\right)$$
38	37	3adant1	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to H\left(X\right)+H\left(Y\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},X\right)+\left({\sum }_{{ℂ}_{\mathrm{fld}}},Y\right)$$
39	25 30 38	3eqtr4d	$$⊢\left(I\in V\wedge X\in A\wedge Y\in A\right)\to H\left(X{+}_{f}Y\right)=H\left(X\right)+H\left(Y\right)$$