Step | Hyp | Ref
| Expression |
1 | | reex 10027 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
2 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℝ ∈
V) |
3 | | i1fmulc.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | | i1fmulc.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ dom
∫1) |
5 | | i1ff 23443 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℝ⟶ℝ) |
7 | | ffn 6045 |
. . . . . . . . . 10
⊢ (𝐹:ℝ⟶ℝ →
𝐹 Fn
ℝ) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn ℝ) |
9 | | eqidd 2623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (𝐹‘𝑧) = (𝐹‘𝑧)) |
10 | 2, 3, 8, 9 | ofc1 6920 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ) → (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑧) = (𝐴 · (𝐹‘𝑧))) |
11 | 10 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝑧 ∈ ℝ) → (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑧) = (𝐴 · (𝐹‘𝑧))) |
12 | 11 | adantlr 751 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑧) = (𝐴 · (𝐹‘𝑧))) |
13 | 12 | eqeq1d 2624 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑧) = 𝐵 ↔ (𝐴 · (𝐹‘𝑧)) = 𝐵)) |
14 | | eqcom 2629 |
. . . . . 6
⊢ ((𝐹‘𝑧) = (𝐵 / 𝐴) ↔ (𝐵 / 𝐴) = (𝐹‘𝑧)) |
15 | | simplr 792 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝐵 ∈ ℝ) |
16 | 15 | recnd 10068 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝐵 ∈ ℂ) |
17 | 3 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝐴 ∈ ℝ) |
18 | 17 | recnd 10068 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝐴 ∈ ℂ) |
19 | 6 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 𝐹:ℝ⟶ℝ) |
20 | 19 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (𝐹‘𝑧) ∈ ℝ) |
21 | 20 | recnd 10068 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → (𝐹‘𝑧) ∈ ℂ) |
22 | | simpllr 799 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → 𝐴 ≠ 0) |
23 | 16, 18, 21, 22 | divmuld 10823 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((𝐵 / 𝐴) = (𝐹‘𝑧) ↔ (𝐴 · (𝐹‘𝑧)) = 𝐵)) |
24 | 14, 23 | syl5bb 272 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((𝐹‘𝑧) = (𝐵 / 𝐴) ↔ (𝐴 · (𝐹‘𝑧)) = 𝐵)) |
25 | 13, 24 | bitr4d 271 |
. . . 4
⊢ ((((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) ∧ 𝑧 ∈ ℝ) → ((((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑧) = 𝐵 ↔ (𝐹‘𝑧) = (𝐵 / 𝐴))) |
26 | 25 | pm5.32da 673 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → ((𝑧 ∈ ℝ ∧ (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑧) = 𝐵) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐵 / 𝐴)))) |
27 | | remulcl 10021 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
28 | 27 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
29 | | fconstg 6092 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (ℝ
× {𝐴}):ℝ⟶{𝐴}) |
30 | 3, 29 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶{𝐴}) |
31 | 3 | snssd 4340 |
. . . . . . . 8
⊢ (𝜑 → {𝐴} ⊆ ℝ) |
32 | 30, 31 | fssd 6057 |
. . . . . . 7
⊢ (𝜑 → (ℝ × {𝐴}):ℝ⟶ℝ) |
33 | | inidm 3822 |
. . . . . . 7
⊢ (ℝ
∩ ℝ) = ℝ |
34 | 28, 32, 6, 2, 2, 33 | off 6912 |
. . . . . 6
⊢ (𝜑 → ((ℝ × {𝐴}) ∘𝑓
· 𝐹):ℝ⟶ℝ) |
35 | 34 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → ((ℝ ×
{𝐴})
∘𝑓 · 𝐹):ℝ⟶ℝ) |
36 | | ffn 6045 |
. . . . 5
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹):ℝ⟶ℝ
→ ((ℝ × {𝐴}) ∘𝑓 ·
𝐹) Fn
ℝ) |
37 | 35, 36 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → ((ℝ ×
{𝐴})
∘𝑓 · 𝐹) Fn ℝ) |
38 | | fniniseg 6338 |
. . . 4
⊢
(((ℝ × {𝐴}) ∘𝑓 ·
𝐹) Fn ℝ → (𝑧 ∈ (◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝐵}) ↔ (𝑧 ∈ ℝ ∧ (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑧) = 𝐵))) |
39 | 37, 38 | syl 17 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝐵}) ↔ (𝑧 ∈ ℝ ∧ (((ℝ ×
{𝐴})
∘𝑓 · 𝐹)‘𝑧) = 𝐵))) |
40 | 19, 7 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → 𝐹 Fn ℝ) |
41 | | fniniseg 6338 |
. . . 4
⊢ (𝐹 Fn ℝ → (𝑧 ∈ (◡𝐹 “ {(𝐵 / 𝐴)}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐵 / 𝐴)))) |
42 | 40, 41 | syl 17 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (◡𝐹 “ {(𝐵 / 𝐴)}) ↔ (𝑧 ∈ ℝ ∧ (𝐹‘𝑧) = (𝐵 / 𝐴)))) |
43 | 26, 39, 42 | 3bitr4d 300 |
. 2
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (𝑧 ∈ (◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝐵}) ↔ 𝑧 ∈ (◡𝐹 “ {(𝐵 / 𝐴)}))) |
44 | 43 | eqrdv 2620 |
1
⊢ (((𝜑 ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ) → (◡((ℝ × {𝐴}) ∘𝑓 ·
𝐹) “ {𝐵}) = (◡𝐹 “ {(𝐵 / 𝐴)})) |