Metamath Proof Explorer

Theorem ofdivcan4

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

Ref Expression
Assertion ofdivcan4 ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → ( ( 𝐹 ∘f · 𝐺 ) ∘f / 𝐺 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐴 ∈ 𝑉 )
2 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐹 : 𝐴 ⟶ ℂ )
3 2 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐹 Fn 𝐴 )
4 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) )
5 4 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐺 Fn 𝐴 )
6 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
7 3 5 1 1 6 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → ( 𝐹 ∘f · 𝐺 ) Fn 𝐴 )
8 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
9 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
10 3 5 1 1 6 8 9 ofval ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) )
11 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
12 2 11 sylan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
13 ffvelcdm ⊢ ( ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
14 eldifsn ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
15 13 14 sylib ⊢ ( ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
16 4 15 sylan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
17 divcan4 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) / ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
18 17 3expb ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) / ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
19 12 16 18 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) / ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
20 1 7 5 3 10 9 19 offveq ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → ( ( 𝐹 ∘f · 𝐺 ) ∘f / 𝐺 ) = 𝐹 )