Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → 𝐴 ∈ 𝑉) |
2 | | simplr 788 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → 𝐹:𝐴⟶ℂ) |
3 | | ffn 5958 |
. . 3
⊢ (𝐹:𝐴⟶ℂ → 𝐹 Fn 𝐴) |
4 | 2, 3 | syl 17 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → 𝐹 Fn 𝐴) |
5 | | simprl 790 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → 𝐺:𝐴⟶(ℂ ∖
{0})) |
6 | | ffn 5958 |
. . . 4
⊢ (𝐺:𝐴⟶(ℂ ∖ {0}) → 𝐺 Fn 𝐴) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → 𝐺 Fn 𝐴) |
8 | | simprr 792 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → 𝐻:𝐴⟶(ℂ ∖
{0})) |
9 | | ffn 5958 |
. . . 4
⊢ (𝐻:𝐴⟶(ℂ ∖ {0}) → 𝐻 Fn 𝐴) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) → 𝐻 Fn 𝐴) |
11 | | inidm 3784 |
. . 3
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
12 | 7, 10, 1, 1, 11 | offn 6806 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) →
(𝐺
∘𝑓 / 𝐻) Fn 𝐴) |
13 | 4, 10, 1, 1, 11 | offn 6806 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) →
(𝐹
∘𝑓 · 𝐻) Fn 𝐴) |
14 | 13, 7, 1, 1, 11 | offn 6806 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) →
((𝐹
∘𝑓 · 𝐻) ∘𝑓 / 𝐺) Fn 𝐴) |
15 | | eqidd 2611 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
16 | | eqidd 2611 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘𝑓 / 𝐻)‘𝑥) = ((𝐺 ∘𝑓 / 𝐻)‘𝑥)) |
17 | | ffvelrn 6265 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
18 | 2, 17 | sylan 487 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
19 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ (ℂ ∖
{0})) |
20 | | eldifsn 4260 |
. . . . . 6
⊢ ((𝐺‘𝑥) ∈ (ℂ ∖ {0}) ↔ ((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0)) |
21 | 19, 20 | sylib 207 |
. . . . 5
⊢ ((𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0)) |
22 | 5, 21 | sylan 487 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → ((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0)) |
23 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝐻:𝐴⟶(ℂ ∖ {0}) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈ (ℂ ∖
{0})) |
24 | | eldifsn 4260 |
. . . . . 6
⊢ ((𝐻‘𝑥) ∈ (ℂ ∖ {0}) ↔ ((𝐻‘𝑥) ∈ ℂ ∧ (𝐻‘𝑥) ≠ 0)) |
25 | 23, 24 | sylib 207 |
. . . . 5
⊢ ((𝐻:𝐴⟶(ℂ ∖ {0}) ∧ 𝑥 ∈ 𝐴) → ((𝐻‘𝑥) ∈ ℂ ∧ (𝐻‘𝑥) ≠ 0)) |
26 | 8, 25 | sylan 487 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → ((𝐻‘𝑥) ∈ ℂ ∧ (𝐻‘𝑥) ≠ 0)) |
27 | | divdiv2 10616 |
. . . 4
⊢ (((𝐹‘𝑥) ∈ ℂ ∧ ((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑥) ≠ 0) ∧ ((𝐻‘𝑥) ∈ ℂ ∧ (𝐻‘𝑥) ≠ 0)) → ((𝐹‘𝑥) / ((𝐺‘𝑥) / (𝐻‘𝑥))) = (((𝐹‘𝑥) · (𝐻‘𝑥)) / (𝐺‘𝑥))) |
28 | 18, 22, 26, 27 | syl3anc 1318 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) / ((𝐺‘𝑥) / (𝐻‘𝑥))) = (((𝐹‘𝑥) · (𝐻‘𝑥)) / (𝐺‘𝑥))) |
29 | | eqidd 2611 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
30 | | eqidd 2611 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐻‘𝑥)) |
31 | 7, 10, 1, 1, 11, 29, 30 | ofval 6804 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘𝑓 / 𝐻)‘𝑥) = ((𝐺‘𝑥) / (𝐻‘𝑥))) |
32 | 31 | oveq2d 6565 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) / ((𝐺 ∘𝑓 / 𝐻)‘𝑥)) = ((𝐹‘𝑥) / ((𝐺‘𝑥) / (𝐻‘𝑥)))) |
33 | 4, 10, 1, 1, 11, 15, 30 | ofval 6804 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘𝑓 · 𝐻)‘𝑥) = ((𝐹‘𝑥) · (𝐻‘𝑥))) |
34 | 13, 7, 1, 1, 11, 33, 29 | ofval 6804 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → (((𝐹 ∘𝑓 · 𝐻) ∘𝑓 /
𝐺)‘𝑥) = (((𝐹‘𝑥) · (𝐻‘𝑥)) / (𝐺‘𝑥))) |
35 | 28, 32, 34 | 3eqtr4d 2654 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) / ((𝐺 ∘𝑓 / 𝐻)‘𝑥)) = (((𝐹 ∘𝑓 · 𝐻) ∘𝑓 /
𝐺)‘𝑥)) |
36 | 1, 4, 12, 14, 15, 16, 35 | offveq 6816 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶(ℂ ∖ {0}) ∧ 𝐻:𝐴⟶(ℂ ∖ {0}))) →
(𝐹
∘𝑓 / (𝐺 ∘𝑓 / 𝐻)) = ((𝐹 ∘𝑓 · 𝐻) ∘𝑓 /
𝐺)) |