Theorem ofdivdiv2

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

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

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → 𝐴 ∈ 𝑉 )
2		simplr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → 𝐹 : 𝐴 ⟶ ℂ )
3	2	ffnd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → 𝐹 Fn 𝐴 )
4		simprl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) )
5	4	ffnd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → 𝐺 Fn 𝐴 )
6		simprr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) )
7	6	ffnd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → 𝐻 Fn 𝐴 )
8		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
9	5 7 1 1 8	offn	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → ( 𝐺 ∘f / 𝐻 ) Fn 𝐴 )
10	3 7 1 1 8	offn	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → ( 𝐹 ∘f · 𝐻 ) Fn 𝐴 )
11	10 5 1 1 8	offn	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → ( ( 𝐹 ∘f · 𝐻 ) ∘f / 𝐺 ) Fn 𝐴 )
12		eqidd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
13		eqidd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ∘f / 𝐻 ) ‘ 𝑥 ) = ( ( 𝐺 ∘f / 𝐻 ) ‘ 𝑥 ) )
14		ffvelcdm	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
15	2 14	sylan	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
16		ffvelcdm	⊢ ( ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
17		eldifsn	⊢ ( ( 𝐺 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
18	16 17	sylib	⊢ ( ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
19	4 18	sylan	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) )
20		ffvelcdm	⊢ ( ( 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
21		eldifsn	⊢ ( ( 𝐻 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐻 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐻 ‘ 𝑥 ) ≠ 0 ) )
22	20 21	sylib	⊢ ( ( 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐻 ‘ 𝑥 ) ≠ 0 ) )
23	6 22	sylan	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐻 ‘ 𝑥 ) ≠ 0 ) )
24		divdiv2	⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℂ ∧ ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ≠ 0 ) ∧ ( ( 𝐻 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐻 ‘ 𝑥 ) ≠ 0 ) ) → ( ( 𝐹 ‘ 𝑥 ) / ( ( 𝐺 ‘ 𝑥 ) / ( 𝐻 ‘ 𝑥 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) / ( 𝐺 ‘ 𝑥 ) ) )
25	15 19 23 24	syl3anc	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) / ( ( 𝐺 ‘ 𝑥 ) / ( 𝐻 ‘ 𝑥 ) ) ) = ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) / ( 𝐺 ‘ 𝑥 ) ) )
26		eqidd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
27		eqidd	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
28	5 7 1 1 8 26 27	ofval	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ∘f / 𝐻 ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) / ( 𝐻 ‘ 𝑥 ) ) )
29	28	oveq2d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) / ( ( 𝐺 ∘f / 𝐻 ) ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) / ( ( 𝐺 ‘ 𝑥 ) / ( 𝐻 ‘ 𝑥 ) ) ) )
30	3 7 1 1 8 12 27	ofval	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ∘f · 𝐻 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) )
31	10 5 1 1 8 30 26	ofval	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ∘f · 𝐻 ) ∘f / 𝐺 ) ‘ 𝑥 ) = ( ( ( 𝐹 ‘ 𝑥 ) · ( 𝐻 ‘ 𝑥 ) ) / ( 𝐺 ‘ 𝑥 ) ) )
32	25 29 31	3eqtr4d	⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) / ( ( 𝐺 ∘f / 𝐻 ) ‘ 𝑥 ) ) = ( ( ( 𝐹 ∘f · 𝐻 ) ∘f / 𝐺 ) ‘ 𝑥 ) )
33	1 3 9 11 12 13 32	offveq	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ℂ ) ∧ ( 𝐺 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ∧ 𝐻 : 𝐴 ⟶ ( ℂ ∖ { 0 } ) ) ) → ( 𝐹 ∘f / ( 𝐺 ∘f / 𝐻 ) ) = ( ( 𝐹 ∘f · 𝐻 ) ∘f / 𝐺 ) )