Theorem tdeglem3

Description: Additivity of the total degree helper function. (Contributed by Stefan O'Rear, 26-Mar-2015) (Proof shortened by AV, 27-Jul-2019) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024)

	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	tdeglem3	$$⊢\left(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(X\in A\wedge Y\in A\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
9		simpl	$$⊢\left(X\in A\wedge Y\in A\right)\to X\in A$$
10	1	psrbagf	$$⊢X\in A\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	$$⊢X\in A\to X:I⟶ℂ$$
14	13	adantr	$$⊢\left(X\in A\wedge Y\in A\right)\to X:I⟶ℂ$$
15	14	ffnd	$$⊢\left(X\in A\wedge Y\in A\right)\to XFnI$$
16	9 15	fndmexd	$$⊢\left(X\in A\wedge Y\in A\right)\to I\in \mathrm{V}$$
17	1	psrbagf	$$⊢Y\in A\to Y:I⟶{\mathbb{N}}_0$$
18		fss	$$⊢\left(Y:I⟶{\mathbb{N}}_0\wedge {\mathbb{N}}_0\subseteq ℂ\right)\to Y:I⟶ℂ$$
19	17 11 18	sylancl	$$⊢Y\in A\to Y:I⟶ℂ$$
20	19	adantl	$$⊢\left(X\in A\wedge Y\in A\right)\to Y:I⟶ℂ$$
21	1	psrbagfsupp	$$⊢X\in A\to {finSupp}_0\left(X\right)$$
22	21	adantr	$$⊢\left(X\in A\wedge Y\in A\right)\to {finSupp}_0\left(X\right)$$
23	1	psrbagfsupp	$$⊢Y\in A\to {finSupp}_0\left(Y\right)$$
24	23	adantl	$$⊢\left(X\in A\wedge Y\in A\right)\to {finSupp}_0\left(Y\right)$$
25	3 4 5 8 16 14 20 22 24	gsumadd	$$⊢\left(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	psrbagaddcl	$$⊢\left(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(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	25 30 37	3eqtr4d	$$⊢\left(X\in A\wedge Y\in A\right)\to H\left(X{+}_{f}Y\right)=H\left(X\right)+H\left(Y\right)$$