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	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge n\in {\mathbb{N}}_0\wedge L\in B\right)\to n\underset{\dot{}}{·}L\in B$$
35	31 32 33 34	syl3anc	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge n\in {\mathbb{N}}_0\right)\to n\underset{\dot{}}{·}L\in B$$
36	35	fmpttd	$$⊢\left(\phi \wedge a\in H\right)\to \left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right):{\mathbb{N}}_0⟶B$$
37	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}$$
38		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$$
39		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$$
40	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$$
41	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)$$
42	37 38 39 40 41	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)$$
43		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)=\left(n\in {\mathbb{N}}_0⟼n\underset{\dot{}}{·}L\right)$$
44		oveq1	$$⊢n=x+y\to n\underset{\dot{}}{·}L=\left(x+y\right)\underset{\dot{}}{·}L$$
45		nn0addcl	$$⊢\left(x\in {\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to x+y\in {\mathbb{N}}_0$$
46	45	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$$
47		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}$$
48	43 44 46 47	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$$
49		oveq1	$$⊢n=x\to n\underset{\dot{}}{·}L=x\underset{\dot{}}{·}L$$
50		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}$$
51	43 49 38 50	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$$
52		oveq1	$$⊢n=y\to n\underset{\dot{}}{·}L=y\underset{\dot{}}{·}L$$
53		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}$$
54	43 52 39 53	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$$
55	51 54	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)$$
56	42 48 55	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)$$
57		oveq1	$$⊢n=0\to n\underset{\dot{}}{·}L=0\underset{\dot{}}{·}L$$
58		0nn0	$$⊢0\in {\mathbb{N}}_0$$
59	58	a1i	$$⊢\left(\phi \wedge a\in H\right)\to 0\in {\mathbb{N}}_0$$
60		ovexd	$$⊢\left(\phi \wedge a\in H\right)\to 0\underset{\dot{}}{·}L\in \mathrm{V}$$
61	43 57 59 60	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$$
62	7	adantr	$$⊢\left(\phi \wedge a\in H\right)\to L\in B$$
63	3 28 4	mulg0	$$⊢L\in B\to 0\underset{\dot{}}{·}L=0_G$$
64	62 63	syl	$$⊢\left(\phi \wedge a\in H\right)\to 0\underset{\dot{}}{·}L=0_G$$
65	61 64	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$$
66	12 3 26 27 15 28 30 22 36 56 65	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)$$
67		elrabi	$$⊢a\in \left\{g\in D|{\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g=N\right\}\to a\in D$$
68	67 2	eleq2s	$$⊢a\in H\to a\in D$$
69	68	adantl	$$⊢\left(\phi \wedge a\in H\right)\to a\in D$$
70	1	psrbagf	$$⊢a\in D\to a:I⟶{\mathbb{N}}_0$$
71	69 70	syl	$$⊢\left(\phi \wedge a\in H\right)\to a:I⟶{\mathbb{N}}_0$$
72	71	ffvelrnda	$$⊢\left(\left(\phi \wedge a\in H\right)\wedge v\in I\right)\to a\left(v\right)\in {\mathbb{N}}_0$$
73	71	feqmptd	$$⊢\left(\phi \wedge a\in H\right)\to a=\left(v\in I⟼a\left(v\right)\right)$$
74	1	psrbagfsupp	$$⊢a\in D\to {finSupp}_0\left(a\right)$$
75	69 74	syl	$$⊢\left(\phi \wedge a\in H\right)\to {finSupp}_0\left(a\right)$$
76	73 75	eqbrtrrd	$$⊢\left(\phi \wedge a\in H\right)\to {finSupp}_0\left(\left(v\in I⟼a\left(v\right)\right)\right)$$
77		oveq1	$$⊢n=a\left(v\right)\to n\underset{\dot{}}{·}L=a\left(v\right)\underset{\dot{}}{·}L$$
78		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$$
79	12 15 21 22 23 66 72 76 77 78	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$$
80	73	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)$$
81		oveq2	$$⊢g=a\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}g={\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a$$
82	81	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)$$
83	82 2	elrab2	$$⊢a\in H\leftrightarrow \left(a\in D\wedge {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a=N\right)$$
84	83	simprbi	$$⊢a\in H\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a=N$$
85	84	adantl	$$⊢\left(\phi \wedge a\in H\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}{\mathbb{N}}_0}a=N$$
86	80 85	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$$
87	86	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$$
88	79 87	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$$