i1fmullem

Description: Decompose the preimage of a product. (Contributed by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
	i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
Assertion	i1fmullem	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to {(F \times_{f} G)}^{-1} [\{A\}] = ⋃_{y \in ran G ∖ \{0\}} (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}])$

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
2		i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
3		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
4	1 3	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
5	4	ffnd	$⊢ φ \to F Fn ℝ$
6		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
7	2 6	syl	$⊢ φ \to G : ℝ ⟶ ℝ$
8	7	ffnd	$⊢ φ \to G Fn ℝ$
9		reex	$⊢ ℝ \in V$
10	9	a1i	$⊢ φ \to ℝ \in V$
11		inidm	$⊢ ℝ \cap ℝ = ℝ$
12	5 8 10 10 11	offn	$⊢ φ \to (F \times_{f} G) Fn ℝ$
13	12	adantr	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to (F \times_{f} G) Fn ℝ$
14		fniniseg	$⊢ (F \times_{f} G) Fn ℝ \to (z \in {(F \times_{f} G)}^{-1} [\{A\}] \leftrightarrow (z \in ℝ \land (F \times_{f} G) (z) = A))$
15	13 14	syl	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to (z \in {(F \times_{f} G)}^{-1} [\{A\}] \leftrightarrow (z \in ℝ \land (F \times_{f} G) (z) = A))$
16	5	adantr	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to F Fn ℝ$
17	8	adantr	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to G Fn ℝ$
18	9	a1i	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to ℝ \in V$
19		eqidd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land z \in ℝ) \to F (z) = F (z)$
20		eqidd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land z \in ℝ) \to G (z) = G (z)$
21	16 17 18 18 11 19 20	ofval	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land z \in ℝ) \to (F \times_{f} G) (z) = F (z) G (z)$
22	21	eqeq1d	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land z \in ℝ) \to ((F \times_{f} G) (z) = A \leftrightarrow F (z) G (z) = A)$
23	22	pm5.32da	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to ((z \in ℝ \land (F \times_{f} G) (z) = A) \leftrightarrow (z \in ℝ \land F (z) G (z) = A))$
24	8	ad2antrr	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to G Fn ℝ$
25		simprl	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to z \in ℝ$
26		fnfvelrn	$⊢ (G Fn ℝ \land z \in ℝ) \to G (z) \in ran G$
27	24 25 26	syl2anc	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to G (z) \in ran G$
28		eldifsni	$⊢ A \in (ℂ ∖ \{0\}) \to A \neq 0$
29	28	ad2antlr	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to A \neq 0$
30		simprr	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to F (z) G (z) = A$
31	4	ad2antrr	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to F : ℝ ⟶ ℝ$
32	31 25	ffvelrnd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to F (z) \in ℝ$
33	32	recnd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to F (z) \in ℂ$
34	33	mul01d	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to F (z) \cdot 0 = 0$
35	29 30 34	3netr4d	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to F (z) G (z) \neq F (z) \cdot 0$
36		oveq2	$⊢ G (z) = 0 \to F (z) G (z) = F (z) \cdot 0$
37	36	necon3i	$⊢ F (z) G (z) \neq F (z) \cdot 0 \to G (z) \neq 0$
38	35 37	syl	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to G (z) \neq 0$
39		eldifsn	$⊢ G (z) \in (ran G ∖ \{0\}) \leftrightarrow (G (z) \in ran G \land G (z) \neq 0)$
40	27 38 39	sylanbrc	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to G (z) \in (ran G ∖ \{0\})$
41	7	ad2antrr	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to G : ℝ ⟶ ℝ$
42	41 25	ffvelrnd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to G (z) \in ℝ$
43	42	recnd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to G (z) \in ℂ$
44	33 43 38	divcan4d	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to \frac{F (z) G (z)}{G (z)} = F (z)$
45	30	oveq1d	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to \frac{F (z) G (z)}{G (z)} = \frac{A}{G (z)}$
46	44 45	eqtr3d	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to F (z) = \frac{A}{G (z)}$
47	31	ffnd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to F Fn ℝ$
48		fniniseg	$⊢ F Fn ℝ \to (z \in F^{-1} [\{\frac{A}{G (z)}\}] \leftrightarrow (z \in ℝ \land F (z) = \frac{A}{G (z)}))$
49	47 48	syl	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to (z \in F^{-1} [\{\frac{A}{G (z)}\}] \leftrightarrow (z \in ℝ \land F (z) = \frac{A}{G (z)}))$
50	25 46 49	mpbir2and	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to z \in F^{-1} [\{\frac{A}{G (z)}\}]$
51		eqidd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to G (z) = G (z)$
52		fniniseg	$⊢ G Fn ℝ \to (z \in G^{-1} [\{G (z)\}] \leftrightarrow (z \in ℝ \land G (z) = G (z)))$
53	24 52	syl	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to (z \in G^{-1} [\{G (z)\}] \leftrightarrow (z \in ℝ \land G (z) = G (z)))$
54	25 51 53	mpbir2and	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to z \in G^{-1} [\{G (z)\}]$
55	50 54	elind	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to z \in (F^{-1} [\{\frac{A}{G (z)}\}] \cap G^{-1} [\{G (z)\}])$
56		oveq2	$⊢ y = G (z) \to \frac{A}{y} = \frac{A}{G (z)}$
57	56	sneqd	$⊢ y = G (z) \to \{\frac{A}{y}\} = \{\frac{A}{G (z)}\}$
58	57	imaeq2d	$⊢ y = G (z) \to F^{-1} [\{\frac{A}{y}\}] = F^{-1} [\{\frac{A}{G (z)}\}]$
59		sneq	$⊢ y = G (z) \to \{y\} = \{G (z)\}$
60	59	imaeq2d	$⊢ y = G (z) \to G^{-1} [\{y\}] = G^{-1} [\{G (z)\}]$
61	58 60	ineq12d	$⊢ y = G (z) \to F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}] = F^{-1} [\{\frac{A}{G (z)}\}] \cap G^{-1} [\{G (z)\}]$
62	61	eleq2d	$⊢ y = G (z) \to (z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]) \leftrightarrow z \in (F^{-1} [\{\frac{A}{G (z)}\}] \cap G^{-1} [\{G (z)\}]))$
63	62	rspcev	$⊢ (G (z) \in (ran G ∖ \{0\}) \land z \in (F^{-1} [\{\frac{A}{G (z)}\}] \cap G^{-1} [\{G (z)\}])) \to \exists y \in (ran G ∖ \{0\}) z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}])$
64	40 55 63	syl2anc	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (z \in ℝ \land F (z) G (z) = A)) \to \exists y \in (ran G ∖ \{0\}) z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}])$
65	64	ex	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to ((z \in ℝ \land F (z) G (z) = A) \to \exists y \in (ran G ∖ \{0\}) z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]))$
66		fniniseg	$⊢ F Fn ℝ \to (z \in F^{-1} [\{\frac{A}{y}\}] \leftrightarrow (z \in ℝ \land F (z) = \frac{A}{y}))$
67	16 66	syl	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to (z \in F^{-1} [\{\frac{A}{y}\}] \leftrightarrow (z \in ℝ \land F (z) = \frac{A}{y}))$
68		fniniseg	$⊢ G Fn ℝ \to (z \in G^{-1} [\{y\}] \leftrightarrow (z \in ℝ \land G (z) = y))$
69	17 68	syl	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to (z \in G^{-1} [\{y\}] \leftrightarrow (z \in ℝ \land G (z) = y))$
70	67 69	anbi12d	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to ((z \in F^{-1} [\{\frac{A}{y}\}] \land z \in G^{-1} [\{y\}]) \leftrightarrow ((z \in ℝ \land F (z) = \frac{A}{y}) \land (z \in ℝ \land G (z) = y)))$
71		elin	$⊢ z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]) \leftrightarrow (z \in F^{-1} [\{\frac{A}{y}\}] \land z \in G^{-1} [\{y\}])$
72		anandi	$⊢ (z \in ℝ \land (F (z) = \frac{A}{y} \land G (z) = y)) \leftrightarrow ((z \in ℝ \land F (z) = \frac{A}{y}) \land (z \in ℝ \land G (z) = y))$
73	70 71 72	3bitr4g	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to (z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]) \leftrightarrow (z \in ℝ \land (F (z) = \frac{A}{y} \land G (z) = y)))$
74	73	adantr	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land y \in (ran G ∖ \{0\})) \to (z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]) \leftrightarrow (z \in ℝ \land (F (z) = \frac{A}{y} \land G (z) = y)))$
75		eldifi	$⊢ A \in (ℂ ∖ \{0\}) \to A \in ℂ$
76	75	ad2antlr	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to A \in ℂ$
77	7	ad2antrr	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to G : ℝ ⟶ ℝ$
78	77	frnd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to ran G \subseteq ℝ$
79		simprl	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to y \in (ran G ∖ \{0\})$
80		eldifsn	$⊢ y \in (ran G ∖ \{0\}) \leftrightarrow (y \in ran G \land y \neq 0)$
81	79 80	sylib	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to (y \in ran G \land y \neq 0)$
82	81	simpld	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to y \in ran G$
83	78 82	sseldd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to y \in ℝ$
84	83	recnd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to y \in ℂ$
85	81	simprd	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to y \neq 0$
86	76 84 85	divcan1d	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to (\frac{A}{y}) y = A$
87		oveq12	$⊢ (F (z) = \frac{A}{y} \land G (z) = y) \to F (z) G (z) = (\frac{A}{y}) y$
88	87	eqeq1d	$⊢ (F (z) = \frac{A}{y} \land G (z) = y) \to (F (z) G (z) = A \leftrightarrow (\frac{A}{y}) y = A)$
89	86 88	syl5ibrcom	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land (y \in (ran G ∖ \{0\}) \land z \in ℝ)) \to ((F (z) = \frac{A}{y} \land G (z) = y) \to F (z) G (z) = A)$
90	89	anassrs	$⊢ (((φ \land A \in (ℂ ∖ \{0\})) \land y \in (ran G ∖ \{0\})) \land z \in ℝ) \to ((F (z) = \frac{A}{y} \land G (z) = y) \to F (z) G (z) = A)$
91	90	imdistanda	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land y \in (ran G ∖ \{0\})) \to ((z \in ℝ \land (F (z) = \frac{A}{y} \land G (z) = y)) \to (z \in ℝ \land F (z) G (z) = A))$
92	74 91	sylbid	$⊢ ((φ \land A \in (ℂ ∖ \{0\})) \land y \in (ran G ∖ \{0\})) \to (z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]) \to (z \in ℝ \land F (z) G (z) = A))$
93	92	rexlimdva	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to (\exists y \in (ran G ∖ \{0\}) z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]) \to (z \in ℝ \land F (z) G (z) = A))$
94	65 93	impbid	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to ((z \in ℝ \land F (z) G (z) = A) \leftrightarrow \exists y \in (ran G ∖ \{0\}) z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]))$
95	15 23 94	3bitrd	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to (z \in {(F \times_{f} G)}^{-1} [\{A\}] \leftrightarrow \exists y \in (ran G ∖ \{0\}) z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]))$
96		eliun	$⊢ z \in ⋃_{y \in ran G ∖ \{0\}} (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]) \leftrightarrow \exists y \in (ran G ∖ \{0\}) z \in (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}])$
97	95 96	bitr4di	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to (z \in {(F \times_{f} G)}^{-1} [\{A\}] \leftrightarrow z \in ⋃_{y \in ran G ∖ \{0\}} (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}]))$
98	97	eqrdv	$⊢ (φ \land A \in (ℂ ∖ \{0\})) \to {(F \times_{f} G)}^{-1} [\{A\}] = ⋃_{y \in ran G ∖ \{0\}} (F^{-1} [\{\frac{A}{y}\}] \cap G^{-1} [\{y\}])$

Metamath Proof Explorer

Theorem i1fmullem

Proof