Theorem breprexplema 34881

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

Hypotheses

Ref	Expression
breprexp.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)
breprexp.s	⊢ (𝜑 → 𝑆 ∈ ℕ0)
breprexplema.m	⊢ (𝜑 → 𝑀 ∈ ℕ0)
breprexplema.1	⊢ (𝜑 → 𝑀 ≤ ((𝑆 + 1) · 𝑁))
breprexplema.l	⊢ (((𝜑 ∧ 𝑥 ∈ (0..^(𝑆 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿‘𝑥)‘𝑦) ∈ ℂ)

Assertion

Ref	Expression
breprexplema	⊢ (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))

Distinct variable groups:   𝑆,𝑎   𝐿,𝑎,𝑏,𝑑,𝑥,𝑦   𝑀,𝑎,𝑏,𝑑   𝑁,𝑎,𝑏,𝑑   𝑆,𝑏,𝑑,𝑥,𝑦   𝜑,𝑎,𝑏,𝑑,𝑥,𝑦

Allowed substitution hints:   𝑀(𝑥,𝑦)   𝑁(𝑥,𝑦)

Proof of Theorem breprexplema

Dummy variables 𝑐 𝑒 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fz1ssnn 13550	. . . . 5 ⊢ (1...𝑁) ⊆ ℕ
2	1	a1i 11	. . . 4 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
3		breprexplema.m	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
4	3	nn0zd 12583	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℤ)
5		breprexp.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ ℕ0)
6		eqid 2756	. . . 4 ⊢ (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) = (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
7	2, 4, 5, 6	reprsuc 34866	. . 3 ⊢ (𝜑 → ((1...𝑁)(repr‘(𝑆 + 1))𝑀) = ∪ 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
8	7	sumeq1d 15703	. 2 ⊢ (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∪ 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)))
9		fzfid 13976	. . 3 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
10	1	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
11	4	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑀 ∈ ℤ)
12		fzssz 13521	. . . . . . . 8 ⊢ (1...𝑁) ⊆ ℤ
13		simpr 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
14	12, 13	sselid 3929	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
15	11, 14	zsubcld 12672	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑀 − 𝑏) ∈ ℤ)
16	5	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
17	9	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
18	10, 15, 16, 17	reprfi 34867	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ∈ Fin)
19		mptfi 9284	. . . . 5 ⊢ (((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ∈ Fin → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin)
20	18, 19	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin)
21		rnfi 9273	. . . 4 ⊢ ((𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin → ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin)
22	20, 21	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin)
23	10, 15, 16	reprval 34861	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) = {𝑐 ∈ ((1...𝑁) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏)})
24		ssrab2 4028	. . . . 5 ⊢ {𝑐 ∈ ((1...𝑁) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏)} ⊆ ((1...𝑁) ↑m (0..^𝑆))
25	23, 24	eqsstrdi 3975	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ⊆ ((1...𝑁) ↑m (0..^𝑆)))
26	9	elexd 3471	. . . 4 ⊢ (𝜑 → (1...𝑁) ∈ V)
27		fzonel 13669	. . . . 5 ⊢ ¬ 𝑆 ∈ (0..^𝑆)
28	27	a1i 11	. . . 4 ⊢ (𝜑 → ¬ 𝑆 ∈ (0..^𝑆))
29	25, 26, 5, 28, 6	actfunsnrndisj 34856	. . 3 ⊢ (𝜑 → Disj 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
30		fzofi 13977	. . . . . 6 ⊢ (0..^(𝑆 + 1)) ∈ Fin
31	30	a1i 11	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → (0..^(𝑆 + 1)) ∈ Fin)
32		breprexplema.l	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (0..^(𝑆 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
33	32	ralrimiva 3148	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(𝑆 + 1))) → ∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
34	33	ralrimiva 3148	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
35	34	ad3antrrr 738	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
36		simpr 487	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑎 ∈ (0..^(𝑆 + 1)))
37		nfv 1928	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣(𝜑 ∧ 𝑏 ∈ (1...𝑁))
38		nfcv 2918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣𝑑
39		nfmpt1 5193	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣(𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
40	39	nfrn 5921	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑣ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
41	38, 40	nfel 2932	. . . . . . . . . . . 12 ⊢ Ⅎ𝑣 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
42	37, 41	nfan 1913	. . . . . . . . . . 11 ⊢ Ⅎ𝑣((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
43	1	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (1...𝑁) ⊆ ℕ)
44	15	ad3antrrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀 − 𝑏) ∈ ℤ)
45	16	ad3antrrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ0)
46		simplr 776	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)))
47	43, 44, 45, 46	reprf 34863	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑣:(0..^𝑆)⟶(1...𝑁))
48	13	ad3antrrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ (1...𝑁))
49	45, 48	fsnd 6840	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶(1...𝑁))
50		fzodisjsn 13693	. . . . . . . . . . . . . 14 ⊢ ((0..^𝑆) ∩ {𝑆}) = ∅
51	50	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
52		fun2 6716	. . . . . . . . . . . . 13 ⊢ (((𝑣:(0..^𝑆)⟶(1...𝑁) ∧ {⟨𝑆, 𝑏⟩}:{𝑆}⟶(1...𝑁)) ∧ ((0..^𝑆) ∩ {𝑆}) = ∅) → (𝑣 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁))
53	47, 49, 51, 52	syl21anc 846	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (𝑣 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁))
54		simpr 487	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
55		nn0uz 12867	. . . . . . . . . . . . . . . 16 ⊢ ℕ0 = (ℤ≥‘0)
56	5, 55	eleqtrdi 2866	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘0))
57		fzosplitsn 13772	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ (ℤ≥‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
58	56, 57	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
59	58	ad4antr 740	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
60	54, 59	feq12d 6668	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (𝑑:(0..^(𝑆 + 1))⟶(1...𝑁) ↔ (𝑣 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁)))
61	53, 60	mpbird 259	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁))
62		vex 3452	. . . . . . . . . . . . . 14 ⊢ 𝑣 ∈ V
63		snex 5390	. . . . . . . . . . . . . 14 ⊢ {⟨𝑆, 𝑏⟩} ∈ V
64	62, 63	unex 7716	. . . . . . . . . . . . 13 ⊢ (𝑣 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
65	6, 64	elrnmpti 5931	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ↔ ∃𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
66	65	bilani 507	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → ∃𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
67	42, 61, 66	r19.29af 3265	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁))
68	67	adantr 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁))
69	68, 36	ffvelcdmd 7055	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) ∈ (1...𝑁))
70	1, 69	sselid 3929	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) ∈ ℕ)
71		fveq2 6856	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝐿‘𝑥) = (𝐿‘𝑎))
72	71	fveq1d 6858	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → ((𝐿‘𝑥)‘𝑦) = ((𝐿‘𝑎)‘𝑦))
73	72	eleq1d 2841	. . . . . . . 8 ⊢ (𝑥 = 𝑎 → (((𝐿‘𝑥)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘𝑦) ∈ ℂ))
74		fveq2 6856	. . . . . . . . 9 ⊢ (𝑦 = (𝑑‘𝑎) → ((𝐿‘𝑎)‘𝑦) = ((𝐿‘𝑎)‘(𝑑‘𝑎)))
75	74	eleq1d 2841	. . . . . . . 8 ⊢ (𝑦 = (𝑑‘𝑎) → (((𝐿‘𝑎)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ))
76	73, 75	rspc2v 3587	. . . . . . 7 ⊢ ((𝑎 ∈ (0..^(𝑆 + 1)) ∧ (𝑑‘𝑎) ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ))
77	36, 70, 76	syl2anc 592	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ))
78	35, 77	mpd 15	. . . . 5 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
79	31, 78	fprodcl 15958	. . . 4 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
80	79	anasss 469	. . 3 ⊢ ((𝜑 ∧ (𝑏 ∈ (1...𝑁) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
81	9, 22, 29, 80	fsumiun 15825	. 2 ⊢ (𝜑 → Σ𝑑 ∈ ∪ 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)))
82	58	ad2antrr 734	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
83	82	prodeq1d 15926	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = ∏𝑎 ∈ ((0..^𝑆) ∪ {𝑆})((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)))
84		nfv 1928	. . . . . . 7 ⊢ Ⅎ𝑎((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)))
85		nfcv 2918	. . . . . . 7 ⊢ Ⅎ𝑎((𝐿‘𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
86		fzofi 13977	. . . . . . . 8 ⊢ (0..^𝑆) ∈ Fin
87	86	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^𝑆) ∈ Fin)
88	16	adantr 483	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ ℕ0)
89	27	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ¬ 𝑆 ∈ (0..^𝑆))
90	1	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (1...𝑁) ⊆ ℕ)
91	15	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑀 − 𝑏) ∈ ℤ)
92		simpr 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)))
93	90, 91, 88, 92	reprf 34863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒:(0..^𝑆)⟶(1...𝑁))
94	93	ffnd 6681	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒 Fn (0..^𝑆))
95	94	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 Fn (0..^𝑆))
96	13	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ (1...𝑁))
97		fnsng 6562	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ ℕ0 ∧ 𝑏 ∈ (1...𝑁)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
98	88, 96, 97	syl2anc 592	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
99	98	adantr 483	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
100	50	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
101		simpr 487	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
102		fvun1 6947	. . . . . . . . . 10 ⊢ ((𝑒 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑒‘𝑎))
103	95, 99, 100, 101, 102	syl112anc 1389	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑒‘𝑎))
104	103	fveq2d 6860	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = ((𝐿‘𝑎)‘(𝑒‘𝑎)))
105	34	ad2antrr 734	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
106	105	adantr 483	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
107		fzossfzop1 13739	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ ℕ0 → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
108	5, 107	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
109	108	ad2antrr 734	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
110	109	sselda 3931	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
111	93	ffvelcdmda 7054	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ (1...𝑁))
112	1, 111	sselid 3929	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℕ)
113		fveq2 6856	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑒‘𝑎) → ((𝐿‘𝑎)‘𝑦) = ((𝐿‘𝑎)‘(𝑒‘𝑎)))
114	113	eleq1d 2841	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑒‘𝑎) → (((𝐿‘𝑎)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ))
115	73, 114	rspc2v 3587	. . . . . . . . . 10 ⊢ ((𝑎 ∈ (0..^(𝑆 + 1)) ∧ (𝑒‘𝑎) ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ))
116	110, 112, 115	syl2anc 592	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ))
117	106, 116	mpd 15	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ)
118	104, 117	eqeltrd 2856	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) ∈ ℂ)
119		fveq2 6856	. . . . . . . 8 ⊢ (𝑎 = 𝑆 → (𝐿‘𝑎) = (𝐿‘𝑆))
120		fveq2 6856	. . . . . . . 8 ⊢ (𝑎 = 𝑆 → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
121	119, 120	fveq12d 6863	. . . . . . 7 ⊢ (𝑎 = 𝑆 → ((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = ((𝐿‘𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆)))
122	50	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
123		snidg 4613	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ ℕ0 → 𝑆 ∈ {𝑆})
124	88, 123	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ {𝑆})
125		fvun2 6948	. . . . . . . . . . 11 ⊢ ((𝑒 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
126	94, 98, 122, 124, 125	syl112anc 1389	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
127		fvsng 7153	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ ℕ0 ∧ 𝑏 ∈ (1...𝑁)) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
128	88, 96, 127	syl2anc 592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
129	126, 128	eqtrd 2791	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = 𝑏)
130	129	fveq2d 6860	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆)) = ((𝐿‘𝑆)‘𝑏))
131		fzonn0p1 13738	. . . . . . . . . . . 12 ⊢ (𝑆 ∈ ℕ0 → 𝑆 ∈ (0..^(𝑆 + 1)))
132	5, 131	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ (0..^(𝑆 + 1)))
133	132	ad2antrr 734	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ (0..^(𝑆 + 1)))
134	1, 96	sselid 3929	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ ℕ)
135		fveq2 6856	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑆 → (𝐿‘𝑥) = (𝐿‘𝑆))
136	135	fveq1d 6858	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑆 → ((𝐿‘𝑥)‘𝑦) = ((𝐿‘𝑆)‘𝑦))
137	136	eleq1d 2841	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑆 → (((𝐿‘𝑥)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑆)‘𝑦) ∈ ℂ))
138		fveq2 6856	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝐿‘𝑆)‘𝑦) = ((𝐿‘𝑆)‘𝑏))
139	138	eleq1d 2841	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → (((𝐿‘𝑆)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑆)‘𝑏) ∈ ℂ))
140	137, 139	rspc2v 3587	. . . . . . . . . 10 ⊢ ((𝑆 ∈ (0..^(𝑆 + 1)) ∧ 𝑏 ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑆)‘𝑏) ∈ ℂ))
141	133, 134, 140	syl2anc 592	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑆)‘𝑏) ∈ ℂ))
142	105, 141	mpd 15	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘𝑏) ∈ ℂ)
143	130, 142	eqeltrd 2856	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆)) ∈ ℂ)
144	84, 85, 87, 88, 89, 118, 121, 143	fprodsplitsn 15995	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ ((0..^𝑆) ∪ {𝑆})((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) · ((𝐿‘𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))))
145	104	prodeq2dv 15928	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)))
146	145, 130	oveq12d 7403	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) · ((𝐿‘𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))
147	83, 144, 146	3eqtrd 2795	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))
148	147	sumeq2dv 15705	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))
149		simpl 485	. . . . . . . 8 ⊢ ((𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}))
150	149	fveq1d 6858	. . . . . . 7 ⊢ ((𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) = ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
151	150	fveq2d 6860	. . . . . 6 ⊢ ((𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) = ((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)))
152	151	prodeq2dv 15928	. . . . 5 ⊢ (𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)))
153	25, 26, 5, 28, 6	actfunsnf1o 34855	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})):((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))–1-1-onto→ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
154	6	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) = (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
155		simpr 487	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑣 = 𝑒) → 𝑣 = 𝑒)
156	155	uneq1d 4115	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑣 = 𝑒) → (𝑣 ∪ {⟨𝑆, 𝑏⟩}) = (𝑒 ∪ {⟨𝑆, 𝑏⟩}))
157		vex 3452	. . . . . . . 8 ⊢ 𝑒 ∈ V
158	157, 63	unex 7716	. . . . . . 7 ⊢ (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
159	158	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∈ V)
160	154, 156, 92, 159	fvmptd 6972	. . . . 5 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))‘𝑒) = (𝑒 ∪ {⟨𝑆, 𝑏⟩}))
161	152, 18, 153, 160, 79	fsumf1o 15726	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)))
162		simpl 485	. . . . . . . . . 10 ⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = 𝑒)
163	162	fveq1d 6858	. . . . . . . . 9 ⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑‘𝑎) = (𝑒‘𝑎))
164	163	fveq2d 6860	. . . . . . . 8 ⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) = ((𝐿‘𝑎)‘(𝑒‘𝑎)))
165	164	prodeq2dv 15928	. . . . . . 7 ⊢ (𝑑 = 𝑒 → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)))
166	165	oveq1d 7400	. . . . . 6 ⊢ (𝑑 = 𝑒 → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))
167	166	cbvsumv 15699	. . . . 5 ⊢ Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))
168	167	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))
169	148, 161, 168	3eqtr4d 2801	. . 3 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))
170	169	sumeq2dv 15705	. 2 ⊢ (𝜑 → Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))
171	8, 81, 170	3eqtrd 2795	1 ⊢ (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1554   ∈ wcel 2136  ∀wral 3070  ∃wrex 3080  {crab 3408  Vcvv 3448   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899  ∅c0 4280  {csn 4576  ⟨cop 4582  ∪ ciun 4943   class class class wbr 5094   ↦ cmpt 5175  ran crn 5641   Fn wfn 6505  ⟶wf 6506  ‘cfv 6510  (class class class)co 7385   ↑_m cmap 8796  Fincfn 8916  ℂcc 11061  0cc0 11063  1c1 11064   + caddc 11066   · cmul 11068   ≤ cle 11207   − cmin 11404  ℕcn 12200  ℕ₀cn0 12471  ℤcz 12558  ℤ_≥cuz 12829  ...cfz 13502  ..^cfzo 13649  Σcsu 15689  ∏cprod 15909  reprcrepr 34859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-rep 5221  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-inf2 9586  ax-cnex 11119  ax-resscn 11120  ax-1cn 11121  ax-icn 11122  ax-addcl 11123  ax-addrcl 11124  ax-mulcl 11125  ax-mulrcl 11126  ax-mulcom 11127  ax-addass 11128  ax-mulass 11129  ax-distr 11130  ax-i2m1 11131  ax-1ne0 11132  ax-1rid 11133  ax-rnegex 11134  ax-rrecex 11135  ax-cnre 11136  ax-pre-lttri 11137  ax-pre-lttrn 11138  ax-pre-ltadd 11139  ax-pre-mulgt0 11140  ax-pre-sup 11141

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-nel 3056  df-ral 3071  df-rex 3081  df-rmo 3361  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-int 4900  df-iun 4945  df-disj 5062  df-br 5095  df-opab 5157  df-mpt 5176  df-tr 5202  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-se 5594  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-isom 6519  df-riota 7342  df-ov 7388  df-oprab 7389  df-mpo 7390  df-om 7836  df-1st 7959  df-2nd 7960  df-frecs 8250  df-wrecs 8281  df-recs 8330  df-rdg 8369  df-1o 8425  df-er 8666  df-map 8798  df-pm 8799  df-en 8917  df-dom 8918  df-sdom 8919  df-fin 8920  df-sup 9378  df-oi 9448  df-card 9887  df-pnf 11208  df-mnf 11209  df-xr 11210  df-ltxr 11211  df-le 11212  df-sub 11406  df-neg 11407  df-div 11835  df-nn 12201  df-2 12270  df-3 12271  df-n0 12472  df-z 12559  df-uz 12830  df-rp 12984  df-fz 13503  df-fzo 13650  df-seq 14005  df-exp 14065  df-hash 14334  df-cj 15102  df-re 15103  df-im 15104  df-sqrt 15238  df-abs 15239  df-clim 15491  df-sum 15690  df-prod 15910  df-repr 34860

This theorem is referenced by:  breprexplemc  34883