ofdivcan4

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

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to A \in V$
2		simp2	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to F : A ⟶ ℂ$
3	2	ffnd	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to F Fn A$
4		simp3	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to G : A ⟶ ℂ ∖ \{0\}$
5	4	ffnd	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to G Fn A$
6		inidm	$⊢ A \cap A = A$
7	3 5 1 1 6	offn	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to (F \times_{f} G) Fn A$
8		eqidd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to F (x) = F (x)$
9		eqidd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to G (x) = G (x)$
10	3 5 1 1 6 8 9	ofval	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to (F \times_{f} G) (x) = F (x) G (x)$
11		ffvelcdm	$⊢ (F : A ⟶ ℂ \land x \in A) \to F (x) \in ℂ$
12	2 11	sylan	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to F (x) \in ℂ$
13		ffvelcdm	$⊢ (G : A ⟶ ℂ ∖ \{0\} \land x \in A) \to G (x) \in (ℂ ∖ \{0\})$
14		eldifsn	$⊢ G (x) \in (ℂ ∖ \{0\}) \leftrightarrow (G (x) \in ℂ \land G (x) \neq 0)$
15	13 14	sylib	$⊢ (G : A ⟶ ℂ ∖ \{0\} \land x \in A) \to (G (x) \in ℂ \land G (x) \neq 0)$
16	4 15	sylan	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to (G (x) \in ℂ \land G (x) \neq 0)$
17		divcan4	$⊢ (F (x) \in ℂ \land G (x) \in ℂ \land G (x) \neq 0) \to \frac{F (x) G (x)}{G (x)} = F (x)$
18	17	3expb	$⊢ (F (x) \in ℂ \land (G (x) \in ℂ \land G (x) \neq 0)) \to \frac{F (x) G (x)}{G (x)} = F (x)$
19	12 16 18	syl2anc	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to \frac{F (x) G (x)}{G (x)} = F (x)$
20	1 7 5 3 10 9 19	offveq	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to (F \times_{f} G) \div_{f} G = F$

Metamath Proof Explorer

Theorem ofdivcan4

Proof