Theorem mhphflem

Description: Lemma for mhphf . Add several multiples of L together, in a case where the total amount of multiplies is N . (Contributed by SN, 30-Jul-2024)

	Ref	Expression
Hypotheses	mhphflem.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mhphflem.h	$$⊢H=\left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
	mhphflem.k	$$⊢B={\mathrm{Base}}_G$$
	mhphflem.e	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	mhphflem.i	$$⊢\phi \to I\in V$$
	mhphflem.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
	mhphflem.l	$$⊢\phi \to L\in B$$
	mhphflem.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	mhphflem	$$⊢\left(\phi \wedge a\in H\right)\to \underset{v\in I}{{\sum }_G}\left(a\left(v\right)\underset{\dot{}}{·}L\right)=N\underset{\dot{}}{·}L$$

Proof

Step	Hyp	Ref	Expression
1		mhphflem.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		mhphflem.h	$$⊢H=\left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}$$
3		mhphflem.k	$$⊢B={\mathrm{Base}}_G$$
4		mhphflem.e	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
5		mhphflem.i	$$⊢\phi \to I\in V$$
6		mhphflem.g	$$⊢\phi \to G\in \mathrm{Mnd}$$
7		mhphflem.l	$$⊢\phi \to L\in B$$
8		mhphflem.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
9		nn0subm	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$$
10		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0$$
11	10	submbas	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to {\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
12	9 11	ax-mp	$$⊢{\mathbb{N}}_0={\mathrm{Base}}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
13		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
14	10 13	subm0	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to 0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
15	9 14	ax-mp	$$⊢0=0_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
16		cnring	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
17		ringcmn	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
18	16 17	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
19	10	submcmn	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}\wedge {\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
20	18 9 19	mp2an	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
21	20	a1i	$$⊢\left(\phi \wedge a\in H\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{CMnd}$$
22	6	adantr	$$⊢\left(\phi \wedge a\in H\right)\to G\in \mathrm{Mnd}$$
23	5	adantr	$$⊢\left(\phi \wedge a\in H\right)\to I\in V$$
24		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
25	10 24	ressplusg	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to +={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
26	9 25	ax-mp	$$⊢+={+}_{\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)}$$
27		eqid	$$⊢{+}_G={+}_G$$
28		eqid	$$⊢0_G=0_G$$
29	10	submmnd	$$⊢{\mathbb{N}}_0\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
30	9 29	mp1i	$$⊢\left(\phi \wedge a\in H\right)\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\in \mathrm{Mnd}$$
31	6	ad2antrr	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge n\in {\mathbb{N}}_0\right)\to G\in \mathrm{Mnd}$$
32		simpr	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge n\in {\mathbb{N}}_0\right)\to n\in {\mathbb{N}}_0$$
33	7	ad2antrr	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge n\in {\mathbb{N}}_0\right)\to L\in B$$
34	3 4 31 32 33	mulgnn0cld	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge n\in {\mathbb{N}}_0\right)\to n\underset{\dot{}}{·}L\in B$$
35	34	fmpttd	$$⊢\left(\phi \wedge a\in H\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right):{\mathbb{N}}_0⟶B$$
36	6	ad2antrr	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to G\in \mathrm{Mnd}$$
37		simprl	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to x\in {\mathbb{N}}_0$$
38		simprr	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to y\in {\mathbb{N}}_0$$
39	7	ad2antrr	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to L\in B$$
40	3 4 27	mulgnn0dir	$$⊢\left(G\in \mathrm{Mnd}\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\wedge L\in B\right)\right)\to \left(x+y\right)\underset{\dot{}}{·}L=\left(x\underset{\dot{}}{·}L\right){+}_G\left(y\underset{\dot{}}{·}L\right)$$
41	36 37 38 39 40	syl13anc	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to \left(x+y\right)\underset{\dot{}}{·}L=\left(x\underset{\dot{}}{·}L\right){+}_G\left(y\underset{\dot{}}{·}L\right)$$
42		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)=\left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)$$
43		oveq1	$$⊢n=x+y\to n\underset{\dot{}}{·}L=\left(x+y\right)\underset{\dot{}}{·}L$$
44		nn0addcl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to x+y\in {\mathbb{N}}_0$$
45	44	adantl	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to x+y\in {\mathbb{N}}_0$$
46		ovexd	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to \left(x+y\right)\underset{\dot{}}{·}L\in \mathrm{V}$$
47	42 43 45 46	fvmptd3	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(x+y\right)=\left(x+y\right)\underset{\dot{}}{·}L$$
48		oveq1	$$⊢n=x\to n\underset{\dot{}}{·}L=x\underset{\dot{}}{·}L$$
49		ovexd	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to x\underset{\dot{}}{·}L\in \mathrm{V}$$
50	42 48 37 49	fvmptd3	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(x\right)=x\underset{\dot{}}{·}L$$
51		oveq1	$$⊢n=y\to n\underset{\dot{}}{·}L=y\underset{\dot{}}{·}L$$
52		ovexd	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to y\underset{\dot{}}{·}L\in \mathrm{V}$$
53	42 51 38 52	fvmptd3	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(y\right)=y\underset{\dot{}}{·}L$$
54	50 53	oveq12d	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(x\right){+}_G\left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(y\right)=\left(x\underset{\dot{}}{·}L\right){+}_G\left(y\underset{\dot{}}{·}L\right)$$
55	41 47 54	3eqtr4d	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge \left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(x+y\right)=\left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(x\right){+}_G\left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(y\right)$$
56		oveq1	$$⊢n=0\to n\underset{\dot{}}{·}L=0\underset{\dot{}}{·}L$$
57		0nn0	$$⊢0\in {\mathbb{N}}_0$$
58	57	a1i	$$⊢\left(\phi \wedge a\in H\right)\to 0\in {\mathbb{N}}_0$$
59		ovexd	$$⊢\left(\phi \wedge a\in H\right)\to 0\underset{\dot{}}{·}L\in \mathrm{V}$$
60	42 56 58 59	fvmptd3	$$⊢\left(\phi \wedge a\in H\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(0\right)=0\underset{\dot{}}{·}L$$
61	7	adantr	$$⊢\left(\phi \wedge a\in H\right)\to L\in B$$
62	3 28 4	mulg0	$$⊢L\in B\to 0\underset{\dot{}}{·}L=0_G$$
63	61 62	syl	$$⊢\left(\phi \wedge a\in H\right)\to 0\underset{\dot{}}{·}L=0_G$$
64	60 63	eqtrd	$$⊢\left(\phi \wedge a\in H\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\left(0\right)=0_G$$
65	12 3 26 27 15 28 30 22 35 55 64	ismhmd	$$⊢\left(\phi \wedge a\in H\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)\in \left(\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0\right)\mathrm{MndHom}G\right)$$
66		elrabi	$$⊢a\in \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\to a\in D$$
67	66 2	eleq2s	$$⊢a\in H\to a\in D$$
68	67	adantl	$$⊢\left(\phi \wedge a\in H\right)\to a\in D$$
69	1	psrbagf	$$⊢a\in D\to a:I⟶{\mathbb{N}}_0$$
70	68 69	syl	$$⊢\left(\phi \wedge a\in H\right)\to a:I⟶{\mathbb{N}}_0$$
71	70	ffvelcdmda	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge v\in I\right)\to a\left(v\right)\in {\mathbb{N}}_0$$
72	70	feqmptd	$$⊢\left(\phi \wedge a\in H\right)\to a=\left(v\in I⟼a\left(v\right)\right)$$
73	1	psrbagfsupp	$$⊢a\in D\to {finSupp}_0\left(a\right)$$
74	68 73	syl	$$⊢\left(\phi \wedge a\in H\right)\to {finSupp}_0\left(a\right)$$
75	72 74	eqbrtrrd	$$⊢\left(\phi \wedge a\in H\right)\to {finSupp}_0\left(\left(v\in I⟼a\left(v\right)\right)\right)$$
76		oveq1	$$⊢n=a\left(v\right)\to n\underset{\dot{}}{·}L=a\left(v\right)\underset{\dot{}}{·}L$$
77		oveq1	$$⊢n=\underset{v\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}a\left(v\right)\to n\underset{\dot{}}{·}L=\left(\underset{v\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}},a\left(v\right)\right)\underset{\dot{}}{·}L$$
78	12 15 21 22 23 65 71 75 76 77	gsummhm2	$$⊢\left(\phi \wedge a\in H\right)\to \underset{v\in I}{{\sum }_G}\left(a\left(v\right)\underset{\dot{}}{·}L\right)=\left(\underset{v\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}},a\left(v\right)\right)\underset{\dot{}}{·}L$$
79	72	oveq2d	$$⊢\left(\phi \wedge a\in H\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a=\underset{v\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}a\left(v\right)$$
80		oveq2	$$⊢g=a\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a$$
81	80	eqeq1d	$$⊢g=a\to \left({\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\leftrightarrow {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a=N\right)$$
82	81 2	elrab2	$$⊢a\in H\leftrightarrow \left(a\in D\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a=N\right)$$
83	82	simprbi	$$⊢a\in H\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a=N$$
84	83	adantl	$$⊢\left(\phi \wedge a\in H\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a=N$$
85	79 84	eqtr3d	$$⊢\left(\phi \wedge a\in H\right)\to \underset{v\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}}a\left(v\right)=N$$
86	85	oveq1d	$$⊢\left(\phi \wedge a\in H\right)\to \left(\underset{v\in I}{{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}},a\left(v\right)\right)\underset{\dot{}}{·}L=N\underset{\dot{}}{·}L$$
87	78 86	eqtrd	$$⊢\left(\phi \wedge a\in H\right)\to \underset{v\in I}{{\sum }_G}\left(a\left(v\right)\underset{\dot{}}{·}L\right)=N\underset{\dot{}}{·}L$$