ofdivrec

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

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

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		ax-1cn	$⊢ 1 \in ℂ$
5		fnconstg	$⊢ 1 \in ℂ \to (A \times \{1\}) Fn A$
6	4 5	mp1i	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to (A \times \{1\}) Fn A$
7		simp3	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to G : A ⟶ ℂ ∖ \{0\}$
8	7	ffnd	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to G Fn A$
9		inidm	$⊢ A \cap A = A$
10	6 8 1 1 9	offn	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to ((A \times \{1\}) \div_{f} G) Fn A$
11	3 8 1 1 9	offn	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to (F \div_{f} G) Fn A$
12		eqidd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to F (x) = F (x)$
13		1cnd	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to 1 \in ℂ$
14		eqidd	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to G (x) = G (x)$
15	1 13 8 14	ofc1	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to ((A \times \{1\}) \div_{f} G) (x) = \frac{1}{G (x)}$
16		ffvelrn	$⊢ (F : A ⟶ ℂ \land x \in A) \to F (x) \in ℂ$
17	2 16	sylan	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to F (x) \in ℂ$
18		ffvelrn	$⊢ (G : A ⟶ ℂ ∖ \{0\} \land x \in A) \to G (x) \in (ℂ ∖ \{0\})$
19		eldifsn	$⊢ G (x) \in (ℂ ∖ \{0\}) \leftrightarrow (G (x) \in ℂ \land G (x) \neq 0)$
20	18 19	sylib	$⊢ (G : A ⟶ ℂ ∖ \{0\} \land x \in A) \to (G (x) \in ℂ \land G (x) \neq 0)$
21	7 20	sylan	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to (G (x) \in ℂ \land G (x) \neq 0)$
22		divrec	$⊢ (F (x) \in ℂ \land G (x) \in ℂ \land G (x) \neq 0) \to \frac{F (x)}{G (x)} = F (x) (\frac{1}{G (x)})$
23	22	eqcomd	$⊢ (F (x) \in ℂ \land G (x) \in ℂ \land G (x) \neq 0) \to F (x) (\frac{1}{G (x)}) = \frac{F (x)}{G (x)}$
24	23	3expb	$⊢ (F (x) \in ℂ \land (G (x) \in ℂ \land G (x) \neq 0)) \to F (x) (\frac{1}{G (x)}) = \frac{F (x)}{G (x)}$
25	17 21 24	syl2anc	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to F (x) (\frac{1}{G (x)}) = \frac{F (x)}{G (x)}$
26	3 8 1 1 9 12 14	ofval	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to (F \div_{f} G) (x) = \frac{F (x)}{G (x)}$
27	25 26	eqtr4d	$⊢ ((A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \land x \in A) \to F (x) (\frac{1}{G (x)}) = (F \div_{f} G) (x)$
28	1 3 10 11 12 15 27	offveq	$⊢ (A \in V \land F : A ⟶ ℂ \land G : A ⟶ ℂ ∖ \{0\}) \to F \times_{f} ((A \times \{1\}) \div_{f} G) = F \div_{f} G$

Metamath Proof Explorer

Theorem ofdivrec

Proof