i1fmulclem

Description: Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Hypotheses	i1fmulc.2	$⊢ φ \to F \in dom \int^{1}$
	i1fmulc.3	$⊢ φ \to A \in ℝ$
Assertion	i1fmulclem	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{B\}] = F^{-1} [\{\frac{B}{A}\}]$

Proof

Step	Hyp	Ref	Expression
1		i1fmulc.2	$⊢ φ \to F \in dom \int^{1}$
2		i1fmulc.3	$⊢ φ \to A \in ℝ$
3		reex	$⊢ ℝ \in V$
4	3	a1i	$⊢ φ \to ℝ \in V$
5		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
6	1 5	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
7	6	ffnd	$⊢ φ \to F Fn ℝ$
8		eqidd	$⊢ (φ \land z \in ℝ) \to F (z) = F (z)$
9	4 2 7 8	ofc1	$⊢ (φ \land z \in ℝ) \to ((ℝ \times \{A\}) \times_{f} F) (z) = A F (z)$
10	9	ad4ant14	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to ((ℝ \times \{A\}) \times_{f} F) (z) = A F (z)$
11	10	eqeq1d	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to (((ℝ \times \{A\}) \times_{f} F) (z) = B \leftrightarrow A F (z) = B)$
12		eqcom	$⊢ F (z) = \frac{B}{A} \leftrightarrow \frac{B}{A} = F (z)$
13		simplr	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to B \in ℝ$
14	13	recnd	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to B \in ℂ$
15	2	ad3antrrr	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to A \in ℝ$
16	15	recnd	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to A \in ℂ$
17	6	ad2antrr	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to F : ℝ ⟶ ℝ$
18	17	ffvelrnda	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to F (z) \in ℝ$
19	18	recnd	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to F (z) \in ℂ$
20		simpllr	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to A \neq 0$
21	14 16 19 20	divmuld	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to (\frac{B}{A} = F (z) \leftrightarrow A F (z) = B)$
22	12 21	syl5bb	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to (F (z) = \frac{B}{A} \leftrightarrow A F (z) = B)$
23	11 22	bitr4d	$⊢ (((φ \land A \neq 0) \land B \in ℝ) \land z \in ℝ) \to (((ℝ \times \{A\}) \times_{f} F) (z) = B \leftrightarrow F (z) = \frac{B}{A})$
24	23	pm5.32da	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to ((z \in ℝ \land ((ℝ \times \{A\}) \times_{f} F) (z) = B) \leftrightarrow (z \in ℝ \land F (z) = \frac{B}{A}))$
25		remulcl	$⊢ (x \in ℝ \land y \in ℝ) \to x y \in ℝ$
26	25	adantl	$⊢ (φ \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
27		fconstg	$⊢ A \in ℝ \to (ℝ \times \{A\}) : ℝ ⟶ \{A\}$
28	2 27	syl	$⊢ φ \to (ℝ \times \{A\}) : ℝ ⟶ \{A\}$
29	2	snssd	$⊢ φ \to \{A\} \subseteq ℝ$
30	28 29	fssd	$⊢ φ \to (ℝ \times \{A\}) : ℝ ⟶ ℝ$
31		inidm	$⊢ ℝ \cap ℝ = ℝ$
32	26 30 6 4 4 31	off	$⊢ φ \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ ℝ$
33	32	ad2antrr	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ ℝ$
34	33	ffnd	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to ((ℝ \times \{A\}) \times_{f} F) Fn ℝ$
35		fniniseg	$⊢ ((ℝ \times \{A\}) \times_{f} F) Fn ℝ \to (z \in {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{B\}] \leftrightarrow (z \in ℝ \land ((ℝ \times \{A\}) \times_{f} F) (z) = B))$
36	34 35	syl	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to (z \in {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{B\}] \leftrightarrow (z \in ℝ \land ((ℝ \times \{A\}) \times_{f} F) (z) = B))$
37	17	ffnd	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to F Fn ℝ$
38		fniniseg	$⊢ F Fn ℝ \to (z \in F^{-1} [\{\frac{B}{A}\}] \leftrightarrow (z \in ℝ \land F (z) = \frac{B}{A}))$
39	37 38	syl	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to (z \in F^{-1} [\{\frac{B}{A}\}] \leftrightarrow (z \in ℝ \land F (z) = \frac{B}{A}))$
40	24 36 39	3bitr4d	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to (z \in {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{B\}] \leftrightarrow z \in F^{-1} [\{\frac{B}{A}\}])$
41	40	eqrdv	$⊢ ((φ \land A \neq 0) \land B \in ℝ) \to {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{B\}] = F^{-1} [\{\frac{B}{A}\}]$

Metamath Proof Explorer

Theorem i1fmulclem

Proof