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 = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	mhphflem.h	$⊢ H = \{g \in D \| \sum_{ℂ_{fld} ↾_{𝑠} ℕ_{0}} g = N\}$
	mhphflem.k	$⊢ B = {Base}_{G}$
	mhphflem.e	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mhphflem.i	$⊢ φ \to I \in V$
	mhphflem.g	$⊢ φ \to G \in Mnd$
	mhphflem.l	$⊢ φ \to L \in B$
	mhphflem.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	mhphflem	$⊢ (φ \land a \in H) \to \underset{v \in I}{\sum_{G}} (a (v) \underset{˙}{\cdot} L) = N \underset{˙}{\cdot} L$

Proof

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

Metamath Proof Explorer

Theorem mhphflem

Proof