| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fz1ssnn 13596 | . . . . 5
⊢
(1...𝑁) ⊆
ℕ | 
| 2 | 1 | a1i 11 | . . . 4
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) | 
| 3 |  | breprexplema.m | . . . . 5
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 4 | 3 | nn0zd 12641 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 5 |  | breprexp.s | . . . 4
⊢ (𝜑 → 𝑆 ∈
ℕ0) | 
| 6 |  | eqid 2736 | . . . 4
⊢ (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) = (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) | 
| 7 | 2, 4, 5, 6 | reprsuc 34631 | . . 3
⊢ (𝜑 → ((1...𝑁)(repr‘(𝑆 + 1))𝑀) = ∪
𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) | 
| 8 | 7 | sumeq1d 15737 | . 2
⊢ (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∪
𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎))) | 
| 9 |  | fzfid 14015 | . . 3
⊢ (𝜑 → (1...𝑁) ∈ Fin) | 
| 10 | 1 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ) | 
| 11 | 4 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑀 ∈ ℤ) | 
| 12 |  | fzssz 13567 | . . . . . . . 8
⊢
(1...𝑁) ⊆
ℤ | 
| 13 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) | 
| 14 | 12, 13 | sselid 3980 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ) | 
| 15 | 11, 14 | zsubcld 12729 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑀 − 𝑏) ∈ ℤ) | 
| 16 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈
ℕ0) | 
| 17 | 9 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin) | 
| 18 | 10, 15, 16, 17 | reprfi 34632 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ∈ Fin) | 
| 19 |  | mptfi 9392 | . . . . 5
⊢
(((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ∈ Fin → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin) | 
| 20 | 18, 19 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin) | 
| 21 |  | rnfi 9381 | . . . 4
⊢ ((𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin → ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin) | 
| 22 | 20, 21 | syl 17 | . . 3
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ∈ Fin) | 
| 23 | 10, 15, 16 | reprval 34626 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) = {𝑐 ∈ ((1...𝑁) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏)}) | 
| 24 |  | ssrab2 4079 | . . . . 5
⊢ {𝑐 ∈ ((1...𝑁) ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = (𝑀 − 𝑏)} ⊆ ((1...𝑁) ↑m (0..^𝑆)) | 
| 25 | 23, 24 | eqsstrdi 4027 | . . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ⊆ ((1...𝑁) ↑m (0..^𝑆))) | 
| 26 | 9 | elexd 3503 | . . . 4
⊢ (𝜑 → (1...𝑁) ∈ V) | 
| 27 |  | fzonel 13714 | . . . . 5
⊢  ¬
𝑆 ∈ (0..^𝑆) | 
| 28 | 27 | a1i 11 | . . . 4
⊢ (𝜑 → ¬ 𝑆 ∈ (0..^𝑆)) | 
| 29 | 25, 26, 5, 28, 6 | actfunsnrndisj 34621 | . . 3
⊢ (𝜑 → Disj 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) | 
| 30 |  | fzofi 14016 | . . . . . 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 3145 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(𝑆 + 1))) → ∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) | 
| 34 | 33 | ralrimiva 3145 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) | 
| 35 | 34 | ad3antrrr 730 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) | 
| 36 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑎 ∈ (0..^(𝑆 + 1))) | 
| 37 |  | nfv 1913 | . . . . . . . . . . . 12
⊢
Ⅎ𝑣(𝜑 ∧ 𝑏 ∈ (1...𝑁)) | 
| 38 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣𝑑 | 
| 39 |  | nfmpt1 5249 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑣(𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) | 
| 40 | 39 | nfrn 5962 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣ran
(𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) | 
| 41 | 38, 40 | nfel 2919 | . . . . . . . . . . . 12
⊢
Ⅎ𝑣 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) | 
| 42 | 37, 41 | nfan 1898 | . . . . . . . . . . 11
⊢
Ⅎ𝑣((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) | 
| 43 | 1 | a1i 11 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (1...𝑁) ⊆ ℕ) | 
| 44 | 15 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (𝑀 − 𝑏) ∈ ℤ) | 
| 45 | 16 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑆 ∈
ℕ0) | 
| 46 |  | simplr 768 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) | 
| 47 | 43, 44, 45, 46 | reprf 34628 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑣:(0..^𝑆)⟶(1...𝑁)) | 
| 48 | 13 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑏 ∈ (1...𝑁)) | 
| 49 | 45, 48 | fsnd 6890 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → {〈𝑆, 𝑏〉}:{𝑆}⟶(1...𝑁)) | 
| 50 |  | fzodisjsn 13738 | . . . . . . . . . . . . . 14
⊢
((0..^𝑆) ∩
{𝑆}) =
∅ | 
| 51 | 50 | a1i 11 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → ((0..^𝑆) ∩ {𝑆}) = ∅) | 
| 52 |  | fun2 6770 | . . . . . . . . . . . . 13
⊢ (((𝑣:(0..^𝑆)⟶(1...𝑁) ∧ {〈𝑆, 𝑏〉}:{𝑆}⟶(1...𝑁)) ∧ ((0..^𝑆) ∩ {𝑆}) = ∅) → (𝑣 ∪ {〈𝑆, 𝑏〉}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁)) | 
| 53 | 47, 49, 51, 52 | syl21anc 837 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (𝑣 ∪ {〈𝑆, 𝑏〉}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁)) | 
| 54 |  | simpr 484 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) | 
| 55 |  | nn0uz 12921 | . . . . . . . . . . . . . . . 16
⊢
ℕ0 = (ℤ≥‘0) | 
| 56 | 5, 55 | eleqtrdi 2850 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈
(ℤ≥‘0)) | 
| 57 |  | fzosplitsn 13815 | . . . . . . . . . . . . . . 15
⊢ (𝑆 ∈
(ℤ≥‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) | 
| 58 | 56, 57 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) | 
| 59 | 58 | ad4antr 732 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) | 
| 60 | 54, 59 | feq12d 6723 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → (𝑑:(0..^(𝑆 + 1))⟶(1...𝑁) ↔ (𝑣 ∪ {〈𝑆, 𝑏〉}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁))) | 
| 61 | 53, 60 | mpbird 257 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁)) | 
| 62 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) → 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) | 
| 63 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑣 ∈ V | 
| 64 |  | snex 5435 | . . . . . . . . . . . . . 14
⊢
{〈𝑆, 𝑏〉} ∈
V | 
| 65 | 63, 64 | unex 7765 | . . . . . . . . . . . . 13
⊢ (𝑣 ∪ {〈𝑆, 𝑏〉}) ∈ V | 
| 66 | 6, 65 | elrnmpti 5972 | . . . . . . . . . . . 12
⊢ (𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) ↔ ∃𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) | 
| 67 | 62, 66 | sylib 218 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) → ∃𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))𝑑 = (𝑣 ∪ {〈𝑆, 𝑏〉})) | 
| 68 | 42, 61, 67 | r19.29af 3267 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁)) | 
| 69 | 68 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁)) | 
| 70 | 69, 36 | ffvelcdmd 7104 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) ∈ (1...𝑁)) | 
| 71 | 1, 70 | sselid 3980 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) ∈ ℕ) | 
| 72 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝐿‘𝑥) = (𝐿‘𝑎)) | 
| 73 | 72 | fveq1d 6907 | . . . . . . . . 9
⊢ (𝑥 = 𝑎 → ((𝐿‘𝑥)‘𝑦) = ((𝐿‘𝑎)‘𝑦)) | 
| 74 | 73 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑥 = 𝑎 → (((𝐿‘𝑥)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘𝑦) ∈ ℂ)) | 
| 75 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑦 = (𝑑‘𝑎) → ((𝐿‘𝑎)‘𝑦) = ((𝐿‘𝑎)‘(𝑑‘𝑎))) | 
| 76 | 75 | eleq1d 2825 | . . . . . . . 8
⊢ (𝑦 = (𝑑‘𝑎) → (((𝐿‘𝑎)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)) | 
| 77 | 74, 76 | rspc2v 3632 | . . . . . . 7
⊢ ((𝑎 ∈ (0..^(𝑆 + 1)) ∧ (𝑑‘𝑎) ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)) | 
| 78 | 36, 71, 77 | syl2anc 584 | . . . . . 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 15989 | . . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) | 
| 81 | 80 | anasss 466 | . . 3
⊢ ((𝜑 ∧ (𝑏 ∈ (1...𝑁) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) | 
| 82 | 9, 22, 29, 81 | fsumiun 15858 | . 2
⊢ (𝜑 → Σ𝑑 ∈ ∪
𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎))) | 
| 83 | 58 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆})) | 
| 84 | 83 | prodeq1d 15957 | . . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = ∏𝑎 ∈ ((0..^𝑆) ∪ {𝑆})((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎))) | 
| 85 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑎((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) | 
| 86 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑎((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)) | 
| 87 |  | fzofi 14016 | . . . . . . . 8
⊢
(0..^𝑆) ∈
Fin | 
| 88 | 87 | a1i 11 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^𝑆) ∈ Fin) | 
| 89 | 16 | adantr 480 | . . . . . . 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 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑀 − 𝑏) ∈ ℤ) | 
| 93 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) | 
| 94 | 91, 92, 89, 93 | reprf 34628 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒:(0..^𝑆)⟶(1...𝑁)) | 
| 95 | 94 | ffnd 6736 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑒 Fn (0..^𝑆)) | 
| 96 | 95 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 Fn (0..^𝑆)) | 
| 97 | 13 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ (1...𝑁)) | 
| 98 |  | fnsng 6617 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ ℕ0
∧ 𝑏 ∈ (1...𝑁)) → {〈𝑆, 𝑏〉} Fn {𝑆}) | 
| 99 | 89, 97, 98 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → {〈𝑆, 𝑏〉} Fn {𝑆}) | 
| 100 | 99 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → {〈𝑆, 𝑏〉} Fn {𝑆}) | 
| 101 | 50 | a1i 11 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅) | 
| 102 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) | 
| 103 |  | fvun1 6999 | . . . . . . . . . 10
⊢ ((𝑒 Fn (0..^𝑆) ∧ {〈𝑆, 𝑏〉} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎) = (𝑒‘𝑎)) | 
| 104 | 96, 100, 101, 102, 103 | syl112anc 1375 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎) = (𝑒‘𝑎)) | 
| 105 | 104 | fveq2d 6909 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = ((𝐿‘𝑎)‘(𝑒‘𝑎))) | 
| 106 | 34 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) | 
| 107 | 106 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ) | 
| 108 |  | fzossfzop1 13783 | . . . . . . . . . . . . 13
⊢ (𝑆 ∈ ℕ0
→ (0..^𝑆) ⊆
(0..^(𝑆 +
1))) | 
| 109 | 5, 108 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (0..^𝑆) ⊆ (0..^(𝑆 + 1))) | 
| 110 | 109 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1))) | 
| 111 | 110 | sselda 3982 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1))) | 
| 112 | 94 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ (1...𝑁)) | 
| 113 | 1, 112 | sselid 3980 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒‘𝑎) ∈ ℕ) | 
| 114 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑦 = (𝑒‘𝑎) → ((𝐿‘𝑎)‘𝑦) = ((𝐿‘𝑎)‘(𝑒‘𝑎))) | 
| 115 | 114 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑦 = (𝑒‘𝑎) → (((𝐿‘𝑎)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ)) | 
| 116 | 74, 115 | rspc2v 3632 | . . . . . . . . . 10
⊢ ((𝑎 ∈ (0..^(𝑆 + 1)) ∧ (𝑒‘𝑎) ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ)) | 
| 117 | 111, 113,
116 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ)) | 
| 118 | 107, 117 | mpd 15 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑒‘𝑎)) ∈ ℂ) | 
| 119 | 105, 118 | eqeltrd 2840 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) ∈ ℂ) | 
| 120 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑎 = 𝑆 → (𝐿‘𝑎) = (𝐿‘𝑆)) | 
| 121 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑎 = 𝑆 → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎) = ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)) | 
| 122 | 120, 121 | fveq12d 6912 | . . . . . . 7
⊢ (𝑎 = 𝑆 → ((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆))) | 
| 123 | 50 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅) | 
| 124 |  | snidg 4659 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈ {𝑆}) | 
| 125 | 89, 124 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ {𝑆}) | 
| 126 |  | fvun2 7000 | . . . . . . . . . . 11
⊢ ((𝑒 Fn (0..^𝑆) ∧ {〈𝑆, 𝑏〉} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆) = ({〈𝑆, 𝑏〉}‘𝑆)) | 
| 127 | 95, 99, 123, 125, 126 | syl112anc 1375 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆) = ({〈𝑆, 𝑏〉}‘𝑆)) | 
| 128 |  | fvsng 7201 | . . . . . . . . . . 11
⊢ ((𝑆 ∈ ℕ0
∧ 𝑏 ∈ (1...𝑁)) → ({〈𝑆, 𝑏〉}‘𝑆) = 𝑏) | 
| 129 | 89, 97, 128 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ({〈𝑆, 𝑏〉}‘𝑆) = 𝑏) | 
| 130 | 127, 129 | eqtrd 2776 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆) = 𝑏) | 
| 131 | 130 | fveq2d 6909 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)) = ((𝐿‘𝑆)‘𝑏)) | 
| 132 |  | fzonn0p1 13782 | . . . . . . . . . . . 12
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈ (0..^(𝑆 + 1))) | 
| 133 | 5, 132 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ (0..^(𝑆 + 1))) | 
| 134 | 133 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑆 ∈ (0..^(𝑆 + 1))) | 
| 135 | 1, 97 | sselid 3980 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → 𝑏 ∈ ℕ) | 
| 136 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑆 → (𝐿‘𝑥) = (𝐿‘𝑆)) | 
| 137 | 136 | fveq1d 6907 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑆 → ((𝐿‘𝑥)‘𝑦) = ((𝐿‘𝑆)‘𝑦)) | 
| 138 | 137 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑆 → (((𝐿‘𝑥)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑆)‘𝑦) ∈ ℂ)) | 
| 139 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → ((𝐿‘𝑆)‘𝑦) = ((𝐿‘𝑆)‘𝑏)) | 
| 140 | 139 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → (((𝐿‘𝑆)‘𝑦) ∈ ℂ ↔ ((𝐿‘𝑆)‘𝑏) ∈ ℂ)) | 
| 141 | 138, 140 | rspc2v 3632 | . . . . . . . . . 10
⊢ ((𝑆 ∈ (0..^(𝑆 + 1)) ∧ 𝑏 ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑆)‘𝑏) ∈ ℂ)) | 
| 142 | 134, 135,
141 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿‘𝑥)‘𝑦) ∈ ℂ → ((𝐿‘𝑆)‘𝑏) ∈ ℂ)) | 
| 143 | 106, 142 | mpd 15 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘𝑏) ∈ ℂ) | 
| 144 | 131, 143 | eqeltrd 2840 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)) ∈ ℂ) | 
| 145 | 85, 86, 88, 89, 90, 119, 122, 144 | fprodsplitsn 16026 | . . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ ((0..^𝑆) ∪ {𝑆})((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) · ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆)))) | 
| 146 | 105 | prodeq2dv 15959 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎))) | 
| 147 | 146, 131 | oveq12d 7450 | . . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) · ((𝐿‘𝑆)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑆))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) | 
| 148 | 84, 145, 147 | 3eqtrd 2780 | . . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) | 
| 149 | 148 | sumeq2dv 15739 | . . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) | 
| 150 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉})) | 
| 151 | 150 | fveq1d 6907 | . . . . . . 7
⊢ ((𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑‘𝑎) = ((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎)) | 
| 152 | 151 | fveq2d 6909 | . . . . . 6
⊢ ((𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) = ((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎))) | 
| 153 | 152 | prodeq2dv 15959 | . . . . 5
⊢ (𝑑 = (𝑒 ∪ {〈𝑆, 𝑏〉}) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎))) | 
| 154 | 25, 26, 5, 28, 6 | actfunsnf1o 34620 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})):((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))–1-1-onto→ran
(𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) | 
| 155 | 6 | a1i 11 | . . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉})) = (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))) | 
| 156 |  | simpr 484 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑣 = 𝑒) → 𝑣 = 𝑒) | 
| 157 | 156 | uneq1d 4166 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) ∧ 𝑣 = 𝑒) → (𝑣 ∪ {〈𝑆, 𝑏〉}) = (𝑒 ∪ {〈𝑆, 𝑏〉})) | 
| 158 |  | vex 3483 | . . . . . . . 8
⊢ 𝑒 ∈ V | 
| 159 | 158, 64 | unex 7765 | . . . . . . 7
⊢ (𝑒 ∪ {〈𝑆, 𝑏〉}) ∈ V | 
| 160 | 159 | a1i 11 | . . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → (𝑒 ∪ {〈𝑆, 𝑏〉}) ∈ V) | 
| 161 | 155, 157,
93, 160 | fvmptd 7022 | . . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))) → ((𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))‘𝑒) = (𝑒 ∪ {〈𝑆, 𝑏〉})) | 
| 162 | 153, 18, 154, 161, 80 | fsumf1o 15760 | . . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘((𝑒 ∪ {〈𝑆, 𝑏〉})‘𝑎))) | 
| 163 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = 𝑒) | 
| 164 | 163 | fveq1d 6907 | . . . . . . . . 9
⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑‘𝑎) = (𝑒‘𝑎)) | 
| 165 | 164 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝑑 = 𝑒 ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) = ((𝐿‘𝑎)‘(𝑒‘𝑎))) | 
| 166 | 165 | prodeq2dv 15959 | . . . . . . 7
⊢ (𝑑 = 𝑒 → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎))) | 
| 167 | 166 | oveq1d 7447 | . . . . . 6
⊢ (𝑑 = 𝑒 → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) | 
| 168 | 167 | cbvsumv 15733 | . . . . 5
⊢
Σ𝑑 ∈
((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) | 
| 169 | 168 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑒‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) | 
| 170 | 149, 162,
169 | 3eqtr4d 2786 | . . 3
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) | 
| 171 | 170 | sumeq2dv 15739 | . 2
⊢ (𝜑 → Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏)) ↦ (𝑣 ∪ {〈𝑆, 𝑏〉}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) | 
| 172 | 8, 82, 171 | 3eqtrd 2780 | 1
⊢ (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀 − 𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑆)‘𝑏))) |