Proof of Theorem itg1addlem2
Step | Hyp | Ref
| Expression |
1 | | iffalse 4095 |
. . . . . . . 8
⊢ (¬
(𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) |
2 | 1 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ ¬ (𝑖 = 0 ∧ 𝑗 = 0)) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) |
3 | | i1fadd.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
4 | | i1fima 23445 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {𝑖}) ∈ dom vol) |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ {𝑖}) ∈ dom vol) |
6 | | i1fadd.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ dom
∫1) |
7 | | i1fima 23445 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ dom ∫1
→ (◡𝐺 “ {𝑗}) ∈ dom vol) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐺 “ {𝑗}) ∈ dom vol) |
9 | | inmbl 23310 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑖}) ∈ dom vol ∧ (◡𝐺 “ {𝑗}) ∈ dom vol) → ((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ∈ dom vol) |
10 | 5, 8, 9 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ∈ dom vol) |
11 | 10 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ ¬ (𝑖 = 0 ∧ 𝑗 = 0)) → ((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ∈ dom vol) |
12 | | mblvol 23298 |
. . . . . . . 8
⊢ (((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ∈ dom vol → (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))) = (vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ ¬ (𝑖 = 0 ∧ 𝑗 = 0)) → (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))) = (vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) |
14 | 2, 13 | eqtrd 2656 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ ¬ (𝑖 = 0 ∧ 𝑗 = 0)) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = (vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) |
15 | | neorian 2888 |
. . . . . . 7
⊢ ((𝑖 ≠ 0 ∨ 𝑗 ≠ 0) ↔ ¬ (𝑖 = 0 ∧ 𝑗 = 0)) |
16 | | inss1 3833 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ⊆ (◡𝐹 “ {𝑖}) |
17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → ((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ⊆ (◡𝐹 “ {𝑖})) |
18 | 5 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → (◡𝐹 “ {𝑖}) ∈ dom vol) |
19 | | mblss 23299 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑖}) ∈ dom vol → (◡𝐹 “ {𝑖}) ⊆ ℝ) |
20 | 18, 19 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → (◡𝐹 “ {𝑖}) ⊆ ℝ) |
21 | | mblvol 23298 |
. . . . . . . . . . 11
⊢ ((◡𝐹 “ {𝑖}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑖})) = (vol*‘(◡𝐹 “ {𝑖}))) |
22 | 18, 21 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → (vol‘(◡𝐹 “ {𝑖})) = (vol*‘(◡𝐹 “ {𝑖}))) |
23 | 3 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → 𝐹 ∈ dom
∫1) |
24 | | simplrl 800 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → 𝑖 ∈ ℝ) |
25 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → 𝑖 ≠ 0) |
26 | | eldifsn 4317 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (ℝ ∖ {0})
↔ (𝑖 ∈ ℝ
∧ 𝑖 ≠
0)) |
27 | 24, 25, 26 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → 𝑖 ∈ (ℝ ∖
{0})) |
28 | | i1fima2sn 23447 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑖 ∈ (ℝ
∖ {0})) → (vol‘(◡𝐹 “ {𝑖})) ∈ ℝ) |
29 | 23, 27, 28 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → (vol‘(◡𝐹 “ {𝑖})) ∈ ℝ) |
30 | 22, 29 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → (vol*‘(◡𝐹 “ {𝑖})) ∈ ℝ) |
31 | | ovolsscl 23254 |
. . . . . . . . 9
⊢ ((((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ⊆ (◡𝐹 “ {𝑖}) ∧ (◡𝐹 “ {𝑖}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑖})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))) ∈ ℝ) |
32 | 17, 20, 30, 31 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑖 ≠ 0) → (vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))) ∈ ℝ) |
33 | | inss2 3834 |
. . . . . . . . . 10
⊢ ((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ⊆ (◡𝐺 “ {𝑗}) |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → ((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ⊆ (◡𝐺 “ {𝑗})) |
35 | 6 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → 𝐺 ∈ dom
∫1) |
36 | 35, 7 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (◡𝐺 “ {𝑗}) ∈ dom vol) |
37 | 36 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → (◡𝐺 “ {𝑗}) ∈ dom vol) |
38 | | mblss 23299 |
. . . . . . . . . 10
⊢ ((◡𝐺 “ {𝑗}) ∈ dom vol → (◡𝐺 “ {𝑗}) ⊆ ℝ) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → (◡𝐺 “ {𝑗}) ⊆ ℝ) |
40 | | mblvol 23298 |
. . . . . . . . . . 11
⊢ ((◡𝐺 “ {𝑗}) ∈ dom vol → (vol‘(◡𝐺 “ {𝑗})) = (vol*‘(◡𝐺 “ {𝑗}))) |
41 | 37, 40 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → (vol‘(◡𝐺 “ {𝑗})) = (vol*‘(◡𝐺 “ {𝑗}))) |
42 | 6 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → 𝐺 ∈ dom
∫1) |
43 | | simplrr 801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → 𝑗 ∈ ℝ) |
44 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → 𝑗 ≠ 0) |
45 | | eldifsn 4317 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (ℝ ∖ {0})
↔ (𝑗 ∈ ℝ
∧ 𝑗 ≠
0)) |
46 | 43, 44, 45 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → 𝑗 ∈ (ℝ ∖
{0})) |
47 | | i1fima2sn 23447 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ dom ∫1
∧ 𝑗 ∈ (ℝ
∖ {0})) → (vol‘(◡𝐺 “ {𝑗})) ∈ ℝ) |
48 | 42, 46, 47 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → (vol‘(◡𝐺 “ {𝑗})) ∈ ℝ) |
49 | 41, 48 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → (vol*‘(◡𝐺 “ {𝑗})) ∈ ℝ) |
50 | | ovolsscl 23254 |
. . . . . . . . 9
⊢ ((((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})) ⊆ (◡𝐺 “ {𝑗}) ∧ (◡𝐺 “ {𝑗}) ⊆ ℝ ∧ (vol*‘(◡𝐺 “ {𝑗})) ∈ ℝ) →
(vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))) ∈ ℝ) |
51 | 34, 39, 49, 50 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ 𝑗 ≠ 0) → (vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))) ∈ ℝ) |
52 | 32, 51 | jaodan 826 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ (𝑖 ≠ 0 ∨ 𝑗 ≠ 0)) → (vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))) ∈ ℝ) |
53 | 15, 52 | sylan2br 493 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ ¬ (𝑖 = 0 ∧ 𝑗 = 0)) → (vol*‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))) ∈ ℝ) |
54 | 14, 53 | eqeltrd 2701 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) ∧ ¬ (𝑖 = 0 ∧ 𝑗 = 0)) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) ∈ ℝ) |
55 | 54 | ex 450 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → (¬ (𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) ∈ ℝ)) |
56 | | iftrue 4092 |
. . . . 5
⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) = 0) |
57 | | 0re 10040 |
. . . . 5
⊢ 0 ∈
ℝ |
58 | 56, 57 | syl6eqel 2709 |
. . . 4
⊢ ((𝑖 = 0 ∧ 𝑗 = 0) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) ∈ ℝ) |
59 | 55, 58 | pm2.61d2 172 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ)) → if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) ∈ ℝ) |
60 | 59 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ ℝ ∀𝑗 ∈ ℝ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) ∈ ℝ) |
61 | | itg1add.3 |
. . 3
⊢ 𝐼 = (𝑖 ∈ ℝ, 𝑗 ∈ ℝ ↦ if((𝑖 = 0 ∧ 𝑗 = 0), 0, (vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗}))))) |
62 | 61 | fmpt2 7237 |
. 2
⊢
(∀𝑖 ∈
ℝ ∀𝑗 ∈
ℝ if((𝑖 = 0 ∧
𝑗 = 0), 0,
(vol‘((◡𝐹 “ {𝑖}) ∩ (◡𝐺 “ {𝑗})))) ∈ ℝ ↔ 𝐼:(ℝ ×
ℝ)⟶ℝ) |
63 | 60, 62 | sylib 208 |
1
⊢ (𝜑 → 𝐼:(ℝ ×
ℝ)⟶ℝ) |