Step |
Hyp |
Ref |
Expression |
1 |
|
neldifsnd |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ¬ 𝑋 ∈ ( 𝐴 ∖ { 𝑋 } ) ) |
2 |
|
disjsn |
⊢ ( ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ ( 𝐴 ∖ { 𝑋 } ) ) |
3 |
1 2
|
sylibr |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅ ) |
4 |
|
uncom |
⊢ ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = ( { 𝑋 } ∪ ( 𝐴 ∖ { 𝑋 } ) ) |
5 |
|
simp2 |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → 𝑋 ∈ 𝐴 ) |
6 |
5
|
snssd |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → { 𝑋 } ⊆ 𝐴 ) |
7 |
|
undif |
⊢ ( { 𝑋 } ⊆ 𝐴 ↔ ( { 𝑋 } ∪ ( 𝐴 ∖ { 𝑋 } ) ) = 𝐴 ) |
8 |
6 7
|
sylib |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( { 𝑋 } ∪ ( 𝐴 ∖ { 𝑋 } ) ) = 𝐴 ) |
9 |
4 8
|
eqtr2id |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → 𝐴 = ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) |
10 |
|
simp1 |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → 𝐴 ∈ Fin ) |
11 |
|
rspcsbela |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℤ ) |
12 |
11
|
zcnd |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℂ ) |
13 |
12
|
expcom |
⊢ ( ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ → ( 𝑥 ∈ 𝐴 → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) |
14 |
13
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( 𝑥 ∈ 𝐴 → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) |
15 |
14
|
imp |
⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ∈ ℂ ) |
16 |
3 9 10 15
|
fsumsplit |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑥 ∈ 𝐴 ⦋ 𝑥 / 𝑘 ⦌ 𝐵 = ( Σ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ⦋ 𝑥 / 𝑘 ⦌ 𝐵 + Σ 𝑥 ∈ { 𝑋 } ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ) ) |
17 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐵 |
18 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐵 |
19 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑥 → 𝐵 = ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ) |
20 |
17 18 19
|
cbvsumi |
⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑥 ∈ 𝐴 ⦋ 𝑥 / 𝑘 ⦌ 𝐵 |
21 |
17 18 19
|
cbvsumi |
⊢ Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 = Σ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ⦋ 𝑥 / 𝑘 ⦌ 𝐵 |
22 |
17 18 19
|
cbvsumi |
⊢ Σ 𝑘 ∈ { 𝑋 } 𝐵 = Σ 𝑥 ∈ { 𝑋 } ⦋ 𝑥 / 𝑘 ⦌ 𝐵 |
23 |
21 22
|
oveq12i |
⊢ ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + Σ 𝑘 ∈ { 𝑋 } 𝐵 ) = ( Σ 𝑥 ∈ ( 𝐴 ∖ { 𝑋 } ) ⦋ 𝑥 / 𝑘 ⦌ 𝐵 + Σ 𝑥 ∈ { 𝑋 } ⦋ 𝑥 / 𝑘 ⦌ 𝐵 ) |
24 |
16 20 23
|
3eqtr4g |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐵 = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + Σ 𝑘 ∈ { 𝑋 } 𝐵 ) ) |
25 |
|
rspcsbela |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∈ ℤ ) |
26 |
25
|
zcnd |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∈ ℂ ) |
27 |
26
|
3adant1 |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∈ ℂ ) |
28 |
|
sumsns |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑋 } 𝐵 = ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ) |
29 |
5 27 28
|
syl2anc |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ { 𝑋 } 𝐵 = ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ) |
30 |
29
|
oveq2d |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + Σ 𝑘 ∈ { 𝑋 } 𝐵 ) = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ) ) |
31 |
24 30
|
eqtrd |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐵 = ( Σ 𝑘 ∈ ( 𝐴 ∖ { 𝑋 } ) 𝐵 + ⦋ 𝑋 / 𝑘 ⦌ 𝐵 ) ) |