Step | Hyp | Ref
| Expression |
1 | | reex 10719 |
. . . . 5
⊢ ℝ
∈ V |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → ℝ ∈
V) |
3 | | i1fmulc.2 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
4 | | i1ff 24441 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
6 | 5 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐹:ℝ⟶ℝ) |
7 | | i1fmulc.3 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
8 | 7 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐴 ∈ ℝ) |
9 | | 0red 10735 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 0 ∈
ℝ) |
10 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → 𝐴 = 0) |
11 | 10 | oveq1d 7198 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = (0 · 𝑥)) |
12 | | mul02lem2 10908 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (0
· 𝑥) =
0) |
13 | 12 | adantl 485 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0) |
14 | 11, 13 | eqtrd 2774 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = 0) |
15 | 2, 6, 8, 9, 14 | caofid2 7471 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) = (ℝ ×
{0})) |
16 | | i1f0 24452 |
. . 3
⊢ (ℝ
× {0}) ∈ dom ∫1 |
17 | 15, 16 | eqeltrdi 2842 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) ∈ dom
∫1) |
18 | | remulcl 10713 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
19 | 18 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
20 | | fconst6g 6578 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (ℝ
× {𝐴}):ℝ⟶ℝ) |
21 | 7, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶ℝ) |
22 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈
V) |
23 | | inidm 4119 |
. . . . 5
⊢ (ℝ
∩ ℝ) = ℝ |
24 | 19, 21, 5, 22, 22, 23 | off 7455 |
. . . 4
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶ℝ) |
25 | 24 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶ℝ) |
26 | | i1frn 24442 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
27 | 3, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
28 | | ovex 7216 |
. . . . . . . 8
⊢ (𝐴 · 𝑦) ∈ V |
29 | | eqid 2739 |
. . . . . . . 8
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) |
30 | 28, 29 | fnmpti 6491 |
. . . . . . 7
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) Fn ran 𝐹 |
31 | | dffn4 6609 |
. . . . . . 7
⊢ ((𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) Fn ran 𝐹 ↔ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) |
32 | 30, 31 | mpbi 233 |
. . . . . 6
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) |
33 | | fofi 8896 |
. . . . . 6
⊢ ((ran
𝐹 ∈ Fin ∧ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) → ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) ∈ Fin) |
34 | 27, 32, 33 | sylancl 589 |
. . . . 5
⊢ (𝜑 → ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) ∈ Fin) |
35 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ran 𝐹 → 𝑤 ∈ ran 𝐹) |
36 | | elsni 4543 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝐴} → 𝑥 = 𝐴) |
37 | 36 | oveq1d 7198 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝐴} → (𝑥 · 𝑤) = (𝐴 · 𝑤)) |
38 | | oveq2 7191 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
39 | 38 | rspceeqv 3544 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ran 𝐹 ∧ (𝑥 · 𝑤) = (𝐴 · 𝑤)) → ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) |
40 | 35, 37, 39 | syl2anr 600 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹) → ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) |
41 | | ovex 7216 |
. . . . . . . . . . 11
⊢ (𝑥 · 𝑤) ∈ V |
42 | | eqeq1 2743 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 · 𝑤) → (𝑧 = (𝐴 · 𝑦) ↔ (𝑥 · 𝑤) = (𝐴 · 𝑦))) |
43 | 42 | rexbidv 3208 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑥 · 𝑤) → (∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦) ↔ ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦))) |
44 | 41, 43 | elab 3578 |
. . . . . . . . . 10
⊢ ((𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)} ↔ ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) |
45 | 40, 44 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹) → (𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
46 | 45 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹)) → (𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
47 | | fconstg 6576 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (ℝ
× {𝐴}):ℝ⟶{𝐴}) |
48 | 7, 47 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶{𝐴}) |
49 | 5 | ffnd 6516 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn ℝ) |
50 | | dffn3 6528 |
. . . . . . . . 9
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
51 | 49, 50 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
52 | 46, 48, 51, 22, 22, 23 | off 7455 |
. . . . . . 7
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹):ℝ⟶{𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
53 | 52 | frnd 6523 |
. . . . . 6
⊢ (𝜑 → ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ⊆ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
54 | 29 | rnmpt 5808 |
. . . . . 6
⊢ ran
(𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) = {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)} |
55 | 53, 54 | sseqtrrdi 3938 |
. . . . 5
⊢ (𝜑 → ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ⊆ ran
(𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) |
56 | 34, 55 | ssfid 8832 |
. . . 4
⊢ (𝜑 → ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∈
Fin) |
57 | 56 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∈
Fin) |
58 | 24 | frnd 6523 |
. . . . . . . 8
⊢ (𝜑 → ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ⊆
ℝ) |
59 | 58 | ssdifssd 4043 |
. . . . . . 7
⊢ (𝜑 → (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
⊆ ℝ) |
60 | 59 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
⊆ ℝ) |
61 | 60 | sselda 3887 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑦 ∈
ℝ) |
62 | 3, 7 | i1fmulclem 24468 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑦}) = (◡𝐹 “ {(𝑦 / 𝐴)})) |
63 | 61, 62 | syldan 594 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑦}) = (◡𝐹 “ {(𝑦 / 𝐴)})) |
64 | | i1fima 24443 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) |
65 | 3, 64 | syl 17 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) |
66 | 65 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) |
67 | 63, 66 | eqeltrd 2834 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(◡((ℝ × {𝐴}) ∘f · 𝐹) “ {𝑦}) ∈ dom vol) |
68 | 63 | fveq2d 6691 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡((ℝ × {𝐴}) ∘f ·
𝐹) “ {𝑦})) = (vol‘(◡𝐹 “ {(𝑦 / 𝐴)}))) |
69 | 3 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐹 ∈ dom
∫1) |
70 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ∈
ℝ) |
71 | | simplr 769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ≠ 0) |
72 | 61, 70, 71 | redivcld 11559 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑦 / 𝐴) ∈ ℝ) |
73 | 61 | recnd 10760 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑦 ∈
ℂ) |
74 | 70 | recnd 10760 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝐴 ∈
ℂ) |
75 | | eldifsni 4688 |
. . . . . . . 8
⊢ (𝑦 ∈ (ran ((ℝ ×
{𝐴}) ∘f
· 𝐹) ∖ {0})
→ 𝑦 ≠
0) |
76 | 75 | adantl 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
𝑦 ≠ 0) |
77 | 73, 74, 76, 71 | divne0d 11523 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑦 / 𝐴) ≠ 0) |
78 | | eldifsn 4685 |
. . . . . 6
⊢ ((𝑦 / 𝐴) ∈ (ℝ ∖ {0}) ↔
((𝑦 / 𝐴) ∈ ℝ ∧ (𝑦 / 𝐴) ≠ 0)) |
79 | 72, 77, 78 | sylanbrc 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(𝑦 / 𝐴) ∈ (ℝ ∖
{0})) |
80 | | i1fima2sn 24445 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ (𝑦 / 𝐴) ∈ (ℝ ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑦 / 𝐴)})) ∈ ℝ) |
81 | 69, 79, 80 | syl2anc 587 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡𝐹 “ {(𝑦 / 𝐴)})) ∈ ℝ) |
82 | 68, 81 | eqeltrd 2834 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘f ·
𝐹) ∖ {0})) →
(vol‘(◡((ℝ × {𝐴}) ∘f ·
𝐹) “ {𝑦})) ∈
ℝ) |
83 | 25, 57, 67, 82 | i1fd 24446 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘f ·
𝐹) ∈ dom
∫1) |
84 | 17, 83 | pm2.61dane 3022 |
1
⊢ (𝜑 → ((ℝ × {𝐴}) ∘f ·
𝐹) ∈ dom
∫1) |