breprexplema

Description: Lemma for breprexp (induction step for weighted sums over representations). (Contributed by Thierry Arnoux, 7-Dec-2021)

	Ref	Expression
Hypotheses	breprexp.n	$⊢ φ \to N \in ℕ_{0}$
	breprexp.s	$⊢ φ \to S \in ℕ_{0}$
	breprexplema.m	$⊢ φ \to M \in ℕ_{0}$
	breprexplema.1	$⊢ φ \to M \leq (S + 1) \cdot N$
	breprexplema.l	$⊢ ((φ \land x \in (0 ..^S + 1)) \land y \in ℕ) \to L (x) (y) \in ℂ$
Assertion	breprexplema	$⊢ φ \to \sum_{d \in (1 \dots N) repr (S + 1) M} \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) = \sum_{b = 1}^{N} \sum_{d \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (d (a)) L (S) (b)$

Proof

Step	Hyp	Ref	Expression
1		breprexp.n	$⊢ φ \to N \in ℕ_{0}$
2		breprexp.s	$⊢ φ \to S \in ℕ_{0}$
3		breprexplema.m	$⊢ φ \to M \in ℕ_{0}$
4		breprexplema.1	$⊢ φ \to M \leq (S + 1) \cdot N$
5		breprexplema.l	$⊢ ((φ \land x \in (0 ..^S + 1)) \land y \in ℕ) \to L (x) (y) \in ℂ$
6		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
7	6	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
8	3	nn0zd	$⊢ φ \to M \in ℤ$
9		eqid	$⊢ (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) = (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
10	7 8 2 9	reprsuc	$⊢ φ \to (1 \dots N) repr (S + 1) M = ⋃_{b = 1}^{N} ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
11	10	sumeq1d	$⊢ φ \to \sum_{d \in (1 \dots N) repr (S + 1) M} \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) = \sum_{d \in ⋃_{b = 1}^{N} ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})} \prod_{a \in (0 ..^S + 1)} L (a) (d (a))$
12		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
13	6	a1i	$⊢ (φ \land b \in (1 \dots N)) \to (1 \dots N) \subseteq ℕ$
14	8	adantr	$⊢ (φ \land b \in (1 \dots N)) \to M \in ℤ$
15		fzssz	$⊢ (1 \dots N) \subseteq ℤ$
16		simpr	$⊢ (φ \land b \in (1 \dots N)) \to b \in (1 \dots N)$
17	15 16	sselid	$⊢ (φ \land b \in (1 \dots N)) \to b \in ℤ$
18	14 17	zsubcld	$⊢ (φ \land b \in (1 \dots N)) \to M - b \in ℤ$
19	2	adantr	$⊢ (φ \land b \in (1 \dots N)) \to S \in ℕ_{0}$
20	12	adantr	$⊢ (φ \land b \in (1 \dots N)) \to (1 \dots N) \in Fin$
21	13 18 19 20	reprfi	$⊢ (φ \land b \in (1 \dots N)) \to (1 \dots N) repr (S) (M - b) \in Fin$
22		mptfi	$⊢ (1 \dots N) repr (S) (M - b) \in Fin \to (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) \in Fin$
23	21 22	syl	$⊢ (φ \land b \in (1 \dots N)) \to (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) \in Fin$
24		rnfi	$⊢ (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) \in Fin \to ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) \in Fin$
25	23 24	syl	$⊢ (φ \land b \in (1 \dots N)) \to ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) \in Fin$
26	13 18 19	reprval	$⊢ (φ \land b \in (1 \dots N)) \to (1 \dots N) repr (S) (M - b) = \{c \in ({(1 \dots N)}^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M - b\}$
27		ssrab2	$⊢ \{c \in ({(1 \dots N)}^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M - b\} \subseteq {(1 \dots N)}^{(0 ..^S)}$
28	26 27	eqsstrdi	$⊢ (φ \land b \in (1 \dots N)) \to (1 \dots N) repr (S) (M - b) \subseteq {(1 \dots N)}^{(0 ..^S)}$
29	12	elexd	$⊢ φ \to (1 \dots N) \in V$
30		fzonel	$⊢ \neg S \in (0 ..^S)$
31	30	a1i	$⊢ φ \to \neg S \in (0 ..^S)$
32	28 29 2 31 9	actfunsnrndisj	$⊢ φ \to {Disj}_{b = 1}^{N} ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
33		fzofi	$⊢ (0 ..^S + 1) \in Fin$
34	33	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \to (0 ..^S + 1) \in Fin$
35	5	ralrimiva	$⊢ (φ \land x \in (0 ..^S + 1)) \to \forall y \in ℕ L (x) (y) \in ℂ$
36	35	ralrimiva	$⊢ φ \to \forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ$
37	36	ad3antrrr	$⊢ (((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land a \in (0 ..^S + 1)) \to \forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ$
38		simpr	$⊢ (((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land a \in (0 ..^S + 1)) \to a \in (0 ..^S + 1)$
39		nfv	$⊢ Ⅎ v (φ \land b \in (1 \dots N))$
40		nfcv	$⊢ \underline{Ⅎ} v d$
41		nfmpt1	$⊢ \underline{Ⅎ} v (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
42	41	nfrn	$⊢ \underline{Ⅎ} v ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
43	40 42	nfel	$⊢ Ⅎ v d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
44	39 43	nfan	$⊢ Ⅎ v ((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}))$
45	6	a1i	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to (1 \dots N) \subseteq ℕ$
46	18	ad3antrrr	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to M - b \in ℤ$
47	19	ad3antrrr	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to S \in ℕ_{0}$
48		simplr	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to v \in ((1 \dots N) repr (S) (M - b))$
49	45 46 47 48	reprf	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to v : (0 ..^S) ⟶ (1 \dots N)$
50	16	ad3antrrr	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to b \in (1 \dots N)$
51	47 50	fsnd	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to \{⟨S, b⟩\} : \{S\} ⟶ (1 \dots N)$
52		fzodisjsn	$⊢ (0 ..^S) \cap \{S\} = \emptyset$
53	52	a1i	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to (0 ..^S) \cap \{S\} = \emptyset$
54		fun2	$⊢ ((v : (0 ..^S) ⟶ (1 \dots N) \land \{⟨S, b⟩\} : \{S\} ⟶ (1 \dots N)) \land (0 ..^S) \cap \{S\} = \emptyset) \to (v \cup \{⟨S, b⟩\}) : (0 ..^S) \cup \{S\} ⟶ (1 \dots N)$
55	49 51 53 54	syl21anc	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to (v \cup \{⟨S, b⟩\}) : (0 ..^S) \cup \{S\} ⟶ (1 \dots N)$
56		simpr	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to d = v \cup \{⟨S, b⟩\}$
57		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
58	2 57	eleqtrdi	$⊢ φ \to S \in ℤ_{\geq 0}$
59		fzosplitsn	$⊢ S \in ℤ_{\geq 0} \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
60	58 59	syl	$⊢ φ \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
61	60	ad4antr	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
62	56 61	feq12d	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to (d : (0 ..^S + 1) ⟶ (1 \dots N) \leftrightarrow (v \cup \{⟨S, b⟩\}) : (0 ..^S) \cup \{S\} ⟶ (1 \dots N))$
63	55 62	mpbird	$⊢ ((((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land v \in ((1 \dots N) repr (S) (M - b))) \land d = v \cup \{⟨S, b⟩\}) \to d : (0 ..^S + 1) ⟶ (1 \dots N)$
64		vex	$⊢ v \in V$
65		snex	$⊢ \{⟨S, b⟩\} \in V$
66	64 65	unex	$⊢ v \cup \{⟨S, b⟩\} \in V$
67	9 66	elrnmpti	$⊢ d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) \leftrightarrow \exists v \in ((1 \dots N) repr (S) (M - b)) d = v \cup \{⟨S, b⟩\}$
68	67	bilani	$⊢ ((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \to \exists v \in ((1 \dots N) repr (S) (M - b)) d = v \cup \{⟨S, b⟩\}$
69	44 63 68	r19.29af	$⊢ ((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \to d : (0 ..^S + 1) ⟶ (1 \dots N)$
70	69	adantr	$⊢ (((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land a \in (0 ..^S + 1)) \to d : (0 ..^S + 1) ⟶ (1 \dots N)$
71	70 38	ffvelcdmd	$⊢ (((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land a \in (0 ..^S + 1)) \to d (a) \in (1 \dots N)$
72	6 71	sselid	$⊢ (((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land a \in (0 ..^S + 1)) \to d (a) \in ℕ$
73		fveq2	$⊢ x = a \to L (x) = L (a)$
74	73	fveq1d	$⊢ x = a \to L (x) (y) = L (a) (y)$
75	74	eleq1d	$⊢ x = a \to (L (x) (y) \in ℂ \leftrightarrow L (a) (y) \in ℂ)$
76		fveq2	$⊢ y = d (a) \to L (a) (y) = L (a) (d (a))$
77	76	eleq1d	$⊢ y = d (a) \to (L (a) (y) \in ℂ \leftrightarrow L (a) (d (a)) \in ℂ)$
78	75 77	rspc2v	$⊢ (a \in (0 ..^S + 1) \land d (a) \in ℕ) \to (\forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ \to L (a) (d (a)) \in ℂ)$
79	38 72 78	syl2anc	$⊢ (((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land a \in (0 ..^S + 1)) \to (\forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ \to L (a) (d (a)) \in ℂ)$
80	37 79	mpd	$⊢ (((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \land a \in (0 ..^S + 1)) \to L (a) (d (a)) \in ℂ$
81	34 80	fprodcl	$⊢ ((φ \land b \in (1 \dots N)) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})) \to \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) \in ℂ$
82	81	anasss	$⊢ (φ \land (b \in (1 \dots N) \land d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}))) \to \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) \in ℂ$
83	12 25 32 82	fsumiun	$⊢ φ \to \sum_{d \in ⋃_{b = 1}^{N} ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})} \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) = \sum_{b = 1}^{N} \sum_{d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})} \prod_{a \in (0 ..^S + 1)} L (a) (d (a))$
84	60	ad2antrr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
85	84	prodeq1d	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \prod_{a \in (0 ..^S + 1)} L (a) ((e \cup \{⟨S, b⟩\}) (a)) = \prod_{a \in (0 ..^S) \cup \{S\}} L (a) ((e \cup \{⟨S, b⟩\}) (a))$
86		nfv	$⊢ Ⅎ a ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b)))$
87		nfcv	$⊢ \underline{Ⅎ} a L (S) ((e \cup \{⟨S, b⟩\}) (S))$
88		fzofi	$⊢ (0 ..^S) \in Fin$
89	88	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (0 ..^S) \in Fin$
90	19	adantr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to S \in ℕ_{0}$
91	30	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \neg S \in (0 ..^S)$
92	6	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (1 \dots N) \subseteq ℕ$
93	18	adantr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to M - b \in ℤ$
94		simpr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to e \in ((1 \dots N) repr (S) (M - b))$
95	92 93 90 94	reprf	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to e : (0 ..^S) ⟶ (1 \dots N)$
96	95	ffnd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to e Fn (0 ..^S)$
97	96	adantr	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to e Fn (0 ..^S)$
98	16	adantr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to b \in (1 \dots N)$
99		fnsng	$⊢ (S \in ℕ_{0} \land b \in (1 \dots N)) \to \{⟨S, b⟩\} Fn \{S\}$
100	90 98 99	syl2anc	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \{⟨S, b⟩\} Fn \{S\}$
101	100	adantr	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to \{⟨S, b⟩\} Fn \{S\}$
102	52	a1i	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to (0 ..^S) \cap \{S\} = \emptyset$
103		simpr	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
104		fvun1	$⊢ (e Fn (0 ..^S) \land \{⟨S, b⟩\} Fn \{S\} \land ((0 ..^S) \cap \{S\} = \emptyset \land a \in (0 ..^S))) \to (e \cup \{⟨S, b⟩\}) (a) = e (a)$
105	97 101 102 103 104	syl112anc	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to (e \cup \{⟨S, b⟩\}) (a) = e (a)$
106	105	fveq2d	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to L (a) ((e \cup \{⟨S, b⟩\}) (a)) = L (a) (e (a))$
107	36	ad2antrr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ$
108	107	adantr	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to \forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ$
109		fzossfzop1	$⊢ S \in ℕ_{0} \to (0 ..^S) \subseteq (0 ..^S + 1)$
110	2 109	syl	$⊢ φ \to (0 ..^S) \subseteq (0 ..^S + 1)$
111	110	ad2antrr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (0 ..^S) \subseteq (0 ..^S + 1)$
112	111	sselda	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to a \in (0 ..^S + 1)$
113	95	ffvelcdmda	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to e (a) \in (1 \dots N)$
114	6 113	sselid	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to e (a) \in ℕ$
115		fveq2	$⊢ y = e (a) \to L (a) (y) = L (a) (e (a))$
116	115	eleq1d	$⊢ y = e (a) \to (L (a) (y) \in ℂ \leftrightarrow L (a) (e (a)) \in ℂ)$
117	75 116	rspc2v	$⊢ (a \in (0 ..^S + 1) \land e (a) \in ℕ) \to (\forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ \to L (a) (e (a)) \in ℂ)$
118	112 114 117	syl2anc	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to (\forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ \to L (a) (e (a)) \in ℂ)$
119	108 118	mpd	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to L (a) (e (a)) \in ℂ$
120	106 119	eqeltrd	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land a \in (0 ..^S)) \to L (a) ((e \cup \{⟨S, b⟩\}) (a)) \in ℂ$
121		fveq2	$⊢ a = S \to L (a) = L (S)$
122		fveq2	$⊢ a = S \to (e \cup \{⟨S, b⟩\}) (a) = (e \cup \{⟨S, b⟩\}) (S)$
123	121 122	fveq12d	$⊢ a = S \to L (a) ((e \cup \{⟨S, b⟩\}) (a)) = L (S) ((e \cup \{⟨S, b⟩\}) (S))$
124	52	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (0 ..^S) \cap \{S\} = \emptyset$
125		snidg	$⊢ S \in ℕ_{0} \to S \in \{S\}$
126	90 125	syl	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to S \in \{S\}$
127		fvun2	$⊢ (e Fn (0 ..^S) \land \{⟨S, b⟩\} Fn \{S\} \land ((0 ..^S) \cap \{S\} = \emptyset \land S \in \{S\})) \to (e \cup \{⟨S, b⟩\}) (S) = \{⟨S, b⟩\} (S)$
128	96 100 124 126 127	syl112anc	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (e \cup \{⟨S, b⟩\}) (S) = \{⟨S, b⟩\} (S)$
129		fvsng	$⊢ (S \in ℕ_{0} \land b \in (1 \dots N)) \to \{⟨S, b⟩\} (S) = b$
130	90 98 129	syl2anc	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \{⟨S, b⟩\} (S) = b$
131	128 130	eqtrd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (e \cup \{⟨S, b⟩\}) (S) = b$
132	131	fveq2d	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to L (S) ((e \cup \{⟨S, b⟩\}) (S)) = L (S) (b)$
133		fzonn0p1	$⊢ S \in ℕ_{0} \to S \in (0 ..^S + 1)$
134	2 133	syl	$⊢ φ \to S \in (0 ..^S + 1)$
135	134	ad2antrr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to S \in (0 ..^S + 1)$
136	6 98	sselid	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to b \in ℕ$
137		fveq2	$⊢ x = S \to L (x) = L (S)$
138	137	fveq1d	$⊢ x = S \to L (x) (y) = L (S) (y)$
139	138	eleq1d	$⊢ x = S \to (L (x) (y) \in ℂ \leftrightarrow L (S) (y) \in ℂ)$
140		fveq2	$⊢ y = b \to L (S) (y) = L (S) (b)$
141	140	eleq1d	$⊢ y = b \to (L (S) (y) \in ℂ \leftrightarrow L (S) (b) \in ℂ)$
142	139 141	rspc2v	$⊢ (S \in (0 ..^S + 1) \land b \in ℕ) \to (\forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ \to L (S) (b) \in ℂ)$
143	135 136 142	syl2anc	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (\forall x \in (0 ..^S + 1) \forall y \in ℕ L (x) (y) \in ℂ \to L (S) (b) \in ℂ)$
144	107 143	mpd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to L (S) (b) \in ℂ$
145	132 144	eqeltrd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to L (S) ((e \cup \{⟨S, b⟩\}) (S)) \in ℂ$
146	86 87 89 90 91 120 123 145	fprodsplitsn	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \prod_{a \in (0 ..^S) \cup \{S\}} L (a) ((e \cup \{⟨S, b⟩\}) (a)) = \prod_{a \in (0 ..^S)} L (a) ((e \cup \{⟨S, b⟩\}) (a)) L (S) ((e \cup \{⟨S, b⟩\}) (S))$
147	106	prodeq2dv	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \prod_{a \in (0 ..^S)} L (a) ((e \cup \{⟨S, b⟩\}) (a)) = \prod_{a \in (0 ..^S)} L (a) (e (a))$
148	147 132	oveq12d	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \prod_{a \in (0 ..^S)} L (a) ((e \cup \{⟨S, b⟩\}) (a)) L (S) ((e \cup \{⟨S, b⟩\}) (S)) = \prod_{a \in (0 ..^S)} L (a) (e (a)) L (S) (b)$
149	85 146 148	3eqtrd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \prod_{a \in (0 ..^S + 1)} L (a) ((e \cup \{⟨S, b⟩\}) (a)) = \prod_{a \in (0 ..^S)} L (a) (e (a)) L (S) (b)$
150	149	sumeq2dv	$⊢ (φ \land b \in (1 \dots N)) \to \sum_{e \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S + 1)} L (a) ((e \cup \{⟨S, b⟩\}) (a)) = \sum_{e \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (e (a)) L (S) (b)$
151		simpl	$⊢ (d = e \cup \{⟨S, b⟩\} \land a \in (0 ..^S + 1)) \to d = e \cup \{⟨S, b⟩\}$
152	151	fveq1d	$⊢ (d = e \cup \{⟨S, b⟩\} \land a \in (0 ..^S + 1)) \to d (a) = (e \cup \{⟨S, b⟩\}) (a)$
153	152	fveq2d	$⊢ (d = e \cup \{⟨S, b⟩\} \land a \in (0 ..^S + 1)) \to L (a) (d (a)) = L (a) ((e \cup \{⟨S, b⟩\}) (a))$
154	153	prodeq2dv	$⊢ d = e \cup \{⟨S, b⟩\} \to \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) = \prod_{a \in (0 ..^S + 1)} L (a) ((e \cup \{⟨S, b⟩\}) (a))$
155	28 29 2 31 9	actfunsnf1o	$⊢ (φ \land b \in (1 \dots N)) \to (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) : (1 \dots N) repr (S) (M - b) \underset{1-1 onto}{⟶} ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
156	9	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) = (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
157		simpr	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land v = e) \to v = e$
158	157	uneq1d	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land v = e) \to v \cup \{⟨S, b⟩\} = e \cup \{⟨S, b⟩\}$
159		vex	$⊢ e \in V$
160	159 65	unex	$⊢ e \cup \{⟨S, b⟩\} \in V$
161	160	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to e \cup \{⟨S, b⟩\} \in V$
162	156 158 94 161	fvmptd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\}) (e) = e \cup \{⟨S, b⟩\}$
163	154 21 155 162 81	fsumf1o	$⊢ (φ \land b \in (1 \dots N)) \to \sum_{d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})} \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) = \sum_{e \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S + 1)} L (a) ((e \cup \{⟨S, b⟩\}) (a))$
164		simpl	$⊢ (d = e \land a \in (0 ..^S)) \to d = e$
165	164	fveq1d	$⊢ (d = e \land a \in (0 ..^S)) \to d (a) = e (a)$
166	165	fveq2d	$⊢ (d = e \land a \in (0 ..^S)) \to L (a) (d (a)) = L (a) (e (a))$
167	166	prodeq2dv	$⊢ d = e \to \prod_{a \in (0 ..^S)} L (a) (d (a)) = \prod_{a \in (0 ..^S)} L (a) (e (a))$
168	167	oveq1d	$⊢ d = e \to \prod_{a \in (0 ..^S)} L (a) (d (a)) L (S) (b) = \prod_{a \in (0 ..^S)} L (a) (e (a)) L (S) (b)$
169	168	cbvsumv	$⊢ \sum_{d \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (d (a)) L (S) (b) = \sum_{e \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (e (a)) L (S) (b)$
170	169	a1i	$⊢ (φ \land b \in (1 \dots N)) \to \sum_{d \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (d (a)) L (S) (b) = \sum_{e \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (e (a)) L (S) (b)$
171	150 163 170	3eqtr4d	$⊢ (φ \land b \in (1 \dots N)) \to \sum_{d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})} \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) = \sum_{d \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (d (a)) L (S) (b)$
172	171	sumeq2dv	$⊢ φ \to \sum_{b = 1}^{N} \sum_{d \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})} \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) = \sum_{b = 1}^{N} \sum_{d \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (d (a)) L (S) (b)$
173	11 83 172	3eqtrd	$⊢ φ \to \sum_{d \in (1 \dots N) repr (S + 1) M} \prod_{a \in (0 ..^S + 1)} L (a) (d (a)) = \sum_{b = 1}^{N} \sum_{d \in (1 \dots N) repr (S) (M - b)} \prod_{a \in (0 ..^S)} L (a) (d (a)) L (S) (b)$

Metamath Proof Explorer

Theorem breprexplema

Proof