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 31024
Description: Lemma for esum2d 31025 (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 30966 . . 3 (𝑎 = ∅ → Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶)
2 nfv 1873 . . . 4 𝑧 𝑎 = ∅
3 iuneq1 4803 . . . 4 (𝑎 = ∅ → 𝑗𝑎 ({𝑗} × 𝐵) = 𝑗 ∈ ∅ ({𝑗} × 𝐵))
42, 3esumeq1d 30967 . . 3 (𝑎 = ∅ → Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 = Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹)
51, 4eqeq12d 2787 . 2 (𝑎 = ∅ → (Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 ↔ Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹))
6 esumeq1 30966 . . 3 (𝑎 = 𝑏 → Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑗𝑏Σ*𝑘𝐵𝐶)
7 nfv 1873 . . . 4 𝑧 𝑎 = 𝑏
8 iuneq1 4803 . . . 4 (𝑎 = 𝑏 𝑗𝑎 ({𝑗} × 𝐵) = 𝑗𝑏 ({𝑗} × 𝐵))
97, 8esumeq1d 30967 . . 3 (𝑎 = 𝑏 → Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹)
106, 9eqeq12d 2787 . 2 (𝑎 = 𝑏 → (Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 ↔ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹))
11 esumeq1 30966 . . 3 (𝑎 = (𝑏 ∪ {𝑙}) → Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶)
12 nfv 1873 . . . 4 𝑧 𝑎 = (𝑏 ∪ {𝑙})
13 iuneq1 4803 . . . 4 (𝑎 = (𝑏 ∪ {𝑙}) → 𝑗𝑎 ({𝑗} × 𝐵) = 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵))
1412, 13esumeq1d 30967 . . 3 (𝑎 = (𝑏 ∪ {𝑙}) → Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 = Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹)
1511, 14eqeq12d 2787 . 2 (𝑎 = (𝑏 ∪ {𝑙}) → (Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 ↔ Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹))
16 esumeq1 30966 . . 3 (𝑎 = 𝐴 → Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑗𝐴Σ*𝑘𝐵𝐶)
17 nfv 1873 . . . 4 𝑧 𝑎 = 𝐴
18 iuneq1 4803 . . . 4 (𝑎 = 𝐴 𝑗𝑎 ({𝑗} × 𝐵) = 𝑗𝐴 ({𝑗} × 𝐵))
1917, 18esumeq1d 30967 . . 3 (𝑎 = 𝐴 → Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 = Σ*𝑧 𝑗𝐴 ({𝑗} × 𝐵)𝐹)
2016, 19eqeq12d 2787 . 2 (𝑎 = 𝐴 → (Σ*𝑗𝑎Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑎 ({𝑗} × 𝐵)𝐹 ↔ Σ*𝑗𝐴Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝐴 ({𝑗} × 𝐵)𝐹))
21 esumnul 30980 . . . 4 Σ*𝑧 ∈ ∅𝐹 = 0
22 0iun 4848 . . . . 5 𝑗 ∈ ∅ ({𝑗} × 𝐵) = ∅
23 esumeq1 30966 . . . . 5 ( 𝑗 ∈ ∅ ({𝑗} × 𝐵) = ∅ → Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹 = Σ*𝑧 ∈ ∅𝐹)
2422, 23ax-mp 5 . . . 4 Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹 = Σ*𝑧 ∈ ∅𝐹
25 esumnul 30980 . . . 4 Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶 = 0
2621, 24, 253eqtr4ri 2807 . . 3 Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹
2726a1i 11 . 2 (𝜑 → Σ*𝑗 ∈ ∅Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ ∅ ({𝑗} × 𝐵)𝐹)
28 simpr 477 . . . . 5 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹)
29 nfcsb1v 3798 . . . . . . . . 9 𝑗𝑙 / 𝑗𝐵
30 nfcsb1v 3798 . . . . . . . . 9 𝑗𝑙 / 𝑗𝐶
3129, 30nfesum2 30973 . . . . . . . 8 𝑗Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶
32 csbeq1a 3789 . . . . . . . . . 10 (𝑗 = 𝑙𝐵 = 𝑙 / 𝑗𝐵)
33 csbeq1a 3789 . . . . . . . . . 10 (𝑗 = 𝑙𝐶 = 𝑙 / 𝑗𝐶)
3432, 33esumeq12d 30965 . . . . . . . . 9 (𝑗 = 𝑙 → Σ*𝑘𝐵𝐶 = Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶)
3534adantl 474 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗 = 𝑙) → Σ*𝑘𝐵𝐶 = Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶)
36 simprr 760 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑙 ∈ (𝐴𝑏))
3736eldifad 3835 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑙𝐴)
38 esum2d.3 . . . . . . . . . . . 12 ((𝜑𝑗𝐴) → 𝐵𝑊)
3938adantlr 702 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝐴) → 𝐵𝑊)
4039ralrimiva 3126 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ∀𝑗𝐴 𝐵𝑊)
41 rspcsbela 4265 . . . . . . . . . 10 ((𝑙𝐴 ∧ ∀𝑗𝐴 𝐵𝑊) → 𝑙 / 𝑗𝐵𝑊)
4237, 40, 41syl2anc 576 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑙 / 𝑗𝐵𝑊)
43 simpll 754 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝜑)
4437adantr 473 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝑙𝐴)
45 simpr 477 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝑘𝑙 / 𝑗𝐵)
46 esum2d.4 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑗𝐴𝑘𝐵)) → 𝐶 ∈ (0[,]+∞))
4746ex 405 . . . . . . . . . . . . . 14 (𝜑 → ((𝑗𝐴𝑘𝐵) → 𝐶 ∈ (0[,]+∞)))
4847sbcimdv 3740 . . . . . . . . . . . . 13 (𝜑 → ([𝑙 / 𝑗](𝑗𝐴𝑘𝐵) → [𝑙 / 𝑗]𝐶 ∈ (0[,]+∞)))
49 sbcan 3719 . . . . . . . . . . . . . 14 ([𝑙 / 𝑗](𝑗𝐴𝑘𝐵) ↔ ([𝑙 / 𝑗]𝑗𝐴[𝑙 / 𝑗]𝑘𝐵))
50 sbcel1v 3736 . . . . . . . . . . . . . . 15 ([𝑙 / 𝑗]𝑗𝐴𝑙𝐴)
51 sbcel2 4247 . . . . . . . . . . . . . . 15 ([𝑙 / 𝑗]𝑘𝐵𝑘𝑙 / 𝑗𝐵)
5250, 51anbi12i 617 . . . . . . . . . . . . . 14 (([𝑙 / 𝑗]𝑗𝐴[𝑙 / 𝑗]𝑘𝐵) ↔ (𝑙𝐴𝑘𝑙 / 𝑗𝐵))
5349, 52bitri 267 . . . . . . . . . . . . 13 ([𝑙 / 𝑗](𝑗𝐴𝑘𝐵) ↔ (𝑙𝐴𝑘𝑙 / 𝑗𝐵))
54 vex 3412 . . . . . . . . . . . . . 14 𝑙 ∈ V
55 sbcel1g 4245 . . . . . . . . . . . . . 14 (𝑙 ∈ V → ([𝑙 / 𝑗]𝐶 ∈ (0[,]+∞) ↔ 𝑙 / 𝑗𝐶 ∈ (0[,]+∞)))
5654, 55ax-mp 5 . . . . . . . . . . . . 13 ([𝑙 / 𝑗]𝐶 ∈ (0[,]+∞) ↔ 𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
5748, 53, 563imtr3g 287 . . . . . . . . . . . 12 (𝜑 → ((𝑙𝐴𝑘𝑙 / 𝑗𝐵) → 𝑙 / 𝑗𝐶 ∈ (0[,]+∞)))
5857imp 398 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙𝐴𝑘𝑙 / 𝑗𝐵)) → 𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
5943, 44, 45, 58syl12anc 824 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
6059ralrimiva 3126 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ∀𝑘 𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
61 nfcv 2926 . . . . . . . . . 10 𝑘𝑙 / 𝑗𝐵
6261esumcl 30962 . . . . . . . . 9 ((𝑙 / 𝑗𝐵𝑊 ∧ ∀𝑘 𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 ∈ (0[,]+∞)) → Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
6342, 60, 62syl2anc 576 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 ∈ (0[,]+∞))
6431, 35, 36, 63esumsnf 30996 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶 = Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶)
65 esum2d.0 . . . . . . . . 9 𝑘𝐹
66 nfv 1873 . . . . . . . . 9 𝑘(𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏)))
67 nfv 1873 . . . . . . . . . . 11 𝑗 𝑧 = ⟨𝑙, 𝑘
6830nfeq2 2941 . . . . . . . . . . 11 𝑗 𝐹 = 𝑙 / 𝑗𝐶
6967, 68nfim 1859 . . . . . . . . . 10 𝑗(𝑧 = ⟨𝑙, 𝑘⟩ → 𝐹 = 𝑙 / 𝑗𝐶)
70 opeq1 4673 . . . . . . . . . . . 12 (𝑗 = 𝑙 → ⟨𝑗, 𝑘⟩ = ⟨𝑙, 𝑘⟩)
7170eqeq2d 2782 . . . . . . . . . . 11 (𝑗 = 𝑙 → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑧 = ⟨𝑙, 𝑘⟩))
7233eqeq2d 2782 . . . . . . . . . . 11 (𝑗 = 𝑙 → (𝐹 = 𝐶𝐹 = 𝑙 / 𝑗𝐶))
7371, 72imbi12d 337 . . . . . . . . . 10 (𝑗 = 𝑙 → ((𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶) ↔ (𝑧 = ⟨𝑙, 𝑘⟩ → 𝐹 = 𝑙 / 𝑗𝐶)))
74 esum2d.1 . . . . . . . . . 10 (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐹 = 𝐶)
7569, 73, 74chvar 2326 . . . . . . . . 9 (𝑧 = ⟨𝑙, 𝑘⟩ → 𝐹 = 𝑙 / 𝑗𝐶)
76 vsnid 4470 . . . . . . . . . . . . . . . . 17 𝑗 ∈ {𝑗}
7776a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝑗 ∈ {𝑗})
78 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝑘𝐵)
7977, 78opelxpd 5441 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → ⟨𝑗, 𝑘⟩ ∈ ({𝑗} × 𝐵))
80 xp2nd 7532 . . . . . . . . . . . . . . . 16 (𝑧 ∈ ({𝑗} × 𝐵) → (2nd𝑧) ∈ 𝐵)
81 xp1st 7531 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) ∈ {𝑗})
82 fvex 6509 . . . . . . . . . . . . . . . . . . . . . 22 (1st𝑧) ∈ V
8382elsn 4450 . . . . . . . . . . . . . . . . . . . . 21 ((1st𝑧) ∈ {𝑗} ↔ (1st𝑧) = 𝑗)
8481, 83sylib 210 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ({𝑗} × 𝐵) → (1st𝑧) = 𝑗)
85 eqop 7541 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ ({𝑗} × 𝐵) → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ ((1st𝑧) = 𝑗 ∧ (2nd𝑧) = 𝑘)))
8684, 85mpbirand 694 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ({𝑗} × 𝐵) → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ (2nd𝑧) = 𝑘))
87 eqcom 2779 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑧) = 𝑘𝑘 = (2nd𝑧))
8886, 87syl6bb 279 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ({𝑗} × 𝐵) → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑘 = (2nd𝑧)))
8988ad2antlr 714 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) → (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑘 = (2nd𝑧)))
9089ralrimiva 3126 . . . . . . . . . . . . . . . 16 (((𝜑𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∀𝑘𝐵 (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑘 = (2nd𝑧)))
91 reu6i 3625 . . . . . . . . . . . . . . . 16 (((2nd𝑧) ∈ 𝐵 ∧ ∀𝑘𝐵 (𝑧 = ⟨𝑗, 𝑘⟩ ↔ 𝑘 = (2nd𝑧))) → ∃!𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
9280, 90, 91syl2an2 673 . . . . . . . . . . . . . . 15 (((𝜑𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃!𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
9379, 92f1mptrn 30156 . . . . . . . . . . . . . 14 ((𝜑𝑗𝐴) → Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩))
9493ex 405 . . . . . . . . . . . . 13 (𝜑 → (𝑗𝐴 → Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩)))
9594sbcimdv 3740 . . . . . . . . . . . 12 (𝜑 → ([𝑙 / 𝑗]𝑗𝐴[𝑙 / 𝑗]Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩)))
96 sbcfung 6209 . . . . . . . . . . . . . 14 (𝑙 ∈ V → ([𝑙 / 𝑗]Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) ↔ Fun 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩)))
97 csbcnv 5600 . . . . . . . . . . . . . . . 16 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩)
98 csbmpt12 5292 . . . . . . . . . . . . . . . . . 18 (𝑙 ∈ V → 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝑗, 𝑘⟩))
99 csbopg 4691 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ V → 𝑙 / 𝑗𝑗, 𝑘⟩ = ⟨𝑙 / 𝑗𝑗, 𝑙 / 𝑗𝑘⟩)
100 csbvarg 4261 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ V → 𝑙 / 𝑗𝑗 = 𝑙)
101 csbconstg 3793 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 ∈ V → 𝑙 / 𝑗𝑘 = 𝑘)
102100, 101opeq12d 4681 . . . . . . . . . . . . . . . . . . . 20 (𝑙 ∈ V → ⟨𝑙 / 𝑗𝑗, 𝑙 / 𝑗𝑘⟩ = ⟨𝑙, 𝑘⟩)
10399, 102eqtrd 2808 . . . . . . . . . . . . . . . . . . 19 (𝑙 ∈ V → 𝑙 / 𝑗𝑗, 𝑘⟩ = ⟨𝑙, 𝑘⟩)
104103mpteq2dv 5019 . . . . . . . . . . . . . . . . . 18 (𝑙 ∈ V → (𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
10598, 104eqtrd 2808 . . . . . . . . . . . . . . . . 17 (𝑙 ∈ V → 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
106105cnveqd 5592 . . . . . . . . . . . . . . . 16 (𝑙 ∈ V → 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
10797, 106syl5eqr 2822 . . . . . . . . . . . . . . 15 (𝑙 ∈ V → 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) = (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
108107funeqd 6207 . . . . . . . . . . . . . 14 (𝑙 ∈ V → (Fun 𝑙 / 𝑗(𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) ↔ Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩)))
10996, 108bitrd 271 . . . . . . . . . . . . 13 (𝑙 ∈ V → ([𝑙 / 𝑗]Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) ↔ Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩)))
11054, 109ax-mp 5 . . . . . . . . . . . 12 ([𝑙 / 𝑗]Fun (𝑘𝐵 ↦ ⟨𝑗, 𝑘⟩) ↔ Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
11195, 50, 1103imtr3g 287 . . . . . . . . . . 11 (𝜑 → (𝑙𝐴 → Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩)))
112111imp 398 . . . . . . . . . 10 ((𝜑𝑙𝐴) → Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
11337, 112syldan 582 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Fun (𝑘𝑙 / 𝑗𝐵 ↦ ⟨𝑙, 𝑘⟩))
114 vsnid 4470 . . . . . . . . . . 11 𝑙 ∈ {𝑙}
115114a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → 𝑙 ∈ {𝑙})
116115, 45opelxpd 5441 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑘𝑙 / 𝑗𝐵) → ⟨𝑙, 𝑘⟩ ∈ ({𝑙} × 𝑙 / 𝑗𝐵))
11765, 66, 61, 75, 42, 113, 59, 116esumc 30983 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 = Σ*𝑧 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩}𝐹)
118 nfab1 2928 . . . . . . . . . 10 𝑡{𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩}
119 nfcv 2926 . . . . . . . . . 10 𝑡({𝑙} × 𝑙 / 𝑗𝐵)
120 opeq1 4673 . . . . . . . . . . . . . 14 (𝑖 = 𝑙 → ⟨𝑖, 𝑘⟩ = ⟨𝑙, 𝑘⟩)
121120eqeq2d 2782 . . . . . . . . . . . . 13 (𝑖 = 𝑙 → (𝑡 = ⟨𝑖, 𝑘⟩ ↔ 𝑡 = ⟨𝑙, 𝑘⟩))
122121rexbidv 3236 . . . . . . . . . . . 12 (𝑖 = 𝑙 → (∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑖, 𝑘⟩ ↔ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩))
12354, 122rexsn 4490 . . . . . . . . . . 11 (∃𝑖 ∈ {𝑙}∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑖, 𝑘⟩ ↔ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩)
124 elxp2 5427 . . . . . . . . . . 11 (𝑡 ∈ ({𝑙} × 𝑙 / 𝑗𝐵) ↔ ∃𝑖 ∈ {𝑙}∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑖, 𝑘⟩)
125 abid 2756 . . . . . . . . . . 11 (𝑡 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩} ↔ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩)
126123, 124, 1253bitr4ri 296 . . . . . . . . . 10 (𝑡 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩} ↔ 𝑡 ∈ ({𝑙} × 𝑙 / 𝑗𝐵))
127118, 119, 126eqri 30026 . . . . . . . . 9 {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩} = ({𝑙} × 𝑙 / 𝑗𝐵)
128 esumeq1 30966 . . . . . . . . 9 ({𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩} = ({𝑙} × 𝑙 / 𝑗𝐵) → Σ*𝑧 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩}𝐹 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹)
129127, 128ax-mp 5 . . . . . . . 8 Σ*𝑧 ∈ {𝑡 ∣ ∃𝑘 𝑙 / 𝑗𝐵𝑡 = ⟨𝑙, 𝑘⟩}𝐹 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹
130117, 129syl6eq 2824 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑘𝑙 / 𝑗𝐵𝑙 / 𝑗𝐶 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹)
13164, 130eqtrd 2808 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹)
132131adantr 473 . . . . 5 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶 = Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹)
13328, 132oveq12d 6992 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → (Σ*𝑗𝑏Σ*𝑘𝐵𝐶 +𝑒 Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶) = (Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 +𝑒 Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹))
134 nfv 1873 . . . . . 6 𝑗(𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏)))
135 nfcv 2926 . . . . . 6 𝑗𝑏
136 nfcv 2926 . . . . . 6 𝑗{𝑙}
137 vex 3412 . . . . . . 7 𝑏 ∈ V
138137a1i 11 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑏 ∈ V)
139 snex 5184 . . . . . . 7 {𝑙} ∈ V
140139a1i 11 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → {𝑙} ∈ V)
14136eldifbd 3836 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ¬ 𝑙𝑏)
142 disjsn 4517 . . . . . . 7 ((𝑏 ∩ {𝑙}) = ∅ ↔ ¬ 𝑙𝑏)
143141, 142sylibr 226 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → (𝑏 ∩ {𝑙}) = ∅)
144 simpll 754 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝜑)
145 simprl 758 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑏𝐴)
146145sselda 3852 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝑗𝐴)
14746anassrs 460 . . . . . . . . 9 (((𝜑𝑗𝐴) ∧ 𝑘𝐵) → 𝐶 ∈ (0[,]+∞))
148147ralrimiva 3126 . . . . . . . 8 ((𝜑𝑗𝐴) → ∀𝑘𝐵 𝐶 ∈ (0[,]+∞))
149 nfcv 2926 . . . . . . . . 9 𝑘𝐵
150149esumcl 30962 . . . . . . . 8 ((𝐵𝑊 ∧ ∀𝑘𝐵 𝐶 ∈ (0[,]+∞)) → Σ*𝑘𝐵𝐶 ∈ (0[,]+∞))
15138, 148, 150syl2anc 576 . . . . . . 7 ((𝜑𝑗𝐴) → Σ*𝑘𝐵𝐶 ∈ (0[,]+∞))
152144, 146, 151syl2anc 576 . . . . . 6 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → Σ*𝑘𝐵𝐶 ∈ (0[,]+∞))
153 simpll 754 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗 ∈ {𝑙}) → 𝜑)
15437snssd 4612 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → {𝑙} ⊆ 𝐴)
155154sselda 3852 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗 ∈ {𝑙}) → 𝑗𝐴)
156153, 155, 151syl2anc 576 . . . . . 6 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗 ∈ {𝑙}) → Σ*𝑘𝐵𝐶 ∈ (0[,]+∞))
157134, 135, 136, 138, 140, 143, 152, 156esumsplit 30985 . . . . 5 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = (Σ*𝑗𝑏Σ*𝑘𝐵𝐶 +𝑒 Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶))
158157adantr 473 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = (Σ*𝑗𝑏Σ*𝑘𝐵𝐶 +𝑒 Σ*𝑗 ∈ {𝑙*𝑘𝐵𝐶))
159 iunxun 4878 . . . . . . . 8 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑙} ({𝑗} × 𝐵))
160136, 29nfxp 5436 . . . . . . . . . . 11 𝑗({𝑙} × 𝑙 / 𝑗𝐵)
161 sneq 4445 . . . . . . . . . . . 12 (𝑗 = 𝑙 → {𝑗} = {𝑙})
162161, 32xpeq12d 5434 . . . . . . . . . . 11 (𝑗 = 𝑙 → ({𝑗} × 𝐵) = ({𝑙} × 𝑙 / 𝑗𝐵))
163160, 162iunxsngf 4876 . . . . . . . . . 10 (𝑙 ∈ V → 𝑗 ∈ {𝑙} ({𝑗} × 𝐵) = ({𝑙} × 𝑙 / 𝑗𝐵))
16454, 163ax-mp 5 . . . . . . . . 9 𝑗 ∈ {𝑙} ({𝑗} × 𝐵) = ({𝑙} × 𝑙 / 𝑗𝐵)
165164uneq2i 4019 . . . . . . . 8 ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ 𝑗 ∈ {𝑙} ({𝑗} × 𝐵)) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))
166159, 165eqtri 2796 . . . . . . 7 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))
167 esumeq1 30966 . . . . . . 7 ( 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵)) → Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹 = Σ*𝑧 ∈ ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))𝐹)
168166, 167ax-mp 5 . . . . . 6 Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹 = Σ*𝑧 ∈ ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))𝐹
169 nfv 1873 . . . . . . 7 𝑧(𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏)))
170 nfcv 2926 . . . . . . 7 𝑧 𝑗𝑏 ({𝑗} × 𝐵)
171 nfcv 2926 . . . . . . 7 𝑧({𝑙} × 𝑙 / 𝑗𝐵)
172 snex 5184 . . . . . . . . . 10 {𝑗} ∈ V
173146, 39syldan 582 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝐵𝑊)
174 xpexg 7288 . . . . . . . . . 10 (({𝑗} ∈ V ∧ 𝐵𝑊) → ({𝑗} × 𝐵) ∈ V)
175172, 173, 174sylancr 578 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → ({𝑗} × 𝐵) ∈ V)
176175ralrimiva 3126 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ∀𝑗𝑏 ({𝑗} × 𝐵) ∈ V)
177 iunexg 7474 . . . . . . . 8 ((𝑏 ∈ V ∧ ∀𝑗𝑏 ({𝑗} × 𝐵) ∈ V) → 𝑗𝑏 ({𝑗} × 𝐵) ∈ V)
178137, 176, 177sylancr 578 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑗𝑏 ({𝑗} × 𝐵) ∈ V)
179 xpexg 7288 . . . . . . . 8 (({𝑙} ∈ V ∧ 𝑙 / 𝑗𝐵𝑊) → ({𝑙} × 𝑙 / 𝑗𝐵) ∈ V)
180139, 42, 179sylancr 578 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ({𝑙} × 𝑙 / 𝑗𝐵) ∈ V)
181 simpr 477 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝑗𝑏)
182141adantr 473 . . . . . . . . . . 11 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → ¬ 𝑙𝑏)
183 nelne2 3060 . . . . . . . . . . 11 ((𝑗𝑏 ∧ ¬ 𝑙𝑏) → 𝑗𝑙)
184181, 182, 183syl2anc 576 . . . . . . . . . 10 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → 𝑗𝑙)
185 disjsn2 4518 . . . . . . . . . 10 (𝑗𝑙 → ({𝑗} ∩ {𝑙}) = ∅)
186 xpdisj1 5855 . . . . . . . . . 10 (({𝑗} ∩ {𝑙}) = ∅ → (({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = ∅)
187184, 185, 1863syl 18 . . . . . . . . 9 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑗𝑏) → (({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = ∅)
188187iuneq2dv 4811 . . . . . . . 8 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑗𝑏 (({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = 𝑗𝑏 ∅)
189160iunin1f 30092 . . . . . . . 8 𝑗𝑏 (({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = ( 𝑗𝑏 ({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵))
190 iun0 4847 . . . . . . . 8 𝑗𝑏 ∅ = ∅
191188, 189, 1903eqtr3g 2831 . . . . . . 7 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ( 𝑗𝑏 ({𝑗} × 𝐵) ∩ ({𝑙} × 𝑙 / 𝑗𝐵)) = ∅)
192 simpll 754 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 𝑗𝑏 ({𝑗} × 𝐵)) → 𝜑)
193 iunss1 4801 . . . . . . . . . 10 (𝑏𝐴 𝑗𝑏 ({𝑗} × 𝐵) ⊆ 𝑗𝐴 ({𝑗} × 𝐵))
194145, 193syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → 𝑗𝑏 ({𝑗} × 𝐵) ⊆ 𝑗𝐴 ({𝑗} × 𝐵))
195194sselda 3852 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 𝑗𝑏 ({𝑗} × 𝐵)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐵))
196 nfv 1873 . . . . . . . . . 10 𝑗𝜑
197 nfiu1 4819 . . . . . . . . . . 11 𝑗 𝑗𝐴 ({𝑗} × 𝐵)
198197nfcri 2920 . . . . . . . . . 10 𝑗 𝑧 𝑗𝐴 ({𝑗} × 𝐵)
199196, 198nfan 1862 . . . . . . . . 9 𝑗(𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵))
200 nfv 1873 . . . . . . . . . 10 𝑘(((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵))
201 nfcv 2926 . . . . . . . . . . 11 𝑘(0[,]+∞)
20265, 201nfel 2938 . . . . . . . . . 10 𝑘 𝐹 ∈ (0[,]+∞)
20374adantl 474 . . . . . . . . . . 11 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐹 = 𝐶)
204 simp-5l 772 . . . . . . . . . . . 12 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝜑)
205 simp-4r 771 . . . . . . . . . . . 12 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝑗𝐴)
206 simplr 756 . . . . . . . . . . . 12 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝑘𝐵)
207204, 205, 206, 46syl12anc 824 . . . . . . . . . . 11 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐶 ∈ (0[,]+∞))
208203, 207eqeltrd 2860 . . . . . . . . . 10 ((((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘𝐵) ∧ 𝑧 = ⟨𝑗, 𝑘⟩) → 𝐹 ∈ (0[,]+∞))
209 elsnxp 5977 . . . . . . . . . . . 12 (𝑗𝐴 → (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩))
210209biimpa 469 . . . . . . . . . . 11 ((𝑗𝐴𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
211210adantll 701 . . . . . . . . . 10 ((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘𝐵 𝑧 = ⟨𝑗, 𝑘⟩)
212200, 202, 208, 211r19.29af2 3265 . . . . . . . . 9 ((((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) ∧ 𝑗𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
213 simpr 477 . . . . . . . . . 10 ((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐵))
214 eliun 4792 . . . . . . . . . 10 (𝑧 𝑗𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗𝐴 𝑧 ∈ ({𝑗} × 𝐵))
215213, 214sylib 210 . . . . . . . . 9 ((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) → ∃𝑗𝐴 𝑧 ∈ ({𝑗} × 𝐵))
216199, 212, 215r19.29af 3266 . . . . . . . 8 ((𝜑𝑧 𝑗𝐴 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
217192, 195, 216syl2anc 576 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 𝑗𝑏 ({𝑗} × 𝐵)) → 𝐹 ∈ (0[,]+∞))
218 simpll 754 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)) → 𝜑)
219 nfcv 2926 . . . . . . . . . . 11 𝑗𝐴
220 nfcv 2926 . . . . . . . . . . 11 𝑗𝑙
221219, 220, 160, 162ssiun2sf 30094 . . . . . . . . . 10 (𝑙𝐴 → ({𝑙} × 𝑙 / 𝑗𝐵) ⊆ 𝑗𝐴 ({𝑗} × 𝐵))
22237, 221syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → ({𝑙} × 𝑙 / 𝑗𝐵) ⊆ 𝑗𝐴 ({𝑗} × 𝐵))
223222sselda 3852 . . . . . . . 8 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)) → 𝑧 𝑗𝐴 ({𝑗} × 𝐵))
224218, 223, 216syl2anc 576 . . . . . . 7 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ 𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)) → 𝐹 ∈ (0[,]+∞))
225169, 170, 171, 178, 180, 191, 217, 224esumsplit 30985 . . . . . 6 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑧 ∈ ( 𝑗𝑏 ({𝑗} × 𝐵) ∪ ({𝑙} × 𝑙 / 𝑗𝐵))𝐹 = (Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 +𝑒 Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹))
226168, 225syl5eq 2820 . . . . 5 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹 = (Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 +𝑒 Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹))
227226adantr 473 . . . 4 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹 = (Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 +𝑒 Σ*𝑧 ∈ ({𝑙} × 𝑙 / 𝑗𝐵)𝐹))
228133, 158, 2273eqtr4d 2818 . . 3 (((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) ∧ Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹) → Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹)
229228ex 405 . 2 ((𝜑 ∧ (𝑏𝐴𝑙 ∈ (𝐴𝑏))) → (Σ*𝑗𝑏Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝑏 ({𝑗} × 𝐵)𝐹 → Σ*𝑗 ∈ (𝑏 ∪ {𝑙})Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗 ∈ (𝑏 ∪ {𝑙})({𝑗} × 𝐵)𝐹))
230 esum2dlem.e . 2 (𝜑𝐴 ∈ Fin)
2315, 10, 15, 20, 27, 229, 230findcard2d 8553 1 (𝜑 → Σ*𝑗𝐴Σ*𝑘𝐵𝐶 = Σ*𝑧 𝑗𝐴 ({𝑗} × 𝐵)𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  {cab 2752  wnfc 2910  wne 2961  wral 3082  wrex 3083  ∃!wreu 3084  Vcvv 3409  [wsbc 3675  csb 3780  cdif 3820  cun 3821  cin 3822  wss 3823  c0 4172  {csn 4435  cop 4441   ciun 4788  cmpt 5004   × cxp 5401  ccnv 5402  Fun wfun 6179  cfv 6185  (class class class)co 6974  1st c1st 7497  2nd c2nd 7498  Fincfn 8304  0cc0 10333  +∞cpnf 10469   +𝑒 cxad 12320  [,]cicc 12555  Σ*cesum 30959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-inf2 8896  ax-cnex 10389  ax-resscn 10390  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-addrcl 10394  ax-mulcl 10395  ax-mulrcl 10396  ax-mulcom 10397  ax-addass 10398  ax-mulass 10399  ax-distr 10400  ax-i2m1 10401  ax-1ne0 10402  ax-1rid 10403  ax-rnegex 10404  ax-rrecex 10405  ax-cnre 10406  ax-pre-lttri 10407  ax-pre-lttrn 10408  ax-pre-ltadd 10409  ax-pre-mulgt0 10410  ax-pre-sup 10411  ax-addf 10412  ax-mulf 10413
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-int 4746  df-iun 4790  df-iin 4791  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-se 5363  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-isom 6194  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-of 7225  df-om 7395  df-1st 7499  df-2nd 7500  df-supp 7632  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-1o 7903  df-2o 7904  df-oadd 7907  df-er 8087  df-map 8206  df-pm 8207  df-ixp 8258  df-en 8305  df-dom 8306  df-sdom 8307  df-fin 8308  df-fsupp 8627  df-fi 8668  df-sup 8699  df-inf 8700  df-oi 8767  df-card 9160  df-cda 9386  df-pnf 10474  df-mnf 10475  df-xr 10476  df-ltxr 10477  df-le 10478  df-sub 10670  df-neg 10671  df-div 11097  df-nn 11438  df-2 11501  df-3 11502  df-4 11503  df-5 11504  df-6 11505  df-7 11506  df-8 11507  df-9 11508  df-n0 11706  df-z 11792  df-dec 11910  df-uz 12057  df-q 12161  df-rp 12203  df-xneg 12322  df-xadd 12323  df-xmul 12324  df-ioo 12556  df-ioc 12557  df-ico 12558  df-icc 12559  df-fz 12707  df-fzo 12848  df-fl 12975  df-mod 13051  df-seq 13183  df-exp 13243  df-fac 13447  df-bc 13476  df-hash 13504  df-shft 14285  df-cj 14317  df-re 14318  df-im 14319  df-sqrt 14453  df-abs 14454  df-limsup 14687  df-clim 14704  df-rlim 14705  df-sum 14902  df-ef 15279  df-sin 15281  df-cos 15282  df-pi 15284  df-struct 16339  df-ndx 16340  df-slot 16341  df-base 16343  df-sets 16344  df-ress 16345  df-plusg 16432  df-mulr 16433  df-starv 16434  df-sca 16435  df-vsca 16436  df-ip 16437  df-tset 16438  df-ple 16439  df-ds 16441  df-unif 16442  df-hom 16443  df-cco 16444  df-rest 16550  df-topn 16551  df-0g 16569  df-gsum 16570  df-topgen 16571  df-pt 16572  df-prds 16575  df-ordt 16628  df-xrs 16629  df-qtop 16634  df-imas 16635  df-xps 16637  df-mre 16727  df-mrc 16728  df-acs 16730  df-ps 17680  df-tsr 17681  df-plusf 17721  df-mgm 17722  df-sgrp 17764  df-mnd 17775  df-mhm 17815  df-submnd 17816  df-grp 17906  df-minusg 17907  df-sbg 17908  df-mulg 18024  df-subg 18072  df-cntz 18230  df-cmn 18680  df-abl 18681  df-mgp 18975  df-ur 18987  df-ring 19034  df-cring 19035  df-subrg 19268  df-abv 19322  df-lmod 19370  df-scaf 19371  df-sra 19678  df-rgmod 19679  df-psmet 20251  df-xmet 20252  df-met 20253  df-bl 20254  df-mopn 20255  df-fbas 20256  df-fg 20257  df-cnfld 20260  df-top 21218  df-topon 21235  df-topsp 21257  df-bases 21270  df-cld 21343  df-ntr 21344  df-cls 21345  df-nei 21422  df-lp 21460  df-perf 21461  df-cn 21551  df-cnp 21552  df-haus 21639  df-tx 21886  df-hmeo 22079  df-fil 22170  df-fm 22262  df-flim 22263  df-flf 22264  df-tmd 22396  df-tgp 22397  df-tsms 22450  df-trg 22483  df-xms 22645  df-ms 22646  df-tms 22647  df-nm 22907  df-ngp 22908  df-nrg 22910  df-nlm 22911  df-ii 23200  df-cncf 23201  df-limc 24179  df-dv 24180  df-log 24853  df-esum 30960
This theorem is referenced by:  esum2d  31025
  Copyright terms: Public domain W3C validator