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	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
	mhphflem.h	⊢ 𝐻 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
	mhphflem.k	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mhphflem.e	⊢ · = ( .g ‘ 𝐺 )
	mhphflem.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mhphflem.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	mhphflem.l	⊢ ( 𝜑 → 𝐿 ∈ 𝐵 )
	mhphflem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	mhphflem	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) ) ) = ( 𝑁 · 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		mhphflem.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2		mhphflem.h	⊢ 𝐻 = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 }
3		mhphflem.k	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		mhphflem.e	⊢ · = ( .g ‘ 𝐺 )
5		mhphflem.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		mhphflem.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
7		mhphflem.l	⊢ ( 𝜑 → 𝐿 ∈ 𝐵 )
8		mhphflem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9		nn0subm	⊢ ℕ0 ∈ ( SubMnd ‘ ℂfld )
10		eqid	⊢ ( ℂfld ↾s ℕ0 ) = ( ℂfld ↾s ℕ0 )
11	10	submbas	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) ) )
12	9 11	ax-mp	⊢ ℕ0 = ( Base ‘ ( ℂfld ↾s ℕ0 ) )
13		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
14	10 13	subm0	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) ) )
15	9 14	ax-mp	⊢ 0 = ( 0g ‘ ( ℂfld ↾s ℕ0 ) )
16		cnring	⊢ ℂfld ∈ Ring
17		ringcmn	⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
18	16 17	ax-mp	⊢ ℂfld ∈ CMnd
19	10	submcmn	⊢ ( ( ℂfld ∈ CMnd ∧ ℕ0 ∈ ( SubMnd ‘ ℂfld ) ) → ( ℂfld ↾s ℕ0 ) ∈ CMnd )
20	18 9 19	mp2an	⊢ ( ℂfld ↾s ℕ0 ) ∈ CMnd
21	20	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ℂfld ↾s ℕ0 ) ∈ CMnd )
22	6	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐺 ∈ Mnd )
23	5	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐼 ∈ 𝑉 )
24		cnfldadd	⊢ + = ( +g ‘ ℂfld )
25	10 24	ressplusg	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → + = ( +g ‘ ( ℂfld ↾s ℕ0 ) ) )
26	9 25	ax-mp	⊢ + = ( +g ‘ ( ℂfld ↾s ℕ0 ) )
27		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
28		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
29	10	submmnd	⊢ ( ℕ0 ∈ ( SubMnd ‘ ℂfld ) → ( ℂfld ↾s ℕ0 ) ∈ Mnd )
30	9 29	mp1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ℂfld ↾s ℕ0 ) ∈ Mnd )
31	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
32		simpr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
33	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐿 ∈ 𝐵 )
34	3 4	mulgnn0cl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ 𝐿 ∈ 𝐵 ) → ( 𝑛 · 𝐿 ) ∈ 𝐵 )
35	31 32 33 34	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 𝐿 ) ∈ 𝐵 )
36	35	fmpttd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) : ℕ0 ⟶ 𝐵 )
37	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
38		simprl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝑥 ∈ ℕ0 )
39		simprr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝑦 ∈ ℕ0 )
40	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝐿 ∈ 𝐵 )
41	3 4 27	mulgnn0dir	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝐿 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
42	37 38 39 40 41	syl13anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
43		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) )
44		oveq1	⊢ ( 𝑛 = ( 𝑥 + 𝑦 ) → ( 𝑛 · 𝐿 ) = ( ( 𝑥 + 𝑦 ) · 𝐿 ) )
45		nn0addcl	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
46	45	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
47		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) ∈ V )
48	43 44 46 47	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑥 + 𝑦 ) · 𝐿 ) )
49		oveq1	⊢ ( 𝑛 = 𝑥 → ( 𝑛 · 𝐿 ) = ( 𝑥 · 𝐿 ) )
50		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑥 · 𝐿 ) ∈ V )
51	43 49 38 50	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) = ( 𝑥 · 𝐿 ) )
52		oveq1	⊢ ( 𝑛 = 𝑦 → ( 𝑛 · 𝐿 ) = ( 𝑦 · 𝐿 ) )
53		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑦 · 𝐿 ) ∈ V )
54	43 52 39 53	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) = ( 𝑦 · 𝐿 ) )
55	51 54	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
56	42 48 55	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) ) )
57		oveq1	⊢ ( 𝑛 = 0 → ( 𝑛 · 𝐿 ) = ( 0 · 𝐿 ) )
58		0nn0	⊢ 0 ∈ ℕ0
59	58	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 0 ∈ ℕ0 )
60		ovexd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 0 · 𝐿 ) ∈ V )
61	43 57 59 60	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 0 ) = ( 0 · 𝐿 ) )
62	7	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐿 ∈ 𝐵 )
63	3 28 4	mulg0	⊢ ( 𝐿 ∈ 𝐵 → ( 0 · 𝐿 ) = ( 0g ‘ 𝐺 ) )
64	62 63	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 0 · 𝐿 ) = ( 0g ‘ 𝐺 ) )
65	61 64	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 0 ) = ( 0g ‘ 𝐺 ) )
66	12 3 26 27 15 28 30 22 36 56 65	ismhmd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ∈ ( ( ℂfld ↾s ℕ0 ) MndHom 𝐺 ) )
67		elrabi	⊢ ( 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } → 𝑎 ∈ 𝐷 )
68	67 2	eleq2s	⊢ ( 𝑎 ∈ 𝐻 → 𝑎 ∈ 𝐷 )
69	68	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 ∈ 𝐷 )
70	1	psrbagf	⊢ ( 𝑎 ∈ 𝐷 → 𝑎 : 𝐼 ⟶ ℕ0 )
71	69 70	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 : 𝐼 ⟶ ℕ0 )
72	71	ffvelrnda	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑣 ) ∈ ℕ0 )
73	71	feqmptd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 = ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) )
74	1	psrbagfsupp	⊢ ( 𝑎 ∈ 𝐷 → 𝑎 finSupp 0 )
75	69 74	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 finSupp 0 )
76	73 75	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) finSupp 0 )
77		oveq1	⊢ ( 𝑛 = ( 𝑎 ‘ 𝑣 ) → ( 𝑛 · 𝐿 ) = ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) )
78		oveq1	⊢ ( 𝑛 = ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) → ( 𝑛 · 𝐿 ) = ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) )
79	12 15 21 22 23 66 72 76 77 78	gsummhm2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) ) ) = ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) )
80	73	oveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) )
81		oveq2	⊢ ( 𝑔 = 𝑎 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) )
82	81	eqeq1d	⊢ ( 𝑔 = 𝑎 → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 ↔ ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 ) )
83	82 2	elrab2	⊢ ( 𝑎 ∈ 𝐻 ↔ ( 𝑎 ∈ 𝐷 ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 ) )
84	83	simprbi	⊢ ( 𝑎 ∈ 𝐻 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 )
85	84	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 )
86	80 85	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) = 𝑁 )
87	86	oveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) = ( 𝑁 · 𝐿 ) )
88	79 87	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) ) ) = ( 𝑁 · 𝐿 ) )