Step | Hyp | Ref
| Expression |
1 | | fz1ssnn 12372 |
. . . . 5
⊢
(1...𝑁) ⊆
ℕ |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
3 | | breprexplema.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
4 | 3 | nn0zd 11480 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
5 | | breprexp.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
6 | | eqid 2622 |
. . . 4
⊢ (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) = (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) |
7 | 2, 4, 5, 6 | reprsuc 30693 |
. . 3
⊢ (𝜑 → ((1...𝑁)(repr‘(𝑆 + 1))𝑀) = ∪
𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) |
8 | 7 | sumeq1d 14431 |
. 2
⊢ (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∪
𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎))) |
9 | | fzfid 12772 |
. . 3
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
10 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ) |
11 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑀 ∈ ℤ) |
12 | | fzssz 12343 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℤ |
13 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
14 | 12, 13 | sseldi 3601 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ) |
15 | 11, 14 | zsubcld 11487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑀 − 𝑏) ∈ ℤ) |
16 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈
ℕ0) |
17 | 9 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin) |
18 | 10, 15, 16, 17 | reprfi 30694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ∈ Fin) |
19 | | mptfi 8265 |
. . . . 5
⊢
(((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ∈ Fin → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin) |
21 | | rnfi 8249 |
. . . 4
⊢ ((𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin → ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin) |
23 | 10, 15, 16 | reprval 30688 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) = {𝑐 ∈ ((1...𝑁) ↑𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏)}) |
24 | | ssrab2 3687 |
. . . . 5
⊢ {𝑐 ∈ ((1...𝑁) ↑𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏)} ⊆ ((1...𝑁) ↑𝑚 (0..^𝑆)) |
25 | 23, 24 | syl6eqss 3655 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ⊆ ((1...𝑁) ↑𝑚 (0..^𝑆))) |
26 | 9 | elexd 3214 |
. . . 4
⊢ (𝜑 → (1...𝑁) ∈ V) |
27 | | fzonel 12483 |
. . . . 5
⊢ ¬
𝑆 ∈ (0..^𝑆) |
28 | 27 | a1i 11 |
. . . 4
⊢ (𝜑 → ¬ 𝑆 ∈ (0..^𝑆)) |
29 | 25, 26, 5, 28, 6 | actfunsnrndisj 30683 |
. . 3
⊢ (𝜑 → Disj 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) |
30 | | fzofi 12773 |
. . . . . 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 2966 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(𝑆 + 1))) → ∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) |
34 | 33 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) |
35 | 34 | ad3antrrr 766 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) |
36 | | simpr 477 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑎 ∈ (0..^(𝑆 + 1))) |
37 | | nfv 1843 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑣(𝜑 ∧ 𝑏 ∈ (1...𝑁)) |
38 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑣𝑑 |
39 | | nfmpt1 4747 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑣(𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) |
40 | 39 | nfrn 5368 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑣ran
(𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) |
41 | 38, 40 | nfel 2777 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑣 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) |
42 | 37, 41 | nfan 1828 |
. . . . . . . . . . 11
⊢
Ⅎ𝑣((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) |
43 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (1...𝑁) ⊆ ℕ) |
44 | 15 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (𝑀 − 𝑏) ∈ ℤ) |
45 | 16 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑆 ∈
ℕ0) |
46 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) |
47 | 43, 44, 45, 46 | reprf 30690 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑣:(0..^𝑆)⟶(1...𝑁)) |
48 | 13 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑏 ∈ (1...𝑁)) |
49 | 45, 48 | fsnd 6179 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → {〈𝑆, 𝑏〉}:{𝑆}⟶(1...𝑁)) |
50 | | fzodisjsn 12505 |
. . . . . . . . . . . . . 14
⊢
((0..^𝑆) ∩
{𝑆}) =
∅ |
51 | 50 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → ((0..^𝑆) ∩ {𝑆}) = ∅) |
52 | | fun2 6067 |
. . . . . . . . . . . . 13
⊢ (((𝑣:(0..^𝑆)⟶(1...𝑁) ∧ {〈𝑆, 𝑏〉}:{𝑆}⟶(1...𝑁)) ∧ ((0..^𝑆) ∩ {𝑆}) = ∅) → (𝑣 ∪ {〈𝑆, 𝑏〉}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁)) |
53 | 47, 49, 51, 52 | syl21anc 1325 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (𝑣 ∪ {〈𝑆, 𝑏〉}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁)) |
54 | | simpr 477 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) |
55 | | nn0uz 11722 |
. . . . . . . . . . . . . . . 16
⊢
ℕ0 = (ℤ≥‘0) |
56 | 5, 55 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈
(ℤ≥‘0)) |
57 | | fzosplitsn 12576 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈
(ℤ≥‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
59 | 58 | ad4antr 768 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
60 | 54, 59 | feq12d 6033 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (𝑑:(0..^(𝑆 + 1))⟶(1...𝑁) ↔ (𝑣 ∪ {〈𝑆, 𝑏〉}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁))) |
61 | 53, 60 | mpbird 247 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁)) |
62 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) → 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) |
63 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑣 ∈ V |
64 | | snex 4908 |
. . . . . . . . . . . . . 14
⊢
{〈𝑆, 𝑏〉} ∈
V |
65 | 63, 64 | unex 6956 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∪ {〈𝑆, 𝑏〉}) ∈ V |
66 | 6, 65 | elrnmpti 5376 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ↔ ∃𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) |
67 | 62, 66 | sylib 208 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) → ∃𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) |
68 | 42, 61, 67 | r19.29af 3076 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁)) |
69 | 68 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁)) |
70 | 69, 36 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) ∈ (1...𝑁)) |
71 | 1, 70 | sseldi 3601 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) ∈ ℕ) |
72 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝐿‘𝑥) = (𝐿‘𝑎)) |
73 | 72 | fveq1d 6193 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝐿‘𝑥)‘𝑦) = ((𝐿‘𝑎)‘𝑦)) |
74 | 73 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → (((𝐿‘𝑥)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘𝑦) ∈ ℂ)) |
75 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑦 = (𝑑‘𝑎) → ((𝐿‘𝑎)‘𝑦) = ((𝐿‘𝑎)‘(𝑑‘𝑎))) |
76 | 75 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑦 = (𝑑‘𝑎) → (((𝐿‘𝑎)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)) |
77 | 74, 76 | rspc2v 3322 |
. . . . . . 7
⊢ ((𝑎 ∈ (0..^(𝑆 + 1)) ∧ (𝑑‘𝑎) ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)) |
78 | 36, 71, 77 | syl2anc 693 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)) |
79 | 35, 78 | mpd 15 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
80 | 31, 79 | fprodcl 14682 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
81 | 80 | anasss 679 |
. . 3
⊢ ((𝜑 ∧ (𝑏 ∈ (1...𝑁) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
82 | 9, 22, 29, 81 | fsumiun 14553 |
. 2
⊢ (𝜑 → Σ𝑑 ∈ ∪
𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎))) |
83 | 58 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) |
84 | 83 | prodeq1d 14651 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = ∏𝑎 ∈ ((0..^𝑆) ∪ {𝑆})((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎))) |
85 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑎((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) |
86 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑎((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)) |
87 | | fzofi 12773 |
. . . . . . . 8
⊢
(0..^𝑆) ∈
Fin |
88 | 87 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^𝑆) ∈ Fin) |
89 | 16 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈
ℕ0) |
90 | 27 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ¬ 𝑆 ∈ (0..^𝑆)) |
91 | 1 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (1...𝑁) ⊆ ℕ) |
92 | 15 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑀 − 𝑏) ∈ ℤ) |
93 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) |
94 | 91, 92, 89, 93 | reprf 30690 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒:(0..^𝑆)⟶(1...𝑁)) |
95 | | ffn 6045 |
. . . . . . . . . . . 12
⊢ (𝑒:(0..^𝑆)⟶(1...𝑁) → 𝑒 Fn (0..^𝑆)) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒 Fn (0..^𝑆)) |
97 | 96 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 Fn (0..^𝑆)) |
98 | 13 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ (1...𝑁)) |
99 | | fnsng 5938 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℕ0
∧ 𝑏 ∈ (1...𝑁)) → {〈𝑆, 𝑏〉} Fn {𝑆}) |
100 | 89, 98, 99 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → {〈𝑆, 𝑏〉} Fn {𝑆}) |
101 | 100 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → {〈𝑆, 𝑏〉} Fn {𝑆}) |
102 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅) |
103 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
104 | | fvun1 6269 |
. . . . . . . . . 10
⊢ ((𝑒 Fn (0..^𝑆) ∧ {〈𝑆, 𝑏〉} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎) = (𝑒‘𝑎)) |
105 | 97, 101, 102, 103, 104 | syl112anc 1330 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎) = (𝑒‘𝑎)) |
106 | 105 | fveq2d 6195 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = ((𝐿‘𝑎)‘(𝑒‘𝑎))) |
107 | 34 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) |
108 | 107 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) |
109 | | fzossfzop1 12545 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ ℕ0
→ (0..^𝑆) ⊆
(0..^(𝑆 +
1))) |
110 | 5, 109 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0..^𝑆) ⊆ (0..^(𝑆 + 1))) |
111 | 110 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1))) |
112 | 111 | sselda 3603 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1))) |
113 | 94 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ (1...𝑁)) |
114 | 1, 113 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℕ) |
115 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑒‘𝑎) → ((𝐿‘𝑎)‘𝑦) = ((𝐿‘𝑎)‘(𝑒‘𝑎))) |
116 | 115 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑒‘𝑎) → (((𝐿‘𝑎)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ)) |
117 | 74, 116 | rspc2v 3322 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (0..^(𝑆 + 1)) ∧ (𝑒‘𝑎) ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ)) |
118 | 112, 114,
117 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ)) |
119 | 108, 118 | mpd 15 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ) |
120 | 106, 119 | eqeltrd 2701 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) ∈ ℂ) |
121 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑎 = 𝑆 → (𝐿‘𝑎) = (𝐿‘𝑆)) |
122 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑎 = 𝑆 → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎) = ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)) |
123 | 121, 122 | fveq12d 6197 |
. . . . . . 7
⊢ (𝑎 = 𝑆 → ((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆))) |
124 | 50 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅) |
125 | | snidg 4206 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈ {𝑆}) |
126 | 89, 125 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ {𝑆}) |
127 | | fvun2 6270 |
. . . . . . . . . . 11
⊢ ((𝑒 Fn (0..^𝑆) ∧ {〈𝑆, 𝑏〉} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆) = ({〈𝑆, 𝑏〉}‘𝑆)) |
128 | 96, 100, 124, 126, 127 | syl112anc 1330 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆) = ({〈𝑆, 𝑏〉}‘𝑆)) |
129 | | fvsng 6447 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ ℕ0
∧ 𝑏 ∈ (1...𝑁)) → ({〈𝑆, 𝑏〉}‘𝑆) = 𝑏) |
130 | 89, 98, 129 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ({〈𝑆, 𝑏〉}‘𝑆) = 𝑏) |
131 | 128, 130 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆) = 𝑏) |
132 | 131 | fveq2d 6195 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)) = ((𝐿‘𝑆)‘𝑏)) |
133 | | fzonn0p1 12544 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈ (0..^(𝑆 + 1))) |
134 | 5, 133 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ (0..^(𝑆 + 1))) |
135 | 134 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ (0..^(𝑆 + 1))) |
136 | 1, 98 | sseldi 3601 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ ℕ) |
137 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑆 → (𝐿‘𝑥) = (𝐿‘𝑆)) |
138 | 137 | fveq1d 6193 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑆 → ((𝐿‘𝑥)‘𝑦) = ((𝐿‘𝑆)‘𝑦)) |
139 | 138 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑆 → (((𝐿‘𝑥)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑆)‘𝑦) ∈ ℂ)) |
140 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → ((𝐿‘𝑆)‘𝑦) = ((𝐿‘𝑆)‘𝑏)) |
141 | 140 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → (((𝐿‘𝑆)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑆)‘𝑏) ∈ ℂ)) |
142 | 139, 141 | rspc2v 3322 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (0..^(𝑆 + 1)) ∧ 𝑏 ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑆)‘𝑏) ∈ ℂ)) |
143 | 135, 136,
142 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑆)‘𝑏) ∈ ℂ)) |
144 | 107, 143 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘𝑏) ∈ ℂ) |
145 | 132, 144 | eqeltrd 2701 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)) ∈ ℂ) |
146 | 85, 86, 88, 89, 90, 120, 123, 145 | fprodsplitsn 14720 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ ((0..^𝑆) ∪ {𝑆})((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) · ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)))) |
147 | 106 | prodeq2dv 14653 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎))) |
148 | 147, 132 | oveq12d 6668 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) · ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |
149 | 84, 146, 148 | 3eqtrd 2660 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |
150 | 149 | sumeq2dv 14433 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |
151 | | simpl 473 |
. . . . . . . 8
⊢ ((𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉})) |
152 | 151 | fveq1d 6193 |
. . . . . . 7
⊢ ((𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) = ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) |
153 | 152 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) = ((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎))) |
154 | 153 | prodeq2dv 14653 |
. . . . 5
⊢ (𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉}) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎))) |
155 | 25, 26, 5, 28, 6 | actfunsnf1o 30682 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})):((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))–1-1-onto→ran
(𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) |
156 | 6 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) = (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) |
157 | | simpr 477 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑣 = 𝑒) → 𝑣 = 𝑒) |
158 | 157 | uneq1d 3766 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑣 = 𝑒) → (𝑣 ∪ {〈𝑆, 𝑏〉}) = (𝑒 ∪ {〈𝑆, 𝑏〉})) |
159 | | vex 3203 |
. . . . . . . 8
⊢ 𝑒 ∈ V |
160 | 159, 64 | unex 6956 |
. . . . . . 7
⊢ (𝑒 ∪ {〈𝑆, 𝑏〉}) ∈ V |
161 | 160 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑒 ∪ {〈𝑆, 𝑏〉}) ∈ V) |
162 | 156, 158,
93, 161 | fvmptd 6288 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))‘𝑒) = (𝑒 ∪ {〈𝑆, 𝑏〉})) |
163 | 154, 18, 155, 162, 80 | fsumf1o 14454 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎))) |
164 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = 𝑒) |
165 | 164 | fveq1d 6193 |
. . . . . . . . 9
⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑‘𝑎) = (𝑒‘𝑎)) |
166 | 165 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) = ((𝐿‘𝑎)‘(𝑒‘𝑎))) |
167 | 166 | prodeq2dv 14653 |
. . . . . . 7
⊢ (𝑑 = 𝑒 → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎))) |
168 | 167 | oveq1d 6665 |
. . . . . 6
⊢ (𝑑 = 𝑒 → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |
169 | 168 | cbvsumv 14426 |
. . . . 5
⊢
Σ𝑑 ∈
((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) |
170 | 169 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |
171 | 150, 163,
170 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |
172 | 171 | sumeq2dv 14433 |
. 2
⊢ (𝜑 → Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |
173 | 8, 82, 172 | 3eqtrd 2660 |
1
⊢ (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |