Step | Hyp | Ref
| Expression |
1 | | simp1 1054 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → 𝐴 ∈ 𝑉) |
2 | | simp2 1055 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → 𝐹:𝐴⟶ℂ) |
3 | | ffn 5958 |
. . 3
⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴) |
4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → 𝐹 Fn 𝐴) |
5 | | ax-1cn 9873 |
. . . 4
⊢ 1 ∈
ℂ |
6 | | fnconstg 6006 |
. . . 4
⊢ (1 ∈
ℂ → (𝐴 ×
{1}) Fn 𝐴) |
7 | 5, 6 | mp1i 13 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → (𝐴 × {1}) Fn 𝐴) |
8 | | simp3 1056 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → 𝐺:𝐴⟶(ℂ ∖
{0})) |
9 | | ffn 5958 |
. . . 4
⊢ (𝐺:𝐴⟶(ℂ ∖ {0}) → 𝐺 Fn 𝐴) |
10 | 8, 9 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → 𝐺 Fn 𝐴) |
11 | | inidm 3784 |
. . 3
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
12 | 7, 10, 1, 1, 11 | offn 6806 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) →
((𝐴 × {1})
∘𝑓 / 𝐺) Fn 𝐴) |
13 | 4, 10, 1, 1, 11 | offn 6806 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → (𝐹 ∘𝑓 /
𝐺) Fn 𝐴) |
14 | | eqidd 2611 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
15 | | 1cnd 9935 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → 1
∈ ℂ) |
16 | | eqidd 2611 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
17 | 1, 15, 10, 16 | ofc1 6818 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) ∧ 𝑥 ∈ 𝐴) → (((𝐴 × {1}) ∘𝑓 /
𝐺)‘𝑥) = (1 / (𝐺‘𝑥))) |
18 | | ffvelrn 6265 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
19 | 2, 18 | sylan 487 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
20 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ (ℂ ∖
{0})) |
21 | | eldifsn 4260 |
. . . . . 6
⊢ ((𝐺‘𝑥) ∈ (ℂ ∖ {0}) ↔ ((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0)) |
22 | 20, 21 | sylib 207 |
. . . . 5
⊢ ((𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0)) |
23 | 8, 22 | sylan 487 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0)) |
24 | | divrec 10580 |
. . . . . 6
⊢ (((𝐹‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0) → ((𝐹‘𝑥) / (𝐺‘𝑥)) = ((𝐹‘𝑥) · (1 / (𝐺‘𝑥)))) |
25 | 24 | eqcomd 2616 |
. . . . 5
⊢ (((𝐹‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0) → ((𝐹‘𝑥) · (1 / (𝐺‘𝑥))) = ((𝐹‘𝑥) / (𝐺‘𝑥))) |
26 | 25 | 3expb 1258 |
. . . 4
⊢ (((𝐹‘𝑥) ∈ ℂ ∧ ((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0)) → ((𝐹‘𝑥) · (1 / (𝐺‘𝑥))) = ((𝐹‘𝑥) / (𝐺‘𝑥))) |
27 | 19, 23, 26 | syl2anc 691 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · (1 / (𝐺‘𝑥))) = ((𝐹‘𝑥) / (𝐺‘𝑥))) |
28 | 4, 10, 1, 1, 11, 14, 16 | ofval 6804 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘𝑓 / 𝐺)‘𝑥) = ((𝐹‘𝑥) / (𝐺‘𝑥))) |
29 | 27, 28 | eqtr4d 2647 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · (1 / (𝐺‘𝑥))) = ((𝐹 ∘𝑓 / 𝐺)‘𝑥)) |
30 | 1, 4, 12, 13, 14, 17, 29 | offveq 6816 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶(ℂ ∖ {0})) → (𝐹 ∘𝑓
· ((𝐴 × {1})
∘𝑓 / 𝐺)) = (𝐹 ∘𝑓 / 𝐺)) |