Metamath Proof Explorer

Theorem ofmul12

Description: Function analogue of mul12 . (Contributed by Steve Rodriguez, 13-Nov-2015)

Ref Expression
Assertion ofmul12 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → ( 𝐹 ∘f · ( 𝐺 ∘f · 𝐻 ) ) = ( 𝐺 ∘f · ( 𝐹 ∘f · 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → 𝐴 ∈ 𝑉 )
2 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → 𝐹 : 𝐴 ⟶ ℂ )
3 2 ffnd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → 𝐹 Fn 𝐴 )
4 simprl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → 𝐺 : 𝐴 ⟶ ℂ )
5 4 ffnd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → 𝐺 Fn 𝐴 )
6 simprr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → 𝐻 : 𝐴 ⟶ ℂ )
7 6 ffnd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → 𝐻 Fn 𝐴 )
8 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
9 5 7 1 1 8 offn ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → ( 𝐺 ∘f · 𝐻 ) Fn 𝐴 )
10 3 7 1 1 8 offn ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → ( 𝐹 ∘f · 𝐻 ) Fn 𝐴 )
11 5 10 1 1 8 offn ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → ( 𝐺 ∘f · ( 𝐹 ∘f · 𝐻 ) ) Fn 𝐴 )
12 eqidd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
13 eqidd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
14 eqidd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
15 5 7 1 1 8 13 14 ofval ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ∘f · 𝐻 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) )
16 2 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
17 4 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
18 6 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ ℂ )
19 16 17 18 mul12d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) · ( ( 𝐺 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) ) = ( ( 𝐺 ‘ 𝑥 ) · ( ( 𝐹 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) ) )
20 3 7 1 1 8 12 14 ofval ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f · 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) )
21 5 10 1 1 8 13 20 ofval ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ∘f · ( 𝐹 ∘f · 𝐻 ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) · ( ( 𝐹 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) ) )
22 19 21 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) · ( ( 𝐺 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) ) = ( ( 𝐺 ∘f · ( 𝐹 ∘f · 𝐻 ) ) ‘ 𝑥 ) )
23 1 3 9 11 12 15 22 offveq ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ℂ ∧ 𝐻 : 𝐴 ⟶ ℂ ) ) → ( 𝐹 ∘f · ( 𝐺 ∘f · 𝐻 ) ) = ( 𝐺 ∘f · ( 𝐹 ∘f · 𝐻 ) ) )