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 31 32 33	mulgnn0cld	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 · 𝐿 ) ∈ 𝐵 )
35	34	fmpttd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) : ℕ0 ⟶ 𝐵 )
36	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
37		simprl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝑥 ∈ ℕ0 )
38		simprr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝑦 ∈ ℕ0 )
39	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → 𝐿 ∈ 𝐵 )
40	3 4 27	mulgnn0dir	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝐿 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
41	36 37 38 39 40	syl13anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
42		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) )
43		oveq1	⊢ ( 𝑛 = ( 𝑥 + 𝑦 ) → ( 𝑛 · 𝐿 ) = ( ( 𝑥 + 𝑦 ) · 𝐿 ) )
44		nn0addcl	⊢ ( ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
45	44	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑥 + 𝑦 ) ∈ ℕ0 )
46		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑥 + 𝑦 ) · 𝐿 ) ∈ V )
47	42 43 45 46	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑥 + 𝑦 ) · 𝐿 ) )
48		oveq1	⊢ ( 𝑛 = 𝑥 → ( 𝑛 · 𝐿 ) = ( 𝑥 · 𝐿 ) )
49		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑥 · 𝐿 ) ∈ V )
50	42 48 37 49	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) = ( 𝑥 · 𝐿 ) )
51		oveq1	⊢ ( 𝑛 = 𝑦 → ( 𝑛 · 𝐿 ) = ( 𝑦 · 𝐿 ) )
52		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( 𝑦 · 𝐿 ) ∈ V )
53	42 51 38 52	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) = ( 𝑦 · 𝐿 ) )
54	50 53	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) ) = ( ( 𝑥 · 𝐿 ) ( +g ‘ 𝐺 ) ( 𝑦 · 𝐿 ) ) )
55	41 47 54	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ ( 𝑥 + 𝑦 ) ) = ( ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 𝑦 ) ) )
56		oveq1	⊢ ( 𝑛 = 0 → ( 𝑛 · 𝐿 ) = ( 0 · 𝐿 ) )
57		0nn0	⊢ 0 ∈ ℕ0
58	57	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 0 ∈ ℕ0 )
59		ovexd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 0 · 𝐿 ) ∈ V )
60	42 56 58 59	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 0 ) = ( 0 · 𝐿 ) )
61	7	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝐿 ∈ 𝐵 )
62	3 28 4	mulg0	⊢ ( 𝐿 ∈ 𝐵 → ( 0 · 𝐿 ) = ( 0g ‘ 𝐺 ) )
63	61 62	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 0 · 𝐿 ) = ( 0g ‘ 𝐺 ) )
64	60 63	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ‘ 0 ) = ( 0g ‘ 𝐺 ) )
65	12 3 26 27 15 28 30 22 35 55 64	ismhmd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑛 · 𝐿 ) ) ∈ ( ( ℂfld ↾s ℕ0 ) MndHom 𝐺 ) )
66		elrabi	⊢ ( 𝑎 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } → 𝑎 ∈ 𝐷 )
67	66 2	eleq2s	⊢ ( 𝑎 ∈ 𝐻 → 𝑎 ∈ 𝐷 )
68	67	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 ∈ 𝐷 )
69	1	psrbagf	⊢ ( 𝑎 ∈ 𝐷 → 𝑎 : 𝐼 ⟶ ℕ0 )
70	68 69	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 : 𝐼 ⟶ ℕ0 )
71	70	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) ∧ 𝑣 ∈ 𝐼 ) → ( 𝑎 ‘ 𝑣 ) ∈ ℕ0 )
72	70	feqmptd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 = ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) )
73	1	psrbagfsupp	⊢ ( 𝑎 ∈ 𝐷 → 𝑎 finSupp 0 )
74	68 73	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → 𝑎 finSupp 0 )
75	72 74	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) finSupp 0 )
76		oveq1	⊢ ( 𝑛 = ( 𝑎 ‘ 𝑣 ) → ( 𝑛 · 𝐿 ) = ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) )
77		oveq1	⊢ ( 𝑛 = ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) → ( 𝑛 · 𝐿 ) = ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) )
78	12 15 21 22 23 65 71 75 76 77	gsummhm2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) ) ) = ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) )
79	72	oveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) )
80		oveq2	⊢ ( 𝑔 = 𝑎 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) )
81	80	eqeq1d	⊢ ( 𝑔 = 𝑎 → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 ↔ ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 ) )
82	81 2	elrab2	⊢ ( 𝑎 ∈ 𝐻 ↔ ( 𝑎 ∈ 𝐷 ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 ) )
83	82	simprbi	⊢ ( 𝑎 ∈ 𝐻 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 )
84	83	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg 𝑎 ) = 𝑁 )
85	79 84	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) = 𝑁 )
86	85	oveq1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( ( ( ℂfld ↾s ℕ0 ) Σg ( 𝑣 ∈ 𝐼 ↦ ( 𝑎 ‘ 𝑣 ) ) ) · 𝐿 ) = ( 𝑁 · 𝐿 ) )
87	78 86	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐻 ) → ( 𝐺 Σg ( 𝑣 ∈ 𝐼 ↦ ( ( 𝑎 ‘ 𝑣 ) · 𝐿 ) ) ) = ( 𝑁 · 𝐿 ) )