| Step | Hyp | Ref
| Expression |
| 1 | | simpll 767 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → 𝐴 ∈ 𝑉) |
| 2 | | simplr 769 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → 𝐹:𝐴⟶ℂ) |
| 3 | 2 | ffnd 6737 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → 𝐹 Fn 𝐴) |
| 4 | | simprl 771 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → 𝐺:𝐴⟶ℂ) |
| 5 | 4 | ffnd 6737 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → 𝐺 Fn 𝐴) |
| 6 | | simprr 773 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → 𝐻:𝐴⟶ℂ) |
| 7 | 6 | ffnd 6737 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → 𝐻 Fn 𝐴) |
| 8 | | inidm 4227 |
. . 3
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
| 9 | 5, 7, 1, 1, 8 | offn 7710 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐺 ∘f · 𝐻) Fn 𝐴) |
| 10 | 3, 7, 1, 1, 8 | offn 7710 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐹 ∘f · 𝐻) Fn 𝐴) |
| 11 | 5, 10, 1, 1, 8 | offn 7710 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐺 ∘f · (𝐹 ∘f ·
𝐻)) Fn 𝐴) |
| 12 | | eqidd 2738 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
| 13 | | eqidd 2738 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
| 14 | | eqidd 2738 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) = (𝐻‘𝑥)) |
| 15 | 5, 7, 1, 1, 8, 13,
14 | ofval 7708 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘f · 𝐻)‘𝑥) = ((𝐺‘𝑥) · (𝐻‘𝑥))) |
| 16 | 2 | ffvelcdmda 7104 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
| 17 | 4 | ffvelcdmda 7104 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ ℂ) |
| 18 | 6 | ffvelcdmda 7104 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → (𝐻‘𝑥) ∈ ℂ) |
| 19 | 16, 17, 18 | mul12d 11470 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · ((𝐺‘𝑥) · (𝐻‘𝑥))) = ((𝐺‘𝑥) · ((𝐹‘𝑥) · (𝐻‘𝑥)))) |
| 20 | 3, 7, 1, 1, 8, 12,
14 | ofval 7708 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → ((𝐹 ∘f · 𝐻)‘𝑥) = ((𝐹‘𝑥) · (𝐻‘𝑥))) |
| 21 | 5, 10, 1, 1, 8, 13,
20 | ofval 7708 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘f · (𝐹 ∘f ·
𝐻))‘𝑥) = ((𝐺‘𝑥) · ((𝐹‘𝑥) · (𝐻‘𝑥)))) |
| 22 | 19, 21 | eqtr4d 2780 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) · ((𝐺‘𝑥) · (𝐻‘𝑥))) = ((𝐺 ∘f · (𝐹 ∘f ·
𝐻))‘𝑥)) |
| 23 | 1, 3, 9, 11, 12, 15, 22 | offveq 7723 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶ℂ) ∧ (𝐺:𝐴⟶ℂ ∧ 𝐻:𝐴⟶ℂ)) → (𝐹 ∘f · (𝐺 ∘f ·
𝐻)) = (𝐺 ∘f · (𝐹 ∘f ·
𝐻))) |