ofdivdiv2

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

		Ref	Expression
	Assertion	ofdivdiv2	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to F \div_{f} (G \div_{f} H) = (F \times_{f} H) \div_{f} G$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to A \in V$
2		simplr	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to F : A ⟶ ℂ$
3	2	ffnd	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to F Fn A$
4		simprl	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to G : A ⟶ ℂ ∖ \{0\}$
5	4	ffnd	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to G Fn A$
6		simprr	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to H : A ⟶ ℂ ∖ \{0\}$
7	6	ffnd	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to H Fn A$
8		inidm	$⊢ A \cap A = A$
9	5 7 1 1 8	offn	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to (G \div_{f} H) Fn A$
10	3 7 1 1 8	offn	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to (F \times_{f} H) Fn A$
11	10 5 1 1 8	offn	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to ((F \times_{f} H) \div_{f} G) Fn A$
12		eqidd	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to F (x) = F (x)$
13		eqidd	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to (G \div_{f} H) (x) = (G \div_{f} H) (x)$
14		ffvelcdm	$⊢ (F : A ⟶ ℂ \land x \in A) \to F (x) \in ℂ$
15	2 14	sylan	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to F (x) \in ℂ$
16		ffvelcdm	$⊢ (G : A ⟶ ℂ ∖ \{0\} \land x \in A) \to G (x) \in (ℂ ∖ \{0\})$
17		eldifsn	$⊢ G (x) \in (ℂ ∖ \{0\}) \leftrightarrow (G (x) \in ℂ \land G (x) \neq 0)$
18	16 17	sylib	$⊢ (G : A ⟶ ℂ ∖ \{0\} \land x \in A) \to (G (x) \in ℂ \land G (x) \neq 0)$
19	4 18	sylan	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to (G (x) \in ℂ \land G (x) \neq 0)$
20		ffvelcdm	$⊢ (H : A ⟶ ℂ ∖ \{0\} \land x \in A) \to H (x) \in (ℂ ∖ \{0\})$
21		eldifsn	$⊢ H (x) \in (ℂ ∖ \{0\}) \leftrightarrow (H (x) \in ℂ \land H (x) \neq 0)$
22	20 21	sylib	$⊢ (H : A ⟶ ℂ ∖ \{0\} \land x \in A) \to (H (x) \in ℂ \land H (x) \neq 0)$
23	6 22	sylan	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to (H (x) \in ℂ \land H (x) \neq 0)$
24		divdiv2	$⊢ (F (x) \in ℂ \land (G (x) \in ℂ \land G (x) \neq 0) \land (H (x) \in ℂ \land H (x) \neq 0)) \to \frac{F (x)}{\frac{G (x)}{H (x)}} = \frac{F (x) H (x)}{G (x)}$
25	15 19 23 24	syl3anc	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to \frac{F (x)}{\frac{G (x)}{H (x)}} = \frac{F (x) H (x)}{G (x)}$
26		eqidd	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to G (x) = G (x)$
27		eqidd	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to H (x) = H (x)$
28	5 7 1 1 8 26 27	ofval	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to (G \div_{f} H) (x) = \frac{G (x)}{H (x)}$
29	28	oveq2d	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to \frac{F (x)}{(G \div_{f} H) (x)} = \frac{F (x)}{\frac{G (x)}{H (x)}}$
30	3 7 1 1 8 12 27	ofval	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to (F \times_{f} H) (x) = F (x) H (x)$
31	10 5 1 1 8 30 26	ofval	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to ((F \times_{f} H) \div_{f} G) (x) = \frac{F (x) H (x)}{G (x)}$
32	25 29 31	3eqtr4d	$⊢ (((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \land x \in A) \to \frac{F (x)}{(G \div_{f} H) (x)} = ((F \times_{f} H) \div_{f} G) (x)$
33	1 3 9 11 12 13 32	offveq	$⊢ ((A \in V \land F : A ⟶ ℂ) \land (G : A ⟶ ℂ ∖ \{0\} \land H : A ⟶ ℂ ∖ \{0\})) \to F \div_{f} (G \div_{f} H) = (F \times_{f} H) \div_{f} G$

Metamath Proof Explorer

Theorem ofdivdiv2

Proof