| Step | Hyp | Ref
| Expression |
| 1 | | breprexp.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 2 | | breprexp.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
| 3 | | breprexp.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ ℂ) |
| 4 | | fvex 6919 |
. . . . . 6
⊢
((𝟭‘ℕ)‘𝐴) ∈ V |
| 5 | 4 | fconst 6794 |
. . . . 5
⊢
((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶{((𝟭‘ℕ)‘𝐴)} |
| 6 | | nnex 12272 |
. . . . . . . . 9
⊢ ℕ
∈ V |
| 7 | | breprexpnat.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
| 8 | | indf 32840 |
. . . . . . . . 9
⊢ ((ℕ
∈ V ∧ 𝐴 ⊆
ℕ) → ((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1}) |
| 9 | 6, 7, 8 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 →
((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1}) |
| 10 | | 0cn 11253 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
| 11 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 12 | | prssi 4821 |
. . . . . . . . 9
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → {0, 1} ⊆
ℂ) |
| 13 | 10, 11, 12 | mp2an 692 |
. . . . . . . 8
⊢ {0, 1}
⊆ ℂ |
| 14 | | fss 6752 |
. . . . . . . 8
⊢
((((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆
ℂ) → ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) |
| 15 | 9, 13, 14 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 →
((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) |
| 16 | | cnex 11236 |
. . . . . . . 8
⊢ ℂ
∈ V |
| 17 | 16, 6 | elmap 8911 |
. . . . . . 7
⊢
(((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑m
ℕ) ↔ ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) |
| 18 | 15, 17 | sylibr 234 |
. . . . . 6
⊢ (𝜑 →
((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑m
ℕ)) |
| 19 | 4 | snss 4785 |
. . . . . 6
⊢
(((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑m
ℕ) ↔ {((𝟭‘ℕ)‘𝐴)} ⊆ (ℂ ↑m
ℕ)) |
| 20 | 18, 19 | sylib 218 |
. . . . 5
⊢ (𝜑 →
{((𝟭‘ℕ)‘𝐴)} ⊆ (ℂ ↑m
ℕ)) |
| 21 | | fss 6752 |
. . . . 5
⊢
((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶{((𝟭‘ℕ)‘𝐴)} ∧
{((𝟭‘ℕ)‘𝐴)} ⊆ (ℂ ↑m ℕ))
→ ((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 22 | 5, 20, 21 | sylancr 587 |
. . . 4
⊢ (𝜑 → ((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 23 | 1, 2, 3, 22 | breprexp 34648 |
. . 3
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
| 24 | 4 | fvconst2 7224 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0..^𝑆) → (((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴)) |
| 25 | 24 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → (((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴)) |
| 26 | 25 | fveq1d 6908 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → ((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) = (((𝟭‘ℕ)‘𝐴)‘𝑏)) |
| 27 | 26 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → (((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ((((𝟭‘ℕ)‘𝐴)‘𝑏) · (𝑍↑𝑏))) |
| 28 | 27 | sumeq2dv 15738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (1...𝑁)((((𝟭‘ℕ)‘𝐴)‘𝑏) · (𝑍↑𝑏))) |
| 29 | 6 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → ℕ ∈ V) |
| 30 | | fzfi 14013 |
. . . . . . . 8
⊢
(1...𝑁) ∈
Fin |
| 31 | 30 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → (1...𝑁) ∈ Fin) |
| 32 | | fz1ssnn 13595 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ |
| 33 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → (1...𝑁) ⊆ ℕ) |
| 34 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ) |
| 35 | 3 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
| 36 | | nnssnn0 12529 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℕ0 |
| 37 | 32, 36 | sstri 3993 |
. . . . . . . . 9
⊢
(1...𝑁) ⊆
ℕ0 |
| 38 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
| 39 | 37, 38 | sselid 3981 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0) |
| 40 | 35, 39 | expcld 14186 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ) |
| 41 | 29, 31, 33, 34, 40 | indsumin 32847 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → Σ𝑏 ∈ (1...𝑁)((((𝟭‘ℕ)‘𝐴)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ ((1...𝑁) ∩ 𝐴)(𝑍↑𝑏)) |
| 42 | | incom 4209 |
. . . . . . . 8
⊢
((1...𝑁) ∩ 𝐴) = (𝐴 ∩ (1...𝑁)) |
| 43 | 42 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → ((1...𝑁) ∩ 𝐴) = (𝐴 ∩ (1...𝑁))) |
| 44 | 43 | sumeq1d 15736 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → Σ𝑏 ∈ ((1...𝑁) ∩ 𝐴)(𝑍↑𝑏) = Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)) |
| 45 | 28, 41, 44 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)) |
| 46 | 45 | prodeq2dv 15958 |
. . . 4
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)) |
| 47 | | fzofi 14015 |
. . . . . 6
⊢
(0..^𝑆) ∈
Fin |
| 48 | 47 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0..^𝑆) ∈ Fin) |
| 49 | | inss2 4238 |
. . . . . . . 8
⊢ (𝐴 ∩ (1...𝑁)) ⊆ (1...𝑁) |
| 50 | | ssfi 9213 |
. . . . . . . 8
⊢
(((1...𝑁) ∈ Fin
∧ (𝐴 ∩ (1...𝑁)) ⊆ (1...𝑁)) → (𝐴 ∩ (1...𝑁)) ∈ Fin) |
| 51 | 30, 49, 50 | mp2an 692 |
. . . . . . 7
⊢ (𝐴 ∩ (1...𝑁)) ∈ Fin |
| 52 | 51 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ (1...𝑁)) ∈ Fin) |
| 53 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴 ∩ (1...𝑁))) → 𝑍 ∈ ℂ) |
| 54 | 49, 37 | sstri 3993 |
. . . . . . . 8
⊢ (𝐴 ∩ (1...𝑁)) ⊆
ℕ0 |
| 55 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴 ∩ (1...𝑁))) → 𝑏 ∈ (𝐴 ∩ (1...𝑁))) |
| 56 | 54, 55 | sselid 3981 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴 ∩ (1...𝑁))) → 𝑏 ∈ ℕ0) |
| 57 | 53, 56 | expcld 14186 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴 ∩ (1...𝑁))) → (𝑍↑𝑏) ∈ ℂ) |
| 58 | 52, 57 | fsumcl 15769 |
. . . . 5
⊢ (𝜑 → Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏) ∈ ℂ) |
| 59 | | fprodconst 16014 |
. . . . 5
⊢
(((0..^𝑆) ∈ Fin
∧ Σ𝑏 ∈
(𝐴 ∩ (1...𝑁))(𝑍↑𝑏) ∈ ℂ) → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑(♯‘(0..^𝑆)))) |
| 60 | 48, 58, 59 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑(♯‘(0..^𝑆)))) |
| 61 | | hashfzo0 14469 |
. . . . . 6
⊢ (𝑆 ∈ ℕ0
→ (♯‘(0..^𝑆)) = 𝑆) |
| 62 | 2, 61 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘(0..^𝑆)) = 𝑆) |
| 63 | 62 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑(♯‘(0..^𝑆))) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑𝑆)) |
| 64 | 46, 60, 63 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑𝑆)) |
| 65 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ⊆ ℕ) |
| 66 | | fzssz 13566 |
. . . . . . . 8
⊢
(0...(𝑆 ·
𝑁)) ⊆
ℤ |
| 67 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ (0...(𝑆 · 𝑁))) |
| 68 | 66, 67 | sselid 3981 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℤ) |
| 69 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑆 ∈
ℕ0) |
| 70 | 30 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ∈ Fin) |
| 71 | 65, 68, 69, 70 | reprfi 34631 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((1...𝑁)(repr‘𝑆)𝑚) ∈ Fin) |
| 72 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑍 ∈ ℂ) |
| 73 | | fz0ssnn0 13662 |
. . . . . . . 8
⊢
(0...(𝑆 ·
𝑁)) ⊆
ℕ0 |
| 74 | 73, 67 | sselid 3981 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℕ0) |
| 75 | 72, 74 | expcld 14186 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑍↑𝑚) ∈ ℂ) |
| 76 | 47 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (0..^𝑆) ∈ Fin) |
| 77 | 9 | ad3antrrr 730 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) →
((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1}) |
| 78 | 32 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (1...𝑁) ⊆ ℕ) |
| 79 | 68 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑚 ∈ ℤ) |
| 80 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑆 ∈
ℕ0) |
| 81 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) |
| 82 | 78, 79, 80, 81 | reprf 34627 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑐:(0..^𝑆)⟶(1...𝑁)) |
| 83 | 82 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ (1...𝑁)) |
| 84 | 32, 83 | sselid 3981 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
| 85 | 77, 84 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) →
(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) ∈ {0, 1}) |
| 86 | 13, 85 | sselid 3981 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) →
(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) ∈ ℂ) |
| 87 | 76, 86 | fprodcl 15988 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) ∈ ℂ) |
| 88 | 71, 75, 87 | fsummulc1 15821 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
| 89 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝐴 ⊆ ℕ) |
| 90 | 89, 68, 69, 70, 65 | hashreprin 34635 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
| 91 | 90 | oveq1d 7446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚)) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
| 92 | 24 | fveq1d 6908 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0..^𝑆) → ((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = (((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
| 93 | 92 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑎 ∈ (0..^𝑆)) → ((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = (((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
| 94 | 93 | prodeq2dv 15958 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
| 95 | 94 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
| 96 | 95 | oveq1d 7446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
| 97 | 96 | sumeq2dv 15738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
| 98 | 88, 91, 97 | 3eqtr4rd 2788 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = ((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚))) |
| 99 | 98 | sumeq2dv 15738 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚))) |
| 100 | 23, 64, 99 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑𝑆) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚))) |
| 101 | | breprexpnat.p |
. . 3
⊢ 𝑃 = Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏) |
| 102 | 101 | oveq1i 7441 |
. 2
⊢ (𝑃↑𝑆) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑𝑆) |
| 103 | | breprexpnat.r |
. . . . 5
⊢ 𝑅 = (♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) |
| 104 | 103 | oveq1i 7441 |
. . . 4
⊢ (𝑅 · (𝑍↑𝑚)) = ((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚)) |
| 105 | 104 | a1i 11 |
. . 3
⊢ (𝑚 ∈ (0...(𝑆 · 𝑁)) → (𝑅 · (𝑍↑𝑚)) = ((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚))) |
| 106 | 105 | sumeq2i 15734 |
. 2
⊢
Σ𝑚 ∈
(0...(𝑆 · 𝑁))(𝑅 · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚)) |
| 107 | 100, 102,
106 | 3eqtr4g 2802 |
1
⊢ (𝜑 → (𝑃↑𝑆) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))(𝑅 · (𝑍↑𝑚))) |