ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fisumss GIF version

Theorem fisumss 11047
Description: Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.)
Hypotheses
Ref Expression
fsumss.1 (𝜑𝐴𝐵)
fsumss.2 ((𝜑𝑘𝐴) → 𝐶 ∈ ℂ)
fsumss.3 ((𝜑𝑘 ∈ (𝐵𝐴)) → 𝐶 = 0)
fisumss.adc (𝜑 → ∀𝑗𝐵 DECID 𝑗𝐴)
fsumss.4 (𝜑𝐵 ∈ Fin)
Assertion
Ref Expression
fisumss (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Distinct variable groups:   𝐴,𝑗,𝑘   𝐵,𝑗,𝑘   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑗)   𝐶(𝑗,𝑘)

Proof of Theorem fisumss
Dummy variables 𝑓 𝑢 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsumss.1 . . . . . 6 (𝜑𝐴𝐵)
2 sseq0 3368 . . . . . 6 ((𝐴𝐵𝐵 = ∅) → 𝐴 = ∅)
31, 2sylan 279 . . . . 5 ((𝜑𝐵 = ∅) → 𝐴 = ∅)
43sumeq1d 11021 . . . 4 ((𝜑𝐵 = ∅) → Σ𝑘𝐴 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
5 simpr 109 . . . . 5 ((𝜑𝐵 = ∅) → 𝐵 = ∅)
65sumeq1d 11021 . . . 4 ((𝜑𝐵 = ∅) → Σ𝑘𝐵 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
74, 6eqtr4d 2148 . . 3 ((𝜑𝐵 = ∅) → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
87ex 114 . 2 (𝜑 → (𝐵 = ∅ → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶))
9 cnvimass 4858 . . . . . . . . 9 (𝑓𝐴) ⊆ dom 𝑓
10 simprr 504 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)
11 f1of 5321 . . . . . . . . . 10 (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑓:(1...(♯‘𝐵))⟶𝐵)
1210, 11syl 14 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓:(1...(♯‘𝐵))⟶𝐵)
139, 12fssdm 5243 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓𝐴) ⊆ (1...(♯‘𝐵)))
1412ffnd 5229 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓 Fn (1...(♯‘𝐵)))
15 elpreima 5491 . . . . . . . . . . . 12 (𝑓 Fn (1...(♯‘𝐵)) → (𝑛 ∈ (𝑓𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴)))
1614, 15syl 14 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑛 ∈ (𝑓𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴)))
1712ffvelrnda 5507 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓𝑛) ∈ 𝐵)
1817ex 114 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑛 ∈ (1...(♯‘𝐵)) → (𝑓𝑛) ∈ 𝐵))
1918adantrd 275 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → ((𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴) → (𝑓𝑛) ∈ 𝐵))
2016, 19sylbid 149 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑛 ∈ (𝑓𝐴) → (𝑓𝑛) ∈ 𝐵))
2120imp 123 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (𝑓𝐴)) → (𝑓𝑛) ∈ 𝐵)
22 fsumss.2 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → 𝐶 ∈ ℂ)
2322ex 114 . . . . . . . . . . . . . 14 (𝜑 → (𝑘𝐴𝐶 ∈ ℂ))
2423adantr 272 . . . . . . . . . . . . 13 ((𝜑𝑘𝐵) → (𝑘𝐴𝐶 ∈ ℂ))
25 eldif 3044 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐵𝐴) ↔ (𝑘𝐵 ∧ ¬ 𝑘𝐴))
26 fsumss.3 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵𝐴)) → 𝐶 = 0)
27 0cn 7676 . . . . . . . . . . . . . . . 16 0 ∈ ℂ
2826, 27syl6eqel 2203 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵𝐴)) → 𝐶 ∈ ℂ)
2925, 28sylan2br 284 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘𝐵 ∧ ¬ 𝑘𝐴)) → 𝐶 ∈ ℂ)
3029expr 370 . . . . . . . . . . . . 13 ((𝜑𝑘𝐵) → (¬ 𝑘𝐴𝐶 ∈ ℂ))
31 eleq1w 2173 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑘 → (𝑗𝐴𝑘𝐴))
3231dcbid 806 . . . . . . . . . . . . . . 15 (𝑗 = 𝑘 → (DECID 𝑗𝐴DECID 𝑘𝐴))
33 fisumss.adc . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑗𝐵 DECID 𝑗𝐴)
3433adantr 272 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐵) → ∀𝑗𝐵 DECID 𝑗𝐴)
35 simpr 109 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐵) → 𝑘𝐵)
3632, 34, 35rspcdva 2763 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐵) → DECID 𝑘𝐴)
37 exmiddc 804 . . . . . . . . . . . . . 14 (DECID 𝑘𝐴 → (𝑘𝐴 ∨ ¬ 𝑘𝐴))
3836, 37syl 14 . . . . . . . . . . . . 13 ((𝜑𝑘𝐵) → (𝑘𝐴 ∨ ¬ 𝑘𝐴))
3924, 30, 38mpjaod 690 . . . . . . . . . . . 12 ((𝜑𝑘𝐵) → 𝐶 ∈ ℂ)
4039fmpttd 5527 . . . . . . . . . . 11 (𝜑 → (𝑘𝐵𝐶):𝐵⟶ℂ)
4140adantr 272 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑘𝐵𝐶):𝐵⟶ℂ)
4241ffvelrnda 5507 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ (𝑓𝑛) ∈ 𝐵) → ((𝑘𝐵𝐶)‘(𝑓𝑛)) ∈ ℂ)
4321, 42syldan 278 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (𝑓𝐴)) → ((𝑘𝐵𝐶)‘(𝑓𝑛)) ∈ ℂ)
44 eldifi 3162 . . . . . . . . . . . 12 (𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴)) → 𝑛 ∈ (1...(♯‘𝐵)))
4544, 17sylan2 282 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑓𝑛) ∈ 𝐵)
46 eldifn 3163 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴)) → ¬ 𝑛 ∈ (𝑓𝐴))
4746adantl 273 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ¬ 𝑛 ∈ (𝑓𝐴))
4816adantr 272 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑛 ∈ (𝑓𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴)))
4944adantl 273 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → 𝑛 ∈ (1...(♯‘𝐵)))
5049biantrurd 301 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑓𝑛) ∈ 𝐴 ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴)))
5148, 50bitr4d 190 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑛 ∈ (𝑓𝐴) ↔ (𝑓𝑛) ∈ 𝐴))
5247, 51mtbid 644 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ¬ (𝑓𝑛) ∈ 𝐴)
5345, 52eldifd 3045 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑓𝑛) ∈ (𝐵𝐴))
54 difss 3166 . . . . . . . . . . . . 13 (𝐵𝐴) ⊆ 𝐵
55 resmpt 4823 . . . . . . . . . . . . 13 ((𝐵𝐴) ⊆ 𝐵 → ((𝑘𝐵𝐶) ↾ (𝐵𝐴)) = (𝑘 ∈ (𝐵𝐴) ↦ 𝐶))
5654, 55ax-mp 7 . . . . . . . . . . . 12 ((𝑘𝐵𝐶) ↾ (𝐵𝐴)) = (𝑘 ∈ (𝐵𝐴) ↦ 𝐶)
5756fveq1i 5374 . . . . . . . . . . 11 (((𝑘𝐵𝐶) ↾ (𝐵𝐴))‘(𝑓𝑛)) = ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛))
58 fvres 5397 . . . . . . . . . . 11 ((𝑓𝑛) ∈ (𝐵𝐴) → (((𝑘𝐵𝐶) ↾ (𝐵𝐴))‘(𝑓𝑛)) = ((𝑘𝐵𝐶)‘(𝑓𝑛)))
5957, 58syl5eqr 2159 . . . . . . . . . 10 ((𝑓𝑛) ∈ (𝐵𝐴) → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) = ((𝑘𝐵𝐶)‘(𝑓𝑛)))
6053, 59syl 14 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) = ((𝑘𝐵𝐶)‘(𝑓𝑛)))
61 c0ex 7678 . . . . . . . . . . . . . . 15 0 ∈ V
6261elsn2 3523 . . . . . . . . . . . . . 14 (𝐶 ∈ {0} ↔ 𝐶 = 0)
6326, 62sylibr 133 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵𝐴)) → 𝐶 ∈ {0})
6463fmpttd 5527 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (𝐵𝐴) ↦ 𝐶):(𝐵𝐴)⟶{0})
6564ad2antrr 477 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑘 ∈ (𝐵𝐴) ↦ 𝐶):(𝐵𝐴)⟶{0})
6665, 53ffvelrnd 5508 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) ∈ {0})
67 elsni 3509 . . . . . . . . . 10 (((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) ∈ {0} → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) = 0)
6866, 67syl 14 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) = 0)
6960, 68eqtr3d 2147 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑘𝐵𝐶)‘(𝑓𝑛)) = 0)
70 eleq1 2175 . . . . . . . . . . . . 13 (𝑗 = (𝑓𝑢) → (𝑗𝐴 ↔ (𝑓𝑢) ∈ 𝐴))
7170dcbid 806 . . . . . . . . . . . 12 (𝑗 = (𝑓𝑢) → (DECID 𝑗𝐴DECID (𝑓𝑢) ∈ 𝐴))
7233ad3antrrr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → ∀𝑗𝐵 DECID 𝑗𝐴)
7312ad2antrr 477 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑓:(1...(♯‘𝐵))⟶𝐵)
74 simpr 109 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑢 ∈ (1...(♯‘𝐵)))
7573, 74ffvelrnd 5508 . . . . . . . . . . . 12 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → (𝑓𝑢) ∈ 𝐵)
7671, 72, 75rspcdva 2763 . . . . . . . . . . 11 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → DECID (𝑓𝑢) ∈ 𝐴)
7710ad2antrr 477 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)
78 f1ofun 5323 . . . . . . . . . . . . . 14 (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵 → Fun 𝑓)
7977, 78syl 14 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → Fun 𝑓)
80 f1odm 5325 . . . . . . . . . . . . . . 15 (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵 → dom 𝑓 = (1...(♯‘𝐵)))
8177, 80syl 14 . . . . . . . . . . . . . 14 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → dom 𝑓 = (1...(♯‘𝐵)))
8274, 81eleqtrrd 2192 . . . . . . . . . . . . 13 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑢 ∈ dom 𝑓)
83 fvimacnv 5487 . . . . . . . . . . . . 13 ((Fun 𝑓𝑢 ∈ dom 𝑓) → ((𝑓𝑢) ∈ 𝐴𝑢 ∈ (𝑓𝐴)))
8479, 82, 83syl2anc 406 . . . . . . . . . . . 12 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → ((𝑓𝑢) ∈ 𝐴𝑢 ∈ (𝑓𝐴)))
8584dcbid 806 . . . . . . . . . . 11 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → (DECID (𝑓𝑢) ∈ 𝐴DECID 𝑢 ∈ (𝑓𝐴)))
8676, 85mpbid 146 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → DECID 𝑢 ∈ (𝑓𝐴))
87 elpreima 5491 . . . . . . . . . . . . . . . . 17 (𝑓 Fn (1...(♯‘𝐵)) → (𝑢 ∈ (𝑓𝐴) ↔ (𝑢 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑢) ∈ 𝐴)))
88 simpl 108 . . . . . . . . . . . . . . . . 17 ((𝑢 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑢) ∈ 𝐴) → 𝑢 ∈ (1...(♯‘𝐵)))
8987, 88syl6bi 162 . . . . . . . . . . . . . . . 16 (𝑓 Fn (1...(♯‘𝐵)) → (𝑢 ∈ (𝑓𝐴) → 𝑢 ∈ (1...(♯‘𝐵))))
9089con3d 603 . . . . . . . . . . . . . . 15 (𝑓 Fn (1...(♯‘𝐵)) → (¬ 𝑢 ∈ (1...(♯‘𝐵)) → ¬ 𝑢 ∈ (𝑓𝐴)))
9114, 90syl 14 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (¬ 𝑢 ∈ (1...(♯‘𝐵)) → ¬ 𝑢 ∈ (𝑓𝐴)))
9291adantr 272 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) → (¬ 𝑢 ∈ (1...(♯‘𝐵)) → ¬ 𝑢 ∈ (𝑓𝐴)))
9392imp 123 . . . . . . . . . . . 12 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ ¬ 𝑢 ∈ (1...(♯‘𝐵))) → ¬ 𝑢 ∈ (𝑓𝐴))
9493olcd 706 . . . . . . . . . . 11 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ ¬ 𝑢 ∈ (1...(♯‘𝐵))) → (𝑢 ∈ (𝑓𝐴) ∨ ¬ 𝑢 ∈ (𝑓𝐴)))
95 df-dc 803 . . . . . . . . . . 11 (DECID 𝑢 ∈ (𝑓𝐴) ↔ (𝑢 ∈ (𝑓𝐴) ∨ ¬ 𝑢 ∈ (𝑓𝐴)))
9694, 95sylibr 133 . . . . . . . . . 10 ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) ∧ ¬ 𝑢 ∈ (1...(♯‘𝐵))) → DECID 𝑢 ∈ (𝑓𝐴))
97 eluzelz 9231 . . . . . . . . . . . . 13 (𝑢 ∈ (ℤ‘1) → 𝑢 ∈ ℤ)
9897adantl 273 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) → 𝑢 ∈ ℤ)
99 1zzd 8979 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) → 1 ∈ ℤ)
100 simplrl 507 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) → (♯‘𝐵) ∈ ℕ)
101100nnzd 9070 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) → (♯‘𝐵) ∈ ℤ)
102 fzdcel 9707 . . . . . . . . . . . 12 ((𝑢 ∈ ℤ ∧ 1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → DECID 𝑢 ∈ (1...(♯‘𝐵)))
10398, 99, 101, 102syl3anc 1197 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) → DECID 𝑢 ∈ (1...(♯‘𝐵)))
104 exmiddc 804 . . . . . . . . . . 11 (DECID 𝑢 ∈ (1...(♯‘𝐵)) → (𝑢 ∈ (1...(♯‘𝐵)) ∨ ¬ 𝑢 ∈ (1...(♯‘𝐵))))
105103, 104syl 14 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) → (𝑢 ∈ (1...(♯‘𝐵)) ∨ ¬ 𝑢 ∈ (1...(♯‘𝐵))))
10686, 96, 105mpjaodan 770 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑢 ∈ (ℤ‘1)) → DECID 𝑢 ∈ (𝑓𝐴))
107106ralrimiva 2477 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → ∀𝑢 ∈ (ℤ‘1)DECID 𝑢 ∈ (𝑓𝐴))
108 1zzd 8979 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 1 ∈ ℤ)
109 fzssuz 9732 . . . . . . . . 9 (1...(♯‘𝐵)) ⊆ (ℤ‘1)
110109a1i 9 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (1...(♯‘𝐵)) ⊆ (ℤ‘1))
111103ralrimiva 2477 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → ∀𝑢 ∈ (ℤ‘1)DECID 𝑢 ∈ (1...(♯‘𝐵)))
11213, 43, 69, 107, 108, 110, 111isumss 11046 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑛 ∈ (𝑓𝐴)((𝑘𝐵𝐶)‘(𝑓𝑛)) = Σ𝑛 ∈ (1...(♯‘𝐵))((𝑘𝐵𝐶)‘(𝑓𝑛)))
1131ad2antrr 477 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → 𝐴𝐵)
114113resmptd 4826 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → ((𝑘𝐵𝐶) ↾ 𝐴) = (𝑘𝐴𝐶))
115114fveq1d 5375 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → (((𝑘𝐵𝐶) ↾ 𝐴)‘𝑚) = ((𝑘𝐴𝐶)‘𝑚))
116 fvres 5397 . . . . . . . . . . 11 (𝑚𝐴 → (((𝑘𝐵𝐶) ↾ 𝐴)‘𝑚) = ((𝑘𝐵𝐶)‘𝑚))
117116adantl 273 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → (((𝑘𝐵𝐶) ↾ 𝐴)‘𝑚) = ((𝑘𝐵𝐶)‘𝑚))
118115, 117eqtr3d 2147 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → ((𝑘𝐴𝐶)‘𝑚) = ((𝑘𝐵𝐶)‘𝑚))
119118sumeq2dv 11023 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑚𝐴 ((𝑘𝐵𝐶)‘𝑚))
120 fveq2 5373 . . . . . . . . 9 (𝑚 = (𝑓𝑛) → ((𝑘𝐵𝐶)‘𝑚) = ((𝑘𝐵𝐶)‘(𝑓𝑛)))
1211adantr 272 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝐴𝐵)
122 fsumss.4 . . . . . . . . . . . 12 (𝜑𝐵 ∈ Fin)
123 ssfidc 6773 . . . . . . . . . . . 12 ((𝐵 ∈ Fin ∧ 𝐴𝐵 ∧ ∀𝑗𝐵 DECID 𝑗𝐴) → 𝐴 ∈ Fin)
124122, 1, 33, 123syl3anc 1197 . . . . . . . . . . 11 (𝜑𝐴 ∈ Fin)
125124adantr 272 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝐴 ∈ Fin)
126121, 10, 125preimaf1ofi 6789 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓𝐴) ∈ Fin)
127 f1of1 5320 . . . . . . . . . . . 12 (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑓:(1...(♯‘𝐵))–1-1𝐵)
12810, 127syl 14 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1𝐵)
129 f1ores 5336 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝐵))–1-1𝐵 ∧ (𝑓𝐴) ⊆ (1...(♯‘𝐵))) → (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto→(𝑓 “ (𝑓𝐴)))
130128, 13, 129syl2anc 406 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto→(𝑓 “ (𝑓𝐴)))
131 f1ofo 5328 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑓:(1...(♯‘𝐵))–onto𝐵)
13210, 131syl 14 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓:(1...(♯‘𝐵))–onto𝐵)
133 foimacnv 5339 . . . . . . . . . . . 12 ((𝑓:(1...(♯‘𝐵))–onto𝐵𝐴𝐵) → (𝑓 “ (𝑓𝐴)) = 𝐴)
134132, 121, 133syl2anc 406 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓 “ (𝑓𝐴)) = 𝐴)
135 f1oeq3 5314 . . . . . . . . . . 11 ((𝑓 “ (𝑓𝐴)) = 𝐴 → ((𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto→(𝑓 “ (𝑓𝐴)) ↔ (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto𝐴))
136134, 135syl 14 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → ((𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto→(𝑓 “ (𝑓𝐴)) ↔ (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto𝐴))
137130, 136mpbid 146 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto𝐴)
138 fvres 5397 . . . . . . . . . 10 (𝑛 ∈ (𝑓𝐴) → ((𝑓 ↾ (𝑓𝐴))‘𝑛) = (𝑓𝑛))
139138adantl 273 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (𝑓𝐴)) → ((𝑓 ↾ (𝑓𝐴))‘𝑛) = (𝑓𝑛))
140121sselda 3061 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → 𝑚𝐵)
14141ffvelrnda 5507 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐵) → ((𝑘𝐵𝐶)‘𝑚) ∈ ℂ)
142140, 141syldan 278 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → ((𝑘𝐵𝐶)‘𝑚) ∈ ℂ)
143120, 126, 137, 139, 142fsumf1o 11045 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐵𝐶)‘𝑚) = Σ𝑛 ∈ (𝑓𝐴)((𝑘𝐵𝐶)‘(𝑓𝑛)))
144119, 143eqtrd 2145 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑛 ∈ (𝑓𝐴)((𝑘𝐵𝐶)‘(𝑓𝑛)))
145 simprl 503 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (♯‘𝐵) ∈ ℕ)
146145nnzd 9070 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (♯‘𝐵) ∈ ℤ)
147108, 146fzfigd 10091 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (1...(♯‘𝐵)) ∈ Fin)
148 eqidd 2114 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓𝑛) = (𝑓𝑛))
149120, 147, 10, 148, 141fsumf1o 11045 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐵 ((𝑘𝐵𝐶)‘𝑚) = Σ𝑛 ∈ (1...(♯‘𝐵))((𝑘𝐵𝐶)‘(𝑓𝑛)))
150112, 144, 1493eqtr4d 2155 . . . . . 6 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑚𝐵 ((𝑘𝐵𝐶)‘𝑚))
15122ralrimiva 2477 . . . . . . . 8 (𝜑 → ∀𝑘𝐴 𝐶 ∈ ℂ)
152 sumfct 11029 . . . . . . . 8 (∀𝑘𝐴 𝐶 ∈ ℂ → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑘𝐴 𝐶)
153151, 152syl 14 . . . . . . 7 (𝜑 → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑘𝐴 𝐶)
154153adantr 272 . . . . . 6 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑘𝐴 𝐶)
15522adantlr 466 . . . . . . . . . 10 (((𝜑𝑘𝐵) ∧ 𝑘𝐴) → 𝐶 ∈ ℂ)
156 simpll 501 . . . . . . . . . . . 12 (((𝜑𝑘𝐵) ∧ ¬ 𝑘𝐴) → 𝜑)
157 simplr 502 . . . . . . . . . . . . 13 (((𝜑𝑘𝐵) ∧ ¬ 𝑘𝐴) → 𝑘𝐵)
158 simpr 109 . . . . . . . . . . . . 13 (((𝜑𝑘𝐵) ∧ ¬ 𝑘𝐴) → ¬ 𝑘𝐴)
159157, 158eldifd 3045 . . . . . . . . . . . 12 (((𝜑𝑘𝐵) ∧ ¬ 𝑘𝐴) → 𝑘 ∈ (𝐵𝐴))
160156, 159, 26syl2anc 406 . . . . . . . . . . 11 (((𝜑𝑘𝐵) ∧ ¬ 𝑘𝐴) → 𝐶 = 0)
161 0cnd 7677 . . . . . . . . . . 11 (((𝜑𝑘𝐵) ∧ ¬ 𝑘𝐴) → 0 ∈ ℂ)
162160, 161eqeltrd 2189 . . . . . . . . . 10 (((𝜑𝑘𝐵) ∧ ¬ 𝑘𝐴) → 𝐶 ∈ ℂ)
163155, 162, 38mpjaodan 770 . . . . . . . . 9 ((𝜑𝑘𝐵) → 𝐶 ∈ ℂ)
164163ralrimiva 2477 . . . . . . . 8 (𝜑 → ∀𝑘𝐵 𝐶 ∈ ℂ)
165 sumfct 11029 . . . . . . . 8 (∀𝑘𝐵 𝐶 ∈ ℂ → Σ𝑚𝐵 ((𝑘𝐵𝐶)‘𝑚) = Σ𝑘𝐵 𝐶)
166164, 165syl 14 . . . . . . 7 (𝜑 → Σ𝑚𝐵 ((𝑘𝐵𝐶)‘𝑚) = Σ𝑘𝐵 𝐶)
167166adantr 272 . . . . . 6 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐵 ((𝑘𝐵𝐶)‘𝑚) = Σ𝑘𝐵 𝐶)
168150, 154, 1673eqtr3d 2153 . . . . 5 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
169168expr 370 . . . 4 ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶))
170169exlimdv 1771 . . 3 ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶))
171170expimpd 358 . 2 (𝜑 → (((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵) → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶))
172 fz1f1o 11030 . . 3 (𝐵 ∈ Fin → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)))
173122, 172syl 14 . 2 (𝜑 → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)))
1748, 171, 173mpjaod 690 1 (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 680  DECID wdc 802   = wceq 1312  wex 1449  wcel 1461  wral 2388  cdif 3032  wss 3035  c0 3327  {csn 3491  cmpt 3947  ccnv 4496  dom cdm 4497  cres 4499  cima 4500  Fun wfun 5073   Fn wfn 5074  wf 5075  1-1wf1 5076  ontowfo 5077  1-1-ontowf1o 5078  cfv 5079  (class class class)co 5726  Fincfn 6586  cc 7539  0cc0 7541  1c1 7542  cn 8624  cz 8952  cuz 9222  ...cfz 9677  chash 10408  Σcsu 11008
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-iinf 4460  ax-cnex 7630  ax-resscn 7631  ax-1cn 7632  ax-1re 7633  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-mulrcl 7638  ax-addcom 7639  ax-mulcom 7640  ax-addass 7641  ax-mulass 7642  ax-distr 7643  ax-i2m1 7644  ax-0lt1 7645  ax-1rid 7646  ax-0id 7647  ax-rnegex 7648  ax-precex 7649  ax-cnre 7650  ax-pre-ltirr 7651  ax-pre-ltwlin 7652  ax-pre-lttrn 7653  ax-pre-apti 7654  ax-pre-ltadd 7655  ax-pre-mulgt0 7656  ax-pre-mulext 7657  ax-arch 7658  ax-caucvg 7659
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-reu 2395  df-rmo 2396  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-if 3439  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-po 4176  df-iso 4177  df-iord 4246  df-on 4248  df-ilim 4249  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-isom 5088  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-1st 5990  df-2nd 5991  df-recs 6154  df-irdg 6219  df-frec 6240  df-1o 6265  df-oadd 6269  df-er 6381  df-en 6587  df-dom 6588  df-fin 6589  df-pnf 7720  df-mnf 7721  df-xr 7722  df-ltxr 7723  df-le 7724  df-sub 7852  df-neg 7853  df-reap 8249  df-ap 8256  df-div 8340  df-inn 8625  df-2 8683  df-3 8684  df-4 8685  df-n0 8876  df-z 8953  df-uz 9223  df-q 9308  df-rp 9338  df-fz 9678  df-fzo 9807  df-seqfrec 10106  df-exp 10180  df-ihash 10409  df-cj 10501  df-re 10502  df-im 10503  df-rsqrt 10656  df-abs 10657  df-clim 10934  df-sumdc 11009
This theorem is referenced by:  isumss2  11048
  Copyright terms: Public domain W3C validator