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		simpr	$⊢ ((φ \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 \in ran (v \in ((1 \dots N) repr (S) (M - b)) ⟼ v \cup \{⟨S, b⟩\})$
65		vex	$⊢ v \in V$
66		snex	$⊢ \{⟨S, b⟩\} \in V$
67	65 66	unex	$⊢ v \cup \{⟨S, b⟩\} \in V$
68	9 67	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⟩\}$
69	64 68	sylib	$⊢ ((φ \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⟩\}$
70	44 63 69	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)$
71	70	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)$
72	71 38	ffvelrnd	$⊢ (((φ \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)$
73	6 72	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 ℕ$
74		fveq2	$⊢ x = a \to L (x) = L (a)$
75	74	fveq1d	$⊢ x = a \to L (x) (y) = L (a) (y)$
76	75	eleq1d	$⊢ x = a \to (L (x) (y) \in ℂ \leftrightarrow L (a) (y) \in ℂ)$
77		fveq2	$⊢ y = d (a) \to L (a) (y) = L (a) (d (a))$
78	77	eleq1d	$⊢ y = d (a) \to (L (a) (y) \in ℂ \leftrightarrow L (a) (d (a)) \in ℂ)$
79	76 78	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 ℂ)$
80	38 73 79	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 ℂ)$
81	37 80	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 ℂ$
82	34 81	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 ℂ$
83	82	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 ℂ$
84	12 25 32 83	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))$
85	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\}$
86	85	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))$
87		nfv	$⊢ Ⅎ a ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b)))$
88		nfcv	$⊢ \underline{Ⅎ} a L (S) ((e \cup \{⟨S, b⟩\}) (S))$
89		fzofi	$⊢ (0 ..^S) \in Fin$
90	89	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (0 ..^S) \in Fin$
91	19	adantr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to S \in ℕ_{0}$
92	30	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \neg S \in (0 ..^S)$
93	6	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (1 \dots N) \subseteq ℕ$
94	18	adantr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to M - b \in ℤ$
95		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))$
96	93 94 91 95	reprf	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to e : (0 ..^S) ⟶ (1 \dots N)$
97	96	ffnd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to e Fn (0 ..^S)$
98	97	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)$
99	16	adantr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to b \in (1 \dots N)$
100		fnsng	$⊢ (S \in ℕ_{0} \land b \in (1 \dots N)) \to \{⟨S, b⟩\} Fn \{S\}$
101	91 99 100	syl2anc	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \{⟨S, b⟩\} Fn \{S\}$
102	101	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\}$
103	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$
104		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)$
105		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)$
106	98 102 103 104 105	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)$
107	106	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))$
108	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 ℂ$
109	108	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 ℂ$
110		fzossfzop1	$⊢ S \in ℕ_{0} \to (0 ..^S) \subseteq (0 ..^S + 1)$
111	2 110	syl	$⊢ φ \to (0 ..^S) \subseteq (0 ..^S + 1)$
112	111	ad2antrr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (0 ..^S) \subseteq (0 ..^S + 1)$
113	112	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)$
114	96	ffvelrnda	$⊢ (((φ \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)$
115	6 114	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 ℕ$
116		fveq2	$⊢ y = e (a) \to L (a) (y) = L (a) (e (a))$
117	116	eleq1d	$⊢ y = e (a) \to (L (a) (y) \in ℂ \leftrightarrow L (a) (e (a)) \in ℂ)$
118	76 117	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 ℂ)$
119	113 115 118	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 ℂ)$
120	109 119	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 ℂ$
121	107 120	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 ℂ$
122		fveq2	$⊢ a = S \to L (a) = L (S)$
123		fveq2	$⊢ a = S \to (e \cup \{⟨S, b⟩\}) (a) = (e \cup \{⟨S, b⟩\}) (S)$
124	122 123	fveq12d	$⊢ a = S \to L (a) ((e \cup \{⟨S, b⟩\}) (a)) = L (S) ((e \cup \{⟨S, b⟩\}) (S))$
125	52	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (0 ..^S) \cap \{S\} = \emptyset$
126		snidg	$⊢ S \in ℕ_{0} \to S \in \{S\}$
127	91 126	syl	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to S \in \{S\}$
128		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)$
129	97 101 125 127 128	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)$
130		fvsng	$⊢ (S \in ℕ_{0} \land b \in (1 \dots N)) \to \{⟨S, b⟩\} (S) = b$
131	91 99 130	syl2anc	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to \{⟨S, b⟩\} (S) = b$
132	129 131	eqtrd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to (e \cup \{⟨S, b⟩\}) (S) = b$
133	132	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)$
134		fzonn0p1	$⊢ S \in ℕ_{0} \to S \in (0 ..^S + 1)$
135	2 134	syl	$⊢ φ \to S \in (0 ..^S + 1)$
136	135	ad2antrr	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to S \in (0 ..^S + 1)$
137	6 99	sselid	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to b \in ℕ$
138		fveq2	$⊢ x = S \to L (x) = L (S)$
139	138	fveq1d	$⊢ x = S \to L (x) (y) = L (S) (y)$
140	139	eleq1d	$⊢ x = S \to (L (x) (y) \in ℂ \leftrightarrow L (S) (y) \in ℂ)$
141		fveq2	$⊢ y = b \to L (S) (y) = L (S) (b)$
142	141	eleq1d	$⊢ y = b \to (L (S) (y) \in ℂ \leftrightarrow L (S) (b) \in ℂ)$
143	140 142	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 ℂ)$
144	136 137 143	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 ℂ)$
145	108 144	mpd	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to L (S) (b) \in ℂ$
146	133 145	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 ℂ$
147	87 88 90 91 92 121 124 146	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))$
148	107	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))$
149	148 133	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)$
150	86 147 149	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)$
151	150	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)$
152		simpl	$⊢ (d = e \cup \{⟨S, b⟩\} \land a \in (0 ..^S + 1)) \to d = e \cup \{⟨S, b⟩\}$
153	152	fveq1d	$⊢ (d = e \cup \{⟨S, b⟩\} \land a \in (0 ..^S + 1)) \to d (a) = (e \cup \{⟨S, b⟩\}) (a)$
154	153	fveq2d	$⊢ (d = e \cup \{⟨S, b⟩\} \land a \in (0 ..^S + 1)) \to L (a) (d (a)) = L (a) ((e \cup \{⟨S, b⟩\}) (a))$
155	154	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))$
156	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⟩\})$
157	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⟩\})$
158		simpr	$⊢ (((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \land v = e) \to v = e$
159	158	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⟩\}$
160		vex	$⊢ e \in V$
161	160 66	unex	$⊢ e \cup \{⟨S, b⟩\} \in V$
162	161	a1i	$⊢ ((φ \land b \in (1 \dots N)) \land e \in ((1 \dots N) repr (S) (M - b))) \to e \cup \{⟨S, b⟩\} \in V$
163	157 159 95 162	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⟩\}$
164	155 21 156 163 82	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))$
165		simpl	$⊢ (d = e \land a \in (0 ..^S)) \to d = e$
166	165	fveq1d	$⊢ (d = e \land a \in (0 ..^S)) \to d (a) = e (a)$
167	166	fveq2d	$⊢ (d = e \land a \in (0 ..^S)) \to L (a) (d (a)) = L (a) (e (a))$
168	167	prodeq2dv	$⊢ d = e \to \prod_{a \in (0 ..^S)} L (a) (d (a)) = \prod_{a \in (0 ..^S)} L (a) (e (a))$
169	168	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)$
170	169	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)$
171	170	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)$
172	151 164 171	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)$
173	172	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)$
174	11 84 173	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