Step | Hyp | Ref
| Expression |
1 | | reex 10027 |
. . . . 5
⊢ ℝ
∈ V |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → ℝ ∈
V) |
3 | | i1fmulc.2 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
4 | | i1ff 23443 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
6 | 5 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐹:ℝ⟶ℝ) |
7 | | i1fmulc.3 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
8 | 7 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝐴 ∈ ℝ) |
9 | | 0red 10041 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0) → 0 ∈
ℝ) |
10 | | simplr 792 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → 𝐴 = 0) |
11 | 10 | oveq1d 6665 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = (0 · 𝑥)) |
12 | | mul02lem2 10213 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → (0
· 𝑥) =
0) |
13 | 12 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0) |
14 | 11, 13 | eqtrd 2656 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 = 0) ∧ 𝑥 ∈ ℝ) → (𝐴 · 𝑥) = 0) |
15 | 2, 6, 8, 9, 14 | caofid2 6928 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 0) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹) = (ℝ
× {0})) |
16 | | i1f0 23454 |
. . 3
⊢ (ℝ
× {0}) ∈ dom ∫1 |
17 | 15, 16 | syl6eqel 2709 |
. 2
⊢ ((𝜑 ∧ 𝐴 = 0) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∈ dom
∫1) |
18 | | remulcl 10021 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
19 | 18 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
20 | | fconst6g 6094 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (ℝ
× {𝐴}):ℝ⟶ℝ) |
21 | 7, 20 | syl 17 |
. . . . 5
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶ℝ) |
22 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ ∈
V) |
23 | | inidm 3822 |
. . . . 5
⊢ (ℝ
∩ ℝ) = ℝ |
24 | 19, 21, 5, 22, 22, 23 | off 6912 |
. . . 4
⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓
· 𝐹):ℝ⟶ℝ) |
25 | 24 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹):ℝ⟶ℝ) |
26 | | i1frn 23444 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ ran 𝐹 ∈
Fin) |
27 | 3, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
28 | | ovex 6678 |
. . . . . . . 8
⊢ (𝐴 · 𝑦) ∈ V |
29 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) = (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) |
30 | 28, 29 | fnmpti 6022 |
. . . . . . 7
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) Fn ran 𝐹 |
31 | | dffn4 6121 |
. . . . . . 7
⊢ ((𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) Fn ran 𝐹 ↔ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) |
32 | 30, 31 | mpbi 220 |
. . . . . 6
⊢ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) |
33 | | fofi 8252 |
. . . . . 6
⊢ ((ran
𝐹 ∈ Fin ∧ (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)):ran 𝐹–onto→ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) → ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) ∈ Fin) |
34 | 27, 32, 33 | sylancl 694 |
. . . . 5
⊢ (𝜑 → ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) ∈ Fin) |
35 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ran 𝐹 → 𝑤 ∈ ran 𝐹) |
36 | | elsni 4194 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝐴} → 𝑥 = 𝐴) |
37 | 36 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝐴} → (𝑥 · 𝑤) = (𝐴 · 𝑤)) |
38 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑤 → (𝐴 · 𝑦) = (𝐴 · 𝑤)) |
39 | 38 | eqeq2d 2632 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → ((𝑥 · 𝑤) = (𝐴 · 𝑦) ↔ (𝑥 · 𝑤) = (𝐴 · 𝑤))) |
40 | 39 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ ran 𝐹 ∧ (𝑥 · 𝑤) = (𝐴 · 𝑤)) → ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) |
41 | 35, 37, 40 | syl2anr 495 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹) → ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) |
42 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑥 · 𝑤) ∈ V |
43 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 · 𝑤) → (𝑧 = (𝐴 · 𝑦) ↔ (𝑥 · 𝑤) = (𝐴 · 𝑦))) |
44 | 43 | rexbidv 3052 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑥 · 𝑤) → (∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦) ↔ ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦))) |
45 | 42, 44 | elab 3350 |
. . . . . . . . . 10
⊢ ((𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)} ↔ ∃𝑦 ∈ ran 𝐹(𝑥 · 𝑤) = (𝐴 · 𝑦)) |
46 | 41, 45 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹) → (𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
47 | 46 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ {𝐴} ∧ 𝑤 ∈ ran 𝐹)) → (𝑥 · 𝑤) ∈ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
48 | | fconstg 6092 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (ℝ
× {𝐴}):ℝ⟶{𝐴}) |
49 | 7, 48 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶{𝐴}) |
50 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
51 | 5, 50 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn ℝ) |
52 | | dffn3 6054 |
. . . . . . . . 9
⊢ (𝐹 Fn ℝ ↔ 𝐹:ℝ⟶ran 𝐹) |
53 | 51, 52 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℝ⟶ran 𝐹) |
54 | 47, 49, 53, 22, 22, 23 | off 6912 |
. . . . . . 7
⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓
· 𝐹):ℝ⟶{𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
55 | | frn 6053 |
. . . . . . 7
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹):ℝ⟶{𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)} → ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ⊆ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
56 | 54, 55 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ⊆ {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)}) |
57 | 29 | rnmpt 5371 |
. . . . . 6
⊢ ran
(𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) = {𝑧 ∣ ∃𝑦 ∈ ran 𝐹 𝑧 = (𝐴 · 𝑦)} |
58 | 56, 57 | syl6sseqr 3652 |
. . . . 5
⊢ (𝜑 → ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ⊆ ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) |
59 | | ssfi 8180 |
. . . . 5
⊢ ((ran
(𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦)) ∈ Fin ∧ ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ⊆ ran (𝑦 ∈ ran 𝐹 ↦ (𝐴 · 𝑦))) → ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∈
Fin) |
60 | 34, 58, 59 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∈ Fin) |
61 | 60 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∈
Fin) |
62 | | frn 6053 |
. . . . . . . . 9
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹):ℝ⟶ℝ
→ ran ((ℝ × {𝐴}) ∘𝑓 ·
𝐹) ⊆
ℝ) |
63 | 24, 62 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ⊆ ℝ) |
64 | 63 | ssdifssd 3748 |
. . . . . . 7
⊢ (𝜑 → (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) ⊆
ℝ) |
65 | 64 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) ⊆
ℝ) |
66 | 65 | sselda 3603 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑦 ∈
ℝ) |
67 | 3, 7 | i1fmulclem 23469 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝑦}) = (◡𝐹 “ {(𝑦 / 𝐴)})) |
68 | 66, 67 | syldan 487 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (◡((ℝ × {𝐴}) ∘𝑓
· 𝐹) “ {𝑦}) = (◡𝐹 “ {(𝑦 / 𝐴)})) |
69 | | i1fima 23445 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) |
70 | 3, 69 | syl 17 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) |
71 | 70 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (◡𝐹 “ {(𝑦 / 𝐴)}) ∈ dom vol) |
72 | 68, 71 | eqeltrd 2701 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (◡((ℝ × {𝐴}) ∘𝑓
· 𝐹) “ {𝑦}) ∈ dom
vol) |
73 | 68 | fveq2d 6195 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (vol‘(◡((ℝ ×
{𝐴})
∘𝑓 · 𝐹) “ {𝑦})) = (vol‘(◡𝐹 “ {(𝑦 / 𝐴)}))) |
74 | 3 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐹 ∈ dom
∫1) |
75 | 7 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ∈
ℝ) |
76 | | simplr 792 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ≠
0) |
77 | 66, 75, 76 | redivcld 10853 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑦 / 𝐴) ∈
ℝ) |
78 | 66 | recnd 10068 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑦 ∈
ℂ) |
79 | 75 | recnd 10068 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝐴 ∈
ℂ) |
80 | | eldifsni 4320 |
. . . . . . . 8
⊢ (𝑦 ∈ (ran ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) ∖ {0}) → 𝑦 ≠ 0) |
81 | 80 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ 𝑦 ≠
0) |
82 | 78, 79, 81, 76 | divne0d 10817 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑦 / 𝐴) ≠ 0) |
83 | | eldifsn 4317 |
. . . . . 6
⊢ ((𝑦 / 𝐴) ∈ (ℝ ∖ {0}) ↔
((𝑦 / 𝐴) ∈ ℝ ∧ (𝑦 / 𝐴) ≠ 0)) |
84 | 77, 82, 83 | sylanbrc 698 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (𝑦 / 𝐴) ∈ (ℝ ∖
{0})) |
85 | | i1fima2sn 23447 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ (𝑦 / 𝐴) ∈ (ℝ ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑦 / 𝐴)})) ∈ ℝ) |
86 | 74, 84, 85 | syl2anc 693 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (vol‘(◡𝐹 “ {(𝑦 / 𝐴)})) ∈ ℝ) |
87 | 73, 86 | eqeltrd 2701 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑦 ∈ (ran ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∖ {0}))
→ (vol‘(◡((ℝ ×
{𝐴})
∘𝑓 · 𝐹) “ {𝑦})) ∈ ℝ) |
88 | 25, 61, 72, 87 | i1fd 23448 |
. 2
⊢ ((𝜑 ∧ 𝐴 ≠ 0) → ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∈ dom
∫1) |
89 | 17, 88 | pm2.61dane 2881 |
1
⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓
· 𝐹) ∈ dom
∫1) |