Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esum2dlem Structured version   Visualization version   GIF version

Theorem esum2dlem 30282
Description: Lemma for esum2d 30283 (finite case). (Contributed by Thierry Arnoux, 17-May-2020.) (Proof shortened by AV, 17-Sep-2021.)
Hypotheses
Ref Expression
esum2d.0 𝑘𝐹
esum2d.1 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)
esum2d.2 (𝜑𝐴𝑉)
esum2d.3 ((𝜑𝑗𝐴) → 𝐵𝑊)
esum2d.4 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ (0[,]+∞))
esum2dlem.e (𝜑𝐴 ∈ Fin)
Assertion
Ref Expression
esum2dlem (𝜑 → Σ*𝑗𝐴Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝐴 ({𝑗} × 𝐵)𝐹)
Distinct variable groups:   𝑗,𝑘,𝐴,𝑧   𝑧,𝐶   𝐵,𝑘,𝑧   𝑗,𝐹   𝑗,𝑊,𝑘   𝜑,𝑗,𝑘,𝑧
Allowed substitution hints:   𝐵(𝑗)   𝐶(𝑗,𝑘)   𝐹(𝑧,𝑘)   𝑉(𝑧,𝑗,𝑘)   𝑊(𝑧)

Proof of Theorem esum2dlem
Dummy variables 𝑖 𝑙 𝑡 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 esumeq1 30224 . . 3 (𝑎 = ∅ → Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶)
2 nfv 1883 . . . 4 𝑧 𝑎 = ∅
3 iuneq1 4566 . . . 4 (𝑎 = ∅ → 𝑗𝑎 ({𝑗} × 𝐵) = 𝑗 ∈ ∅ ({𝑗} × 𝐵))
42, 3esumeq1d 30225 . . 3 (𝑎 = ∅ → Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 = Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹)
51, 4eqeq12d 2666 . 2 (𝑎 = ∅ → (Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 ↔ Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹))
6 esumeq1 30224 . . 3 (𝑎 = 𝑏 → Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑗𝑏Σ*𝑘𝐵𝐶)
7 nfv 1883 . . . 4 𝑧 𝑎 = 𝑏
8 iuneq1 4566 . . . 4 (𝑎 = 𝑏 𝑗𝑎 ({𝑗} × 𝐵) = 𝑗𝑏 ({𝑗} × 𝐵))
97, 8esumeq1d 30225 . . 3 (𝑎 = 𝑏 → Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹)
106, 9eqeq12d 2666 . 2 (𝑎 = 𝑏 → (Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 ↔ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹))
11 esumeq1 30224 . . 3 (𝑎 = (𝑏 ∪ {𝑙}) → Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶)
12 nfv 1883 . . . 4 𝑧 𝑎 = (𝑏 ∪ {𝑙})
13 iuneq1 4566 . . . 4 (𝑎 = (𝑏 ∪ {𝑙}) → 𝑗𝑎 ({𝑗} × 𝐵) = 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵))
1412, 13esumeq1d 30225 . . 3 (𝑎 = (𝑏 ∪ {𝑙}) → Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 = Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹)
1511, 14eqeq12d 2666 . 2 (𝑎 = (𝑏 ∪ {𝑙}) → (Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 ↔ Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹))
16 esumeq1 30224 . . 3 (𝑎 = 𝐴 → Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑗𝐴Σ*𝑘𝐵𝐶)
17 nfv 1883 . . . 4 𝑧 𝑎 = 𝐴
18 iuneq1 4566 . . . 4 (𝑎 = 𝐴 𝑗𝑎 ({𝑗} × 𝐵) = 𝑗𝐴 ({𝑗} × 𝐵))
1917, 18esumeq1d 30225 . . 3 (𝑎 = 𝐴 → Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 = Σ*𝑧 𝑗𝐴 ({𝑗} × 𝐵)𝐹)
2016, 19eqeq12d 2666 . 2 (𝑎 = 𝐴 → (Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 ↔ Σ*𝑗𝐴Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝐴 ({𝑗} × 𝐵)𝐹))
21 esumnul 30238 . . . 4 Σ*𝑧 ∈ ∅𝐹 = 0
22 0iun 4609 . . . . 5 𝑗 ∈ ∅ ({𝑗} × 𝐵) = ∅
23 esumeq1 30224 . . . . 5 ( 𝑗 ∈ ∅ ({𝑗} × 𝐵) = ∅ → Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹 = Σ*𝑧 ∈ ∅𝐹)
2422, 23ax-mp 5 . . . 4 Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹 = Σ*𝑧 ∈ ∅𝐹
25 esumnul 30238 . . . 4 Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶 = 0
2621, 24, 253eqtr4ri 2684 . . 3 Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹
2726a1i 11 . 2 (𝜑 → Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹)
28 simpr 476 . . . . 5 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹)
29 nfcsb1v 3582 . . . . . . . . 9 𝑗𝑙 / 𝑗𝐵
30 nfcsb1v 3582 . . . . . . . . 9 𝑗𝑙 / 𝑗𝐶
3129, 30nfesum2 30231 . . . . . . . 8 𝑗Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶
32 csbeq1a 3575 . . . . . . . . . 10 (𝑗 = 𝑙𝐵 = 𝑙 / 𝑗𝐵)
33 csbeq1a 3575 . . . . . . . . . 10 (𝑗 = 𝑙𝐶 = 𝑙 / 𝑗𝐶)
3432, 33esumeq12d 30223 . . . . . . . . 9 (𝑗 = 𝑙 → Σ*𝑘𝐵𝐶 = Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶)
3534adantl 481 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗 = 𝑙) → Σ*𝑘𝐵𝐶 = Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶)
36 simprr 811 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑙 ∈ (𝐴𝑏))
3736eldifad 3619 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑙𝐴)
38 esum2d.3 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → 𝐵𝑊)
3938adantlr 751 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝐴) → 𝐵𝑊)
4039ralrimiva 2995 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ∀𝑗𝐴 𝐵𝑊)
41 rspcsbela 4039 . . . . . . . . . 10 ((𝑙𝐴 ∧ ∀𝑗𝐴 𝐵𝑊) → 𝑙 / 𝑗𝐵𝑊)
4237, 40, 41syl2anc 694 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑙 / 𝑗𝐵𝑊)
43 simpll 805 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝜑)
4437adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝑙𝐴)
45 simpr 476 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝑘𝑙 / 𝑗𝐵)
46 esum2d.4 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ (0[,]+∞))
4746ex 449 . . . . . . . . . . . . . 14 (𝜑 → ((𝑗𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞)))
4847sbcimdv 3531 . . . . . . . . . . . . 13 (𝜑 → ([𝑙 / 𝑗](𝑗𝐴𝑘𝐵) → [𝑙 / 𝑗]𝐶 ∈ (0[,]+∞)))
49 sbcan 3511 . . . . . . . . . . . . . 14 ([𝑙 / 𝑗](𝑗𝐴𝑘𝐵) ↔ ([𝑙 / 𝑗]𝑗𝐴[𝑙 / 𝑗]𝑘𝐵))
50 sbcel1v 3528 . . . . . . . . . . . . . . 15 ([𝑙 / 𝑗]𝑗𝐴𝑙𝐴)
51 sbcel2 4022 . . . . . . . . . . . . . . 15 ([𝑙 / 𝑗]𝑘𝐵𝑘𝑙 / 𝑗𝐵)
5250, 51anbi12i 733 . . . . . . . . . . . . . 14 (([𝑙 / 𝑗]𝑗𝐴[𝑙 / 𝑗]𝑘𝐵) ↔ (𝑙𝐴𝑘𝑙 / 𝑗𝐵))
5349, 52bitri 264 . . . . . . . . . . . . 13 ([𝑙 / 𝑗](𝑗𝐴𝑘𝐵) ↔ (𝑙𝐴𝑘𝑙 / 𝑗𝐵))
54 vex 3234 . . . . . . . . . . . . . 14 𝑙 ∈ V
55 sbcel1g 4020 . . . . . . . . . . . . . 14 (𝑙 ∈ V → ([𝑙 / 𝑗]𝐶 ∈ (0[,]+∞) ↔ 𝑙 / 𝑗𝐶 ∈ (0[,]+∞)))
5654, 55ax-mp 5 . . . . . . . . . . . . 13 ([𝑙 / 𝑗]𝐶 ∈ (0[,]+∞) ↔ 𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
5748, 53, 563imtr3g 284 . . . . . . . . . . . 12 (𝜑 → ((𝑙𝐴𝑘𝑙 / 𝑗𝐵) → 𝑙 / 𝑗𝐶 ∈ (0[,]+∞)))
5857imp 444 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙𝐴𝑘𝑙 / 𝑗𝐵)) → 𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
5943, 44, 45, 58syl12anc 1364 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
6059ralrimiva 2995 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ∀𝑘 𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
61 nfcv 2793 . . . . . . . . . 10 𝑘𝑙 / 𝑗𝐵
6261esumcl 30220 . . . . . . . . 9 ((𝑙 / 𝑗𝐵𝑊 ∧ ∀𝑘 𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 ∈ (0[,]+∞)) → Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
6342, 60, 62syl2anc 694 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
6431, 35, 36, 63esumsnf 30254 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶 = Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶)
65 esum2d.0 . . . . . . . . 9 𝑘𝐹
66 nfv 1883 . . . . . . . . 9 𝑘(𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏)))
67 nfv 1883 . . . . . . . . . . 11 𝑗 𝑧 = ⟨𝑙, 𝑘
6830nfeq2 2809 . . . . . . . . . . 11 𝑗 𝐹 = 𝑙 / 𝑗𝐶
6967, 68nfim 1865 . . . . . . . . . 10 𝑗(𝑧 = ⟨𝑙, 𝑘⟩ → 𝐹 = 𝑙 / 𝑗𝐶)
70 opeq1 4433 . . . . . . . . . . . 12 (𝑗 = 𝑙 → ⟨𝑗, 𝑘⟩ = ⟨𝑙, 𝑘⟩)
7170eqeq2d 2661 . . . . . . . . . . 11 (𝑗 = 𝑙 → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑧 = ⟨𝑙, 𝑘⟩))
7233eqeq2d 2661 . . . . . . . . . . 11 (𝑗 = 𝑙 → (𝐹 = 𝐶𝐹 = 𝑙 / 𝑗𝐶))
7371, 72imbi12d 333 . . . . . . . . . 10 (𝑗 = 𝑙 → ((𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶) ↔ (𝑧 = ⟨𝑙, 𝑘⟩ → 𝐹 = 𝑙 / 𝑗𝐶)))
74 esum2d.1 . . . . . . . . . 10 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)
7569, 73, 74chvar 2298 . . . . . . . . 9 (𝑧 = ⟨𝑙, 𝑘⟩ → 𝐹 = 𝑙 / 𝑗𝐶)
76 vsnid 4242 . . . . . . . . . . . . . . . . 17 𝑗 ∈ {𝑗}
7776a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝑗 ∈ {𝑗})
78 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝑘𝐵)
7977, 78opelxpd 5183 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → ⟨𝑗, 𝑘⟩ ∈ ({𝑗} × 𝐵))
80 xp2nd 7243 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑗} × 𝐵) → (2nd𝑧) ∈ 𝐵)
81 xp1st 7242 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ {𝑗})
82 fvex 6239 . . . . . . . . . . . . . . . . . . . . . 22 (1st𝑧) ∈ V
8382elsn 4225 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑧) ∈ {𝑗} ↔ (1st𝑧) = 𝑗)
8481, 83sylib 208 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) = 𝑗)
85 eqop 7252 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ({𝑗} × 𝐵) → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ ((1st𝑧) = 𝑗 ∧ (2nd𝑧) = 𝑘)))
8684, 85mpbirand 529 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ({𝑗} × 𝐵) → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ (2nd𝑧) = 𝑘))
87 eqcom 2658 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑧) = 𝑘𝑘 = (2nd𝑧))
8886, 87syl6bb 276 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ({𝑗} × 𝐵) → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑘 = (2nd𝑧)))
8988ad2antlr 763 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑘 = (2nd𝑧)))
9089ralrimiva 2995 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∀𝑘𝐵 (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑘 = (2nd𝑧)))
91 reu6i 3430 . . . . . . . . . . . . . . . 16 (((2nd𝑧) ∈ 𝐵 ∧ ∀𝑘𝐵 (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑘 = (2nd𝑧))) → ∃!𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
9280, 90, 91syl2an2 892 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃!𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
9379, 92f1mptrn 29563 . . . . . . . . . . . . . 14 ((𝜑𝑗𝐴) → Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩))
9493ex 449 . . . . . . . . . . . . 13 (𝜑 → (𝑗𝐴 → Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩)))
9594sbcimdv 3531 . . . . . . . . . . . 12 (𝜑 → ([𝑙 / 𝑗]𝑗𝐴[𝑙 / 𝑗]Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩)))
96 sbcfung 5950 . . . . . . . . . . . . . 14 (𝑙 ∈ V → ([𝑙 / 𝑗]Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) ↔ Fun 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩)))
97 csbcnv 5338 . . . . . . . . . . . . . . . 16 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩)
98 csbmpt12 5039 . . . . . . . . . . . . . . . . . 18 (𝑙 ∈ V → 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝑗, 𝑘⟩))
99 csbopg 4451 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ V → 𝑙 / 𝑗𝑗, 𝑘⟩ = ⟨𝑙 / 𝑗𝑗, 𝑙 / 𝑗𝑘⟩)
100 csbvarg 4036 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ V → 𝑙 / 𝑗𝑗 = 𝑙)
101 csbconstg 3579 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ V → 𝑙 / 𝑗𝑘 = 𝑘)
102100, 101opeq12d 4441 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ V → ⟨𝑙 / 𝑗𝑗, 𝑙 / 𝑗𝑘⟩ = ⟨𝑙, 𝑘⟩)
10399, 102eqtrd 2685 . . . . . . . . . . . . . . . . . . 19 (𝑙 ∈ V → 𝑙 / 𝑗𝑗, 𝑘⟩ = ⟨𝑙, 𝑘⟩)
104103mpteq2dv 4778 . . . . . . . . . . . . . . . . . 18 (𝑙 ∈ V → (𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
10598, 104eqtrd 2685 . . . . . . . . . . . . . . . . 17 (𝑙 ∈ V → 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
106105cnveqd 5330 . . . . . . . . . . . . . . . 16 (𝑙 ∈ V → 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
10797, 106syl5eqr 2699 . . . . . . . . . . . . . . 15 (𝑙 ∈ V → 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
108107funeqd 5948 . . . . . . . . . . . . . 14 (𝑙 ∈ V → (Fun 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) ↔ Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩)))
10996, 108bitrd 268 . . . . . . . . . . . . 13 (𝑙 ∈ V → ([𝑙 / 𝑗]Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) ↔ Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩)))
11054, 109ax-mp 5 . . . . . . . . . . . 12 ([𝑙 / 𝑗]Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) ↔ Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
11195, 50, 1103imtr3g 284 . . . . . . . . . . 11 (𝜑 → (𝑙𝐴 → Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩)))
112111imp 444 . . . . . . . . . 10 ((𝜑𝑙𝐴) → Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
11337, 112syldan 486 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
114 vsnid 4242 . . . . . . . . . . 11 𝑙 ∈ {𝑙}
115114a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝑙 ∈ {𝑙})
116115, 45opelxpd 5183 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → ⟨𝑙, 𝑘⟩ ∈ ({𝑙} × 𝑙 / 𝑗𝐵))
11765, 66, 61, 75, 42, 113, 59, 116esumc 30241 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 = Σ*𝑧 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩}𝐹)
118 nfab1 2795 . . . . . . . . . 10 𝑡{𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩}
119 nfcv 2793 . . . . . . . . . 10 𝑡({𝑙} × 𝑙 / 𝑗𝐵)
120 opeq1 4433 . . . . . . . . . . . . . 14 (𝑖 = 𝑙 → ⟨𝑖, 𝑘⟩ = ⟨𝑙, 𝑘⟩)
121120eqeq2d 2661 . . . . . . . . . . . . 13 (𝑖 = 𝑙 → (𝑡 = ⟨𝑖, 𝑘⟩ ↔ 𝑡 = ⟨𝑙, 𝑘⟩))
122121rexbidv 3081 . . . . . . . . . . . 12 (𝑖 = 𝑙 → (∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑖, 𝑘⟩ ↔ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩))
12354, 122rexsn 4255 . . . . . . . . . . 11 (∃𝑖 ∈ {𝑙}∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑖, 𝑘⟩ ↔ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩)
124 elxp2 5166 . . . . . . . . . . 11 (𝑡 ∈ ({𝑙} × 𝑙 / 𝑗𝐵) ↔ ∃𝑖 ∈ {𝑙}∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑖, 𝑘⟩)
125 abid 2639 . . . . . . . . . . 11 (𝑡 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩} ↔ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩)
126123, 124, 1253bitr4ri 293 . . . . . . . . . 10 (𝑡 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩} ↔ 𝑡 ∈ ({𝑙} × 𝑙 / 𝑗𝐵))
127118, 119, 126eqri 29443 . . . . . . . . 9 {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩} = ({𝑙} × 𝑙 / 𝑗𝐵)
128 esumeq1 30224 . . . . . . . . 9 ({𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩} = ({𝑙} × 𝑙 / 𝑗𝐵) → Σ*𝑧 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩}𝐹 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹)
129127, 128ax-mp 5 . . . . . . . 8 Σ*𝑧 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩}𝐹 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹
130117, 129syl6eq 2701 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹)
13164, 130eqtrd 2685 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹)
132131adantr 480 . . . . 5 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹)
13328, 132oveq12d 6708 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → (Σ*𝑗𝑏Σ*𝑘𝐵𝐶 +𝑒 Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶) = (Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 +𝑒 Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹))
134 nfv 1883 . . . . . 6 𝑗(𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏)))
135 nfcv 2793 . . . . . 6 𝑗𝑏
136 nfcv 2793 . . . . . 6 𝑗{𝑙}
137 vex 3234 . . . . . . 7 𝑏 ∈ V
138137a1i 11 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑏 ∈ V)
139 snex 4938 . . . . . . 7 {𝑙} ∈ V
140139a1i 11 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → {𝑙} ∈ V)
14136eldifbd 3620 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ¬ 𝑙𝑏)
142 disjsn 4278 . . . . . . 7 ((𝑏 ∩ {𝑙}) = ∅ ↔ ¬ 𝑙𝑏)
143141, 142sylibr 224 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → (𝑏 ∩ {𝑙}) = ∅)
144 simpll 805 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝜑)
145 simprl 809 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑏𝐴)
146145sselda 3636 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝑗𝐴)
14746anassrs 681 . . . . . . . . 9 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
148147ralrimiva 2995 . . . . . . . 8 ((𝜑𝑗𝐴) → ∀𝑘𝐵 𝐶 ∈ (0[,]+∞))
149 nfcv 2793 . . . . . . . . 9 𝑘𝐵
150149esumcl 30220 . . . . . . . 8 ((𝐵𝑊 ∧ ∀𝑘𝐵 𝐶 ∈ (0[,]+∞)) → Σ*𝑘𝐵𝐶 ∈ (0[,]+∞))
15138, 148, 150syl2anc 694 . . . . . . 7 ((𝜑𝑗𝐴) → Σ*𝑘𝐵𝐶 ∈ (0[,]+∞))
152144, 146, 151syl2anc 694 . . . . . 6 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → Σ*𝑘𝐵𝐶 ∈ (0[,]+∞))
153 simpll 805 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗 ∈ {𝑙}) → 𝜑)
15437snssd 4372 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → {𝑙} ⊆ 𝐴)
155154sselda 3636 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗 ∈ {𝑙}) → 𝑗𝐴)
156153, 155, 151syl2anc 694 . . . . . 6 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗 ∈ {𝑙}) → Σ*𝑘𝐵𝐶 ∈ (0[,]+∞))
157134, 135, 136, 138, 140, 143, 152, 156esumsplit 30243 . . . . 5 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = (Σ*𝑗𝑏Σ*𝑘𝐵𝐶 +𝑒 Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶))
158157adantr 480 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = (Σ*𝑗𝑏Σ*𝑘𝐵𝐶 +𝑒 Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶))
159 iunxun 4637 . . . . . . . 8 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑙} ({𝑗} × 𝐵))
160136, 29nfxp 5176 . . . . . . . . . . 11 𝑗({𝑙} × 𝑙 / 𝑗𝐵)
161 sneq 4220 . . . . . . . . . . . 12 (𝑗 = 𝑙 → {𝑗} = {𝑙})
162161, 32xpeq12d 5174 . . . . . . . . . . 11 (𝑗 = 𝑙 → ({𝑗} × 𝐵) = ({𝑙} × 𝑙 / 𝑗𝐵))
163160, 162iunxsngf 29501 . . . . . . . . . 10 (𝑙 ∈ V → 𝑗 ∈ {𝑙} ({𝑗} × 𝐵) = ({𝑙} × 𝑙 / 𝑗𝐵))
16454, 163ax-mp 5 . . . . . . . . 9 𝑗 ∈ {𝑙} ({𝑗} × 𝐵) = ({𝑙} × 𝑙 / 𝑗𝐵)
165164uneq2i 3797 . . . . . . . 8 ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑙} ({𝑗} × 𝐵)) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))
166159, 165eqtri 2673 . . . . . . 7 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))
167 esumeq1 30224 . . . . . . 7 ( 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵)) → Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹 = Σ*𝑧 ∈ ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))𝐹)
168166, 167ax-mp 5 . . . . . 6 Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹 = Σ*𝑧 ∈ ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))𝐹
169 nfv 1883 . . . . . . 7 𝑧(𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏)))
170 nfcv 2793 . . . . . . 7 𝑧 𝑗𝑏 ({𝑗} × 𝐵)
171 nfcv 2793 . . . . . . 7 𝑧({𝑙} × 𝑙 / 𝑗𝐵)
172 snex 4938 . . . . . . . . . 10 {𝑗} ∈ V
173146, 39syldan 486 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝐵𝑊)
174 xpexg 7002 . . . . . . . . . 10 (({𝑗} ∈ V ∧ 𝐵𝑊) → ({𝑗} × 𝐵) ∈ V)
175172, 173, 174sylancr 696 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → ({𝑗} × 𝐵) ∈ V)
176175ralrimiva 2995 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ∀𝑗𝑏 ({𝑗} × 𝐵) ∈ V)
177 iunexg 7185 . . . . . . . 8 ((𝑏 ∈ V ∧ ∀𝑗𝑏 ({𝑗} × 𝐵) ∈ V) → 𝑗𝑏 ({𝑗} × 𝐵) ∈ V)
178137, 176, 177sylancr 696 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑗𝑏 ({𝑗} × 𝐵) ∈ V)
179 xpexg 7002 . . . . . . . 8 (({𝑙} ∈ V ∧ 𝑙 / 𝑗𝐵𝑊) → ({𝑙} × 𝑙 / 𝑗𝐵) ∈ V)
180139, 42, 179sylancr 696 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ({𝑙} × 𝑙 / 𝑗𝐵) ∈ V)
181 simpr 476 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝑗𝑏)
182141adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → ¬ 𝑙𝑏)
183 nelne2 2920 . . . . . . . . . . 11 ((𝑗𝑏 ∧ ¬ 𝑙𝑏) → 𝑗𝑙)
184181, 182, 183syl2anc 694 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝑗𝑙)
185 disjsn2 4279 . . . . . . . . . 10 (𝑗𝑙 → ({𝑗} ∩ {𝑙}) = ∅)
186 xpdisj1 5590 . . . . . . . . . 10 (({𝑗} ∩ {𝑙}) = ∅ → (({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = ∅)
187184, 185, 1863syl 18 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → (({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = ∅)
188187iuneq2dv 4574 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑗𝑏 (({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = 𝑗𝑏 ∅)
189160iunin1f 29500 . . . . . . . 8 𝑗𝑏 (({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵))
190 iun0 4608 . . . . . . . 8 𝑗𝑏 ∅ = ∅
191188, 189, 1903eqtr3g 2708 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ( 𝑗𝑏 ({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = ∅)
192 simpll 805 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 𝑗𝑏 ({𝑗} × 𝐵)) → 𝜑)
193 iunss1 4564 . . . . . . . . . 10 (𝑏𝐴 𝑗𝑏 ({𝑗} × 𝐵) ⊆ 𝑗𝐴 ({𝑗} × 𝐵))
194145, 193syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑗𝑏 ({𝑗} × 𝐵) ⊆ 𝑗𝐴 ({𝑗} × 𝐵))
195194sselda 3636 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 𝑗𝑏 ({𝑗} × 𝐵)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐵))
196 nfv 1883 . . . . . . . . . 10 𝑗𝜑
197 nfiu1 4582 . . . . . . . . . . 11 𝑗 𝑗𝐴 ({𝑗} × 𝐵)
198197nfcri 2787 . . . . . . . . . 10 𝑗 𝑧 𝑗𝐴 ({𝑗} × 𝐵)
199196, 198nfan 1868 . . . . . . . . 9 𝑗(𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵))
200 nfv 1883 . . . . . . . . . 10 𝑘(((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵))
201 nfcv 2793 . . . . . . . . . . 11 𝑘(0[,]+∞)
20265, 201nfel 2806 . . . . . . . . . 10 𝑘 𝐹 ∈ (0[,]+∞)
20374adantl 481 . . . . . . . . . . 11 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐹 = 𝐶)
204 simp-5l 825 . . . . . . . . . . . 12 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝜑)
205 simp-4r 824 . . . . . . . . . . . 12 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝑗𝐴)
206 simplr 807 . . . . . . . . . . . 12 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝑘𝐵)
207204, 205, 206, 46syl12anc 1364 . . . . . . . . . . 11 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐶 ∈ (0[,]+∞))
208203, 207eqeltrd 2730 . . . . . . . . . 10 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐹 ∈ (0[,]+∞))
209 elsnxp 5715 . . . . . . . . . . . 12 (𝑗𝐴 → (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩))
210209biimpa 500 . . . . . . . . . . 11 ((𝑗𝐴𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
211210adantll 750 . . . . . . . . . 10 ((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
212200, 202, 208, 211r19.29af2 3104 . . . . . . . . 9 ((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
213 simpr 476 . . . . . . . . . 10 ((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐵))
214 eliun 4556 . . . . . . . . . 10 (𝑧 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝐴 𝑧 ∈ ({𝑗} × 𝐵))
215213, 214sylib 208 . . . . . . . . 9 ((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) → ∃𝑗𝐴 𝑧 ∈ ({𝑗} × 𝐵))
216199, 212, 215r19.29af 3105 . . . . . . . 8 ((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
217192, 195, 216syl2anc 694 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 𝑗𝑏 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
218 simpll 805 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)) → 𝜑)
219 nfcv 2793 . . . . . . . . . . 11 𝑗𝐴
220 nfcv 2793 . . . . . . . . . . 11 𝑗𝑙
221219, 220, 160, 162ssiun2sf 29504 . . . . . . . . . 10 (𝑙𝐴 → ({𝑙} × 𝑙 / 𝑗𝐵) ⊆ 𝑗𝐴 ({𝑗} × 𝐵))
22237, 221syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ({𝑙} × 𝑙 / 𝑗𝐵) ⊆ 𝑗𝐴 ({𝑗} × 𝐵))
223222sselda 3636 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐵))
224218, 223, 216syl2anc 694 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)) → 𝐹 ∈ (0[,]+∞))
225169, 170, 171, 178, 180, 191, 217, 224esumsplit 30243 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑧 ∈ ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))𝐹 = (Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 +𝑒 Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹))
226168, 225syl5eq 2697 . . . . 5 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹 = (Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 +𝑒 Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹))
227226adantr 480 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹 = (Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 +𝑒 Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹))
228133, 158, 2273eqtr4d 2695 . . 3 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹)
229228ex 449 . 2 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → (Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 → Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹))
230 esum2dlem.e . 2 (𝜑𝐴 ∈ Fin)
2315, 10, 15, 20, 27, 229, 230findcard2d 8243 1 (𝜑 → Σ*𝑗𝐴Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝐴 ({𝑗} × 𝐵)𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  {cab 2637  wnfc 2780  wne 2823  wral 2941  wrex 2942  ∃!wreu 2943  Vcvv 3231  [wsbc 3468  csb 3566  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  {csn 4210  cop 4216   ciun 4552  cmpt 4762   × cxp 5141  ccnv 5142  Fun wfun 5920  cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  Fincfn 7997  0cc0 9974  +∞cpnf 10109   +𝑒 cxad 11982  [,]cicc 12216  Σ*cesum 30217
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-sin 14844  df-cos 14845  df-pi 14847  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-ordt 16208  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-ps 17247  df-tsr 17248  df-plusf 17288  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-mhm 17382  df-submnd 17383  df-grp 17472  df-minusg 17473  df-sbg 17474  df-mulg 17588  df-subg 17638  df-cntz 17796  df-cmn 18241  df-abl 18242  df-mgp 18536  df-ur 18548  df-ring 18595  df-cring 18596  df-subrg 18826  df-abv 18865  df-lmod 18913  df-scaf 18914  df-sra 19220  df-rgmod 19221  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-tmd 21923  df-tgp 21924  df-tsms 21977  df-trg 22010  df-xms 22172  df-ms 22173  df-tms 22174  df-nm 22434  df-ngp 22435  df-nrg 22437  df-nlm 22438  df-ii 22727  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-esum 30218
This theorem is referenced by:  esum2d  30283
  Copyright terms: Public domain W3C validator