Metamath Proof Explorer

Theorem ofdivrec

Description: Function analogue of divrec , a division analogue of ofnegsub . (Contributed by Steve Rodriguez, 3-Nov-2015)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐴 ∈ 𝑉 )
2 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐹 : 𝐴 ⟶ ℂ )
3 2 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐹 Fn 𝐴 )
4 ax-1cn ⊢ 1 ∈ ℂ
5 fnconstg ⊢ ( 1 ∈ ℂ → ( 𝐴 × { 1 } ) Fn 𝐴 )
6 4 5 mp1i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → ( 𝐴 × { 1 } ) Fn 𝐴 )
7 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) )
8 7 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 𝐺 Fn 𝐴 )
9 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
10 6 8 1 1 9 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → ( ( 𝐴 × { 1 } ) ∘f / 𝐺 ) Fn 𝐴 )
11 3 8 1 1 9 offn ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → ( 𝐹 ∘f / 𝐺 ) Fn 𝐴 )
12 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
13 1cnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → 1 ∈ ℂ )
14 eqidd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
15 1 13 8 14 ofc1 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐴 × { 1 } ) ∘f / 𝐺 ) ‘ 𝑥 ) = ( 1 / ( 𝐺 ‘ 𝑥 ) ) )
16 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
17 2 16 sylan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
18 ffvelcdm ⊢ ( ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
19 eldifsn ⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
20 18 19 sylib ⊢ ( ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
21 7 20 sylan ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
22 divrec ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) → ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 1 / ( 𝐺 ‘ 𝑥 ) ) ) )
23 22 eqcomd ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) → ( ( 𝐹 ‘ 𝑥 ) · ( 1 / ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
24 23 3expb ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( 1 / ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
25 17 21 24 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) · ( 1 / ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
26 3 8 1 1 9 12 14 ofval ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f / 𝐺 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) / ( 𝐺 ‘ 𝑥 ) ) )
27 25 26 eqtr4d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) · ( 1 / ( 𝐺 ‘ 𝑥 ) ) ) = ( ( 𝐹 ∘f / 𝐺 ) ‘ 𝑥 ) )
28 1 3 10 11 12 15 27 offveq ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) → ( 𝐹 ∘f · ( ( 𝐴 × { 1 } ) ∘f / 𝐺 ) ) = ( 𝐹 ∘f / 𝐺 ) )