mbfmulc2lem

Description: Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Hypotheses	mbfmulc2re.1	$⊢ φ \to F \in MblFn$
	mbfmulc2re.2	$⊢ φ \to B \in ℝ$
	mbfmulc2lem.3	$⊢ φ \to F : A ⟶ ℝ$
Assertion	mbfmulc2lem	$⊢ φ \to (A \times \{B\}) \times_{f} F \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfmulc2re.1	$⊢ φ \to F \in MblFn$
2		mbfmulc2re.2	$⊢ φ \to B \in ℝ$
3		mbfmulc2lem.3	$⊢ φ \to F : A ⟶ ℝ$
4		remulcl	$⊢ (x \in ℝ \land y \in ℝ) \to x y \in ℝ$
5	4	adantl	$⊢ (φ \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
6		fconst6g	$⊢ B \in ℝ \to (A \times \{B\}) : A ⟶ ℝ$
7	2 6	syl	$⊢ φ \to (A \times \{B\}) : A ⟶ ℝ$
8	3	fdmd	$⊢ φ \to dom F = A$
9		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
10	1 9	syl	$⊢ φ \to dom F \in dom vol$
11	8 10	eqeltrrd	$⊢ φ \to A \in dom vol$
12		inidm	$⊢ A \cap A = A$
13	5 7 3 11 11 12	off	$⊢ φ \to ((A \times \{B\}) \times_{f} F) : A ⟶ ℝ$
14	13	adantr	$⊢ (φ \land B < 0) \to ((A \times \{B\}) \times_{f} F) : A ⟶ ℝ$
15	11	adantr	$⊢ (φ \land B < 0) \to A \in dom vol$
16		simprl	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to y \in ℝ$
17	16	rexrd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to y \in ℝ^{*}$
18		elioopnf	$⊢ y \in ℝ^{*} \to (((A \times \{B\}) \times_{f} F) (z) \in (y, +∞) \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land y < ((A \times \{B\}) \times_{f} F) (z)))$
19	17 18	syl	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) \in (y, +∞) \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land y < ((A \times \{B\}) \times_{f} F) (z)))$
20	13	ffvelcdmda	$⊢ (φ \land z \in A) \to ((A \times \{B\}) \times_{f} F) (z) \in ℝ$
21	20	ad2ant2rl	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to ((A \times \{B\}) \times_{f} F) (z) \in ℝ$
22	21	biantrurd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (y < ((A \times \{B\}) \times_{f} F) (z) \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land y < ((A \times \{B\}) \times_{f} F) (z)))$
23	3	ffvelcdmda	$⊢ (φ \land z \in A) \to F (z) \in ℝ$
24	23	ad2ant2rl	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to F (z) \in ℝ$
25	24	biantrurd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (F (z) < \frac{y}{B} \leftrightarrow (F (z) \in ℝ \land F (z) < \frac{y}{B}))$
26		simprr	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to z \in A$
27	11	ad2antrr	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to A \in dom vol$
28	2	ad2antrr	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to B \in ℝ$
29	3	ad2antrr	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to F : A ⟶ ℝ$
30	29	ffnd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to F Fn A$
31		eqidd	$⊢ (((φ \land B < 0) \land (y \in ℝ \land z \in A)) \land z \in A) \to F (z) = F (z)$
32	27 28 30 31	ofc1	$⊢ (((φ \land B < 0) \land (y \in ℝ \land z \in A)) \land z \in A) \to ((A \times \{B\}) \times_{f} F) (z) = B F (z)$
33	26 32	mpdan	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to ((A \times \{B\}) \times_{f} F) (z) = B F (z)$
34	33	breq2d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (y < ((A \times \{B\}) \times_{f} F) (z) \leftrightarrow y < B F (z))$
35	33 21	eqeltrrd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to B F (z) \in ℝ$
36	16 35	ltnegd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (y < B F (z) \leftrightarrow - B F (z) < - y)$
37	28	recnd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to B \in ℂ$
38	24	recnd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to F (z) \in ℂ$
39	37 38	mulneg1d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (- B) F (z) = - B F (z)$
40	39	breq1d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to ((- B) F (z) < - y \leftrightarrow - B F (z) < - y)$
41	16	renegcld	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to - y \in ℝ$
42	28	renegcld	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to - B \in ℝ$
43		simplr	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to B < 0$
44	28	lt0neg1d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (B < 0 \leftrightarrow 0 < - B)$
45	43 44	mpbid	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to 0 < - B$
46		ltmuldiv2	$⊢ (F (z) \in ℝ \land - y \in ℝ \land (- B \in ℝ \land 0 < - B)) \to ((- B) F (z) < - y \leftrightarrow F (z) < \frac{- y}{- B})$
47	24 41 42 45 46	syl112anc	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to ((- B) F (z) < - y \leftrightarrow F (z) < \frac{- y}{- B})$
48	36 40 47	3bitr2rd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (F (z) < \frac{- y}{- B} \leftrightarrow y < B F (z))$
49	16	recnd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to y \in ℂ$
50	43	lt0ne0d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to B \neq 0$
51	49 37 50	div2negd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to \frac{- y}{- B} = \frac{y}{B}$
52	51	breq2d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (F (z) < \frac{- y}{- B} \leftrightarrow F (z) < \frac{y}{B})$
53	34 48 52	3bitr2d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (y < ((A \times \{B\}) \times_{f} F) (z) \leftrightarrow F (z) < \frac{y}{B})$
54	16 28 50	redivcld	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to \frac{y}{B} \in ℝ$
55	54	rexrd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to \frac{y}{B} \in ℝ^{*}$
56		elioomnf	$⊢ \frac{y}{B} \in ℝ^{*} \to (F (z) \in (−∞, \frac{y}{B}) \leftrightarrow (F (z) \in ℝ \land F (z) < \frac{y}{B}))$
57	55 56	syl	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (F (z) \in (−∞, \frac{y}{B}) \leftrightarrow (F (z) \in ℝ \land F (z) < \frac{y}{B}))$
58	25 53 57	3bitr4d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (y < ((A \times \{B\}) \times_{f} F) (z) \leftrightarrow F (z) \in (−∞, \frac{y}{B}))$
59	19 22 58	3bitr2d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) \in (y, +∞) \leftrightarrow F (z) \in (−∞, \frac{y}{B}))$
60	59	anassrs	$⊢ (((φ \land B < 0) \land y \in ℝ) \land z \in A) \to (((A \times \{B\}) \times_{f} F) (z) \in (y, +∞) \leftrightarrow F (z) \in (−∞, \frac{y}{B}))$
61	60	pm5.32da	$⊢ ((φ \land B < 0) \land y \in ℝ) \to ((z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (y, +∞)) \leftrightarrow (z \in A \land F (z) \in (−∞, \frac{y}{B})))$
62	13	ffnd	$⊢ φ \to ((A \times \{B\}) \times_{f} F) Fn A$
63	62	ad2antrr	$⊢ ((φ \land B < 0) \land y \in ℝ) \to ((A \times \{B\}) \times_{f} F) Fn A$
64		elpreima	$⊢ ((A \times \{B\}) \times_{f} F) Fn A \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] \leftrightarrow (z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (y, +∞)))$
65	63 64	syl	$⊢ ((φ \land B < 0) \land y \in ℝ) \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] \leftrightarrow (z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (y, +∞)))$
66	3	ffnd	$⊢ φ \to F Fn A$
67	66	ad2antrr	$⊢ ((φ \land B < 0) \land y \in ℝ) \to F Fn A$
68		elpreima	$⊢ F Fn A \to (z \in F^{-1} [(−∞, \frac{y}{B})] \leftrightarrow (z \in A \land F (z) \in (−∞, \frac{y}{B})))$
69	67 68	syl	$⊢ ((φ \land B < 0) \land y \in ℝ) \to (z \in F^{-1} [(−∞, \frac{y}{B})] \leftrightarrow (z \in A \land F (z) \in (−∞, \frac{y}{B})))$
70	61 65 69	3bitr4d	$⊢ ((φ \land B < 0) \land y \in ℝ) \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] \leftrightarrow z \in F^{-1} [(−∞, \frac{y}{B})])$
71	70	eqrdv	$⊢ ((φ \land B < 0) \land y \in ℝ) \to {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] = F^{-1} [(−∞, \frac{y}{B})]$
72		mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(−∞, \frac{y}{B})] \in dom vol$
73	1 3 72	syl2anc	$⊢ φ \to F^{-1} [(−∞, \frac{y}{B})] \in dom vol$
74	73	ad2antrr	$⊢ ((φ \land B < 0) \land y \in ℝ) \to F^{-1} [(−∞, \frac{y}{B})] \in dom vol$
75	71 74	eqeltrd	$⊢ ((φ \land B < 0) \land y \in ℝ) \to {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] \in dom vol$
76		elioomnf	$⊢ y \in ℝ^{*} \to (((A \times \{B\}) \times_{f} F) (z) \in (−∞, y) \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land ((A \times \{B\}) \times_{f} F) (z) < y))$
77	17 76	syl	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) \in (−∞, y) \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land ((A \times \{B\}) \times_{f} F) (z) < y))$
78	21	biantrurd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) < y \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land ((A \times \{B\}) \times_{f} F) (z) < y))$
79	24	biantrurd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (\frac{y}{B} < F (z) \leftrightarrow (F (z) \in ℝ \land \frac{y}{B} < F (z)))$
80	33	breq1d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) < y \leftrightarrow B F (z) < y)$
81	39	breq2d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (- y < (- B) F (z) \leftrightarrow - y < - B F (z))$
82	51	breq1d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (\frac{- y}{- B} < F (z) \leftrightarrow \frac{y}{B} < F (z))$
83		ltdivmul	$⊢ (- y \in ℝ \land F (z) \in ℝ \land (- B \in ℝ \land 0 < - B)) \to (\frac{- y}{- B} < F (z) \leftrightarrow - y < (- B) F (z))$
84	41 24 42 45 83	syl112anc	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (\frac{- y}{- B} < F (z) \leftrightarrow - y < (- B) F (z))$
85	82 84	bitr3d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (\frac{y}{B} < F (z) \leftrightarrow - y < (- B) F (z))$
86	35 16	ltnegd	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (B F (z) < y \leftrightarrow - y < - B F (z))$
87	81 85 86	3bitr4d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (\frac{y}{B} < F (z) \leftrightarrow B F (z) < y)$
88	80 87	bitr4d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) < y \leftrightarrow \frac{y}{B} < F (z))$
89		elioopnf	$⊢ \frac{y}{B} \in ℝ^{*} \to (F (z) \in (\frac{y}{B}, +∞) \leftrightarrow (F (z) \in ℝ \land \frac{y}{B} < F (z)))$
90	55 89	syl	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (F (z) \in (\frac{y}{B}, +∞) \leftrightarrow (F (z) \in ℝ \land \frac{y}{B} < F (z)))$
91	79 88 90	3bitr4d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) < y \leftrightarrow F (z) \in (\frac{y}{B}, +∞))$
92	77 78 91	3bitr2d	$⊢ ((φ \land B < 0) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) \in (−∞, y) \leftrightarrow F (z) \in (\frac{y}{B}, +∞))$
93	92	anassrs	$⊢ (((φ \land B < 0) \land y \in ℝ) \land z \in A) \to (((A \times \{B\}) \times_{f} F) (z) \in (−∞, y) \leftrightarrow F (z) \in (\frac{y}{B}, +∞))$
94	93	pm5.32da	$⊢ ((φ \land B < 0) \land y \in ℝ) \to ((z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (−∞, y)) \leftrightarrow (z \in A \land F (z) \in (\frac{y}{B}, +∞)))$
95		elpreima	$⊢ ((A \times \{B\}) \times_{f} F) Fn A \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] \leftrightarrow (z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (−∞, y)))$
96	63 95	syl	$⊢ ((φ \land B < 0) \land y \in ℝ) \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] \leftrightarrow (z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (−∞, y)))$
97		elpreima	$⊢ F Fn A \to (z \in F^{-1} [(\frac{y}{B}, +∞)] \leftrightarrow (z \in A \land F (z) \in (\frac{y}{B}, +∞)))$
98	67 97	syl	$⊢ ((φ \land B < 0) \land y \in ℝ) \to (z \in F^{-1} [(\frac{y}{B}, +∞)] \leftrightarrow (z \in A \land F (z) \in (\frac{y}{B}, +∞)))$
99	94 96 98	3bitr4d	$⊢ ((φ \land B < 0) \land y \in ℝ) \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] \leftrightarrow z \in F^{-1} [(\frac{y}{B}, +∞)])$
100	99	eqrdv	$⊢ ((φ \land B < 0) \land y \in ℝ) \to {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] = F^{-1} [(\frac{y}{B}, +∞)]$
101		mbfima	$⊢ (F \in MblFn \land F : A ⟶ ℝ) \to F^{-1} [(\frac{y}{B}, +∞)] \in dom vol$
102	1 3 101	syl2anc	$⊢ φ \to F^{-1} [(\frac{y}{B}, +∞)] \in dom vol$
103	102	ad2antrr	$⊢ ((φ \land B < 0) \land y \in ℝ) \to F^{-1} [(\frac{y}{B}, +∞)] \in dom vol$
104	100 103	eqeltrd	$⊢ ((φ \land B < 0) \land y \in ℝ) \to {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] \in dom vol$
105	14 15 75 104	ismbf2d	$⊢ (φ \land B < 0) \to (A \times \{B\}) \times_{f} F \in MblFn$
106	11	adantr	$⊢ (φ \land B = 0) \to A \in dom vol$
107	3	adantr	$⊢ (φ \land B = 0) \to F : A ⟶ ℝ$
108		simpr	$⊢ (φ \land B = 0) \to B = 0$
109		0cn	$⊢ 0 \in ℂ$
110	108 109	eqeltrdi	$⊢ (φ \land B = 0) \to B \in ℂ$
111		0cnd	$⊢ (φ \land B = 0) \to 0 \in ℂ$
112		simplr	$⊢ ((φ \land B = 0) \land x \in ℝ) \to B = 0$
113	112	oveq1d	$⊢ ((φ \land B = 0) \land x \in ℝ) \to B x = 0 \cdot x$
114		mul02lem2	$⊢ x \in ℝ \to 0 \cdot x = 0$
115	114	adantl	$⊢ ((φ \land B = 0) \land x \in ℝ) \to 0 \cdot x = 0$
116	113 115	eqtrd	$⊢ ((φ \land B = 0) \land x \in ℝ) \to B x = 0$
117	106 107 110 111 116	caofid2	$⊢ (φ \land B = 0) \to (A \times \{B\}) \times_{f} F = A \times \{0\}$
118		mbfconst	$⊢ (A \in dom vol \land 0 \in ℂ) \to A \times \{0\} \in MblFn$
119	106 109 118	sylancl	$⊢ (φ \land B = 0) \to A \times \{0\} \in MblFn$
120	117 119	eqeltrd	$⊢ (φ \land B = 0) \to (A \times \{B\}) \times_{f} F \in MblFn$
121	13	adantr	$⊢ (φ \land 0 < B) \to ((A \times \{B\}) \times_{f} F) : A ⟶ ℝ$
122	11	adantr	$⊢ (φ \land 0 < B) \to A \in dom vol$
123		simprl	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to y \in ℝ$
124	123	rexrd	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to y \in ℝ^{*}$
125	124 18	syl	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) \in (y, +∞) \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land y < ((A \times \{B\}) \times_{f} F) (z)))$
126	20	ad2ant2rl	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to ((A \times \{B\}) \times_{f} F) (z) \in ℝ$
127	126	biantrurd	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (y < ((A \times \{B\}) \times_{f} F) (z) \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land y < ((A \times \{B\}) \times_{f} F) (z)))$
128	23	ad2ant2rl	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to F (z) \in ℝ$
129	128	biantrurd	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (\frac{y}{B} < F (z) \leftrightarrow (F (z) \in ℝ \land \frac{y}{B} < F (z)))$
130		eqidd	$⊢ (φ \land z \in A) \to F (z) = F (z)$
131	11 2 66 130	ofc1	$⊢ (φ \land z \in A) \to ((A \times \{B\}) \times_{f} F) (z) = B F (z)$
132	131	ad2ant2rl	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to ((A \times \{B\}) \times_{f} F) (z) = B F (z)$
133	132	breq2d	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (y < ((A \times \{B\}) \times_{f} F) (z) \leftrightarrow y < B F (z))$
134	2	ad2antrr	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to B \in ℝ$
135		simplr	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to 0 < B$
136		ltdivmul	$⊢ (y \in ℝ \land F (z) \in ℝ \land (B \in ℝ \land 0 < B)) \to (\frac{y}{B} < F (z) \leftrightarrow y < B F (z))$
137	123 128 134 135 136	syl112anc	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (\frac{y}{B} < F (z) \leftrightarrow y < B F (z))$
138	133 137	bitr4d	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (y < ((A \times \{B\}) \times_{f} F) (z) \leftrightarrow \frac{y}{B} < F (z))$
139	134 135	elrpd	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to B \in ℝ^{+}$
140	123 139	rerpdivcld	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to \frac{y}{B} \in ℝ$
141	140	rexrd	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to \frac{y}{B} \in ℝ^{*}$
142	141 89	syl	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (F (z) \in (\frac{y}{B}, +∞) \leftrightarrow (F (z) \in ℝ \land \frac{y}{B} < F (z)))$
143	129 138 142	3bitr4d	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (y < ((A \times \{B\}) \times_{f} F) (z) \leftrightarrow F (z) \in (\frac{y}{B}, +∞))$
144	125 127 143	3bitr2d	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) \in (y, +∞) \leftrightarrow F (z) \in (\frac{y}{B}, +∞))$
145	144	anassrs	$⊢ (((φ \land 0 < B) \land y \in ℝ) \land z \in A) \to (((A \times \{B\}) \times_{f} F) (z) \in (y, +∞) \leftrightarrow F (z) \in (\frac{y}{B}, +∞))$
146	145	pm5.32da	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to ((z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (y, +∞)) \leftrightarrow (z \in A \land F (z) \in (\frac{y}{B}, +∞)))$
147	62	ad2antrr	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to ((A \times \{B\}) \times_{f} F) Fn A$
148	147 64	syl	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] \leftrightarrow (z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (y, +∞)))$
149	66	ad2antrr	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to F Fn A$
150	149 97	syl	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to (z \in F^{-1} [(\frac{y}{B}, +∞)] \leftrightarrow (z \in A \land F (z) \in (\frac{y}{B}, +∞)))$
151	146 148 150	3bitr4d	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] \leftrightarrow z \in F^{-1} [(\frac{y}{B}, +∞)])$
152	151	eqrdv	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] = F^{-1} [(\frac{y}{B}, +∞)]$
153	102	ad2antrr	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to F^{-1} [(\frac{y}{B}, +∞)] \in dom vol$
154	152 153	eqeltrd	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to {((A \times \{B\}) \times_{f} F)}^{-1} [(y, +∞)] \in dom vol$
155	124 76	syl	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) \in (−∞, y) \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land ((A \times \{B\}) \times_{f} F) (z) < y))$
156	126	biantrurd	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) < y \leftrightarrow (((A \times \{B\}) \times_{f} F) (z) \in ℝ \land ((A \times \{B\}) \times_{f} F) (z) < y))$
157		ltmuldiv2	$⊢ (F (z) \in ℝ \land y \in ℝ \land (B \in ℝ \land 0 < B)) \to (B F (z) < y \leftrightarrow F (z) < \frac{y}{B})$
158	128 123 134 135 157	syl112anc	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (B F (z) < y \leftrightarrow F (z) < \frac{y}{B})$
159	132	breq1d	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) < y \leftrightarrow B F (z) < y)$
160	141 56	syl	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (F (z) \in (−∞, \frac{y}{B}) \leftrightarrow (F (z) \in ℝ \land F (z) < \frac{y}{B}))$
161	128 160	mpbirand	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (F (z) \in (−∞, \frac{y}{B}) \leftrightarrow F (z) < \frac{y}{B})$
162	158 159 161	3bitr4d	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) < y \leftrightarrow F (z) \in (−∞, \frac{y}{B}))$
163	155 156 162	3bitr2d	$⊢ ((φ \land 0 < B) \land (y \in ℝ \land z \in A)) \to (((A \times \{B\}) \times_{f} F) (z) \in (−∞, y) \leftrightarrow F (z) \in (−∞, \frac{y}{B}))$
164	163	anassrs	$⊢ (((φ \land 0 < B) \land y \in ℝ) \land z \in A) \to (((A \times \{B\}) \times_{f} F) (z) \in (−∞, y) \leftrightarrow F (z) \in (−∞, \frac{y}{B}))$
165	164	pm5.32da	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to ((z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (−∞, y)) \leftrightarrow (z \in A \land F (z) \in (−∞, \frac{y}{B})))$
166	147 95	syl	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] \leftrightarrow (z \in A \land ((A \times \{B\}) \times_{f} F) (z) \in (−∞, y)))$
167	149 68	syl	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to (z \in F^{-1} [(−∞, \frac{y}{B})] \leftrightarrow (z \in A \land F (z) \in (−∞, \frac{y}{B})))$
168	165 166 167	3bitr4d	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to (z \in {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] \leftrightarrow z \in F^{-1} [(−∞, \frac{y}{B})])$
169	168	eqrdv	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] = F^{-1} [(−∞, \frac{y}{B})]$
170	73	ad2antrr	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to F^{-1} [(−∞, \frac{y}{B})] \in dom vol$
171	169 170	eqeltrd	$⊢ ((φ \land 0 < B) \land y \in ℝ) \to {((A \times \{B\}) \times_{f} F)}^{-1} [(−∞, y)] \in dom vol$
172	121 122 154 171	ismbf2d	$⊢ (φ \land 0 < B) \to (A \times \{B\}) \times_{f} F \in MblFn$
173		0re	$⊢ 0 \in ℝ$
174		lttri4	$⊢ (B \in ℝ \land 0 \in ℝ) \to (B < 0 \lor B = 0 \lor 0 < B)$
175	2 173 174	sylancl	$⊢ φ \to (B < 0 \lor B = 0 \lor 0 < B)$
176	105 120 172 175	mpjao3dan	$⊢ φ \to (A \times \{B\}) \times_{f} F \in MblFn$

Metamath Proof Explorer

Theorem mbfmulc2lem

Proof