i1fmulc

Description: A nonnegative constant times a simple function gives another simple 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	i1fmulc	$⊢ φ \to (ℝ \times \{A\}) \times_{f} F \in dom \int^{1}$

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	$⊢ (φ \land A = 0) \to ℝ \in V$
5		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
6	1 5	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
7	6	adantr	$⊢ (φ \land A = 0) \to F : ℝ ⟶ ℝ$
8	2	adantr	$⊢ (φ \land A = 0) \to A \in ℝ$
9		0red	$⊢ (φ \land A = 0) \to 0 \in ℝ$
10		simplr	$⊢ ((φ \land A = 0) \land x \in ℝ) \to A = 0$
11	10	oveq1d	$⊢ ((φ \land A = 0) \land x \in ℝ) \to A x = 0 \cdot x$
12		mul02lem2	$⊢ x \in ℝ \to 0 \cdot x = 0$
13	12	adantl	$⊢ ((φ \land A = 0) \land x \in ℝ) \to 0 \cdot x = 0$
14	11 13	eqtrd	$⊢ ((φ \land A = 0) \land x \in ℝ) \to A x = 0$
15	4 7 8 9 14	caofid2	$⊢ (φ \land A = 0) \to (ℝ \times \{A\}) \times_{f} F = ℝ \times \{0\}$
16		i1f0	$⊢ ℝ \times \{0\} \in dom \int^{1}$
17	15 16	eqeltrdi	$⊢ (φ \land A = 0) \to (ℝ \times \{A\}) \times_{f} F \in dom \int^{1}$
18		remulcl	$⊢ (x \in ℝ \land y \in ℝ) \to x y \in ℝ$
19	18	adantl	$⊢ (φ \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
20		fconst6g	$⊢ A \in ℝ \to (ℝ \times \{A\}) : ℝ ⟶ ℝ$
21	2 20	syl	$⊢ φ \to (ℝ \times \{A\}) : ℝ ⟶ ℝ$
22	3	a1i	$⊢ φ \to ℝ \in V$
23		inidm	$⊢ ℝ \cap ℝ = ℝ$
24	19 21 6 22 22 23	off	$⊢ φ \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ ℝ$
25	24	adantr	$⊢ (φ \land A \neq 0) \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ ℝ$
26		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
27	1 26	syl	$⊢ φ \to ran F \in Fin$
28		ovex	$⊢ A y \in V$
29		eqid	$⊢ (y \in ran F ⟼ A y) = (y \in ran F ⟼ A y)$
30	28 29	fnmpti	$⊢ (y \in ran F ⟼ A y) Fn ran F$
31		dffn4	$⊢ (y \in ran F ⟼ A y) Fn ran F \leftrightarrow (y \in ran F ⟼ A y) : ran F \underset{onto}{⟶} ran (y \in ran F ⟼ A y)$
32	30 31	mpbi	$⊢ (y \in ran F ⟼ A y) : ran F \underset{onto}{⟶} ran (y \in ran F ⟼ A y)$
33		fofi	$⊢ (ran F \in Fin \land (y \in ran F ⟼ A y) : ran F \underset{onto}{⟶} ran (y \in ran F ⟼ A y)) \to ran (y \in ran F ⟼ A y) \in Fin$
34	27 32 33	sylancl	$⊢ φ \to ran (y \in ran F ⟼ A y) \in Fin$
35		id	$⊢ w \in ran F \to w \in ran F$
36		elsni	$⊢ x \in \{A\} \to x = A$
37	36	oveq1d	$⊢ x \in \{A\} \to x w = A w$
38		oveq2	$⊢ y = w \to A y = A w$
39	38	rspceeqv	$⊢ (w \in ran F \land x w = A w) \to \exists y \in ran F x w = A y$
40	35 37 39	syl2anr	$⊢ (x \in \{A\} \land w \in ran F) \to \exists y \in ran F x w = A y$
41		ovex	$⊢ x w \in V$
42		eqeq1	$⊢ z = x w \to (z = A y \leftrightarrow x w = A y)$
43	42	rexbidv	$⊢ z = x w \to (\exists y \in ran F z = A y \leftrightarrow \exists y \in ran F x w = A y)$
44	41 43	elab	$⊢ x w \in \{z \| \exists y \in ran F z = A y\} \leftrightarrow \exists y \in ran F x w = A y$
45	40 44	sylibr	$⊢ (x \in \{A\} \land w \in ran F) \to x w \in \{z \| \exists y \in ran F z = A y\}$
46	45	adantl	$⊢ (φ \land (x \in \{A\} \land w \in ran F)) \to x w \in \{z \| \exists y \in ran F z = A y\}$
47		fconstg	$⊢ A \in ℝ \to (ℝ \times \{A\}) : ℝ ⟶ \{A\}$
48	2 47	syl	$⊢ φ \to (ℝ \times \{A\}) : ℝ ⟶ \{A\}$
49	6	ffnd	$⊢ φ \to F Fn ℝ$
50		dffn3	$⊢ F Fn ℝ \leftrightarrow F : ℝ ⟶ ran F$
51	49 50	sylib	$⊢ φ \to F : ℝ ⟶ ran F$
52	46 48 51 22 22 23	off	$⊢ φ \to ((ℝ \times \{A\}) \times_{f} F) : ℝ ⟶ \{z \| \exists y \in ran F z = A y\}$
53	52	frnd	$⊢ φ \to ran ((ℝ \times \{A\}) \times_{f} F) \subseteq \{z \| \exists y \in ran F z = A y\}$
54	29	rnmpt	$⊢ ran (y \in ran F ⟼ A y) = \{z \| \exists y \in ran F z = A y\}$
55	53 54	sseqtrrdi	$⊢ φ \to ran ((ℝ \times \{A\}) \times_{f} F) \subseteq ran (y \in ran F ⟼ A y)$
56	34 55	ssfid	$⊢ φ \to ran ((ℝ \times \{A\}) \times_{f} F) \in Fin$
57	56	adantr	$⊢ (φ \land A \neq 0) \to ran ((ℝ \times \{A\}) \times_{f} F) \in Fin$
58	24	frnd	$⊢ φ \to ran ((ℝ \times \{A\}) \times_{f} F) \subseteq ℝ$
59	58	ssdifssd	$⊢ φ \to ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \subseteq ℝ$
60	59	adantr	$⊢ (φ \land A \neq 0) \to ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\} \subseteq ℝ$
61	60	sselda	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to y \in ℝ$
62	1 2	i1fmulclem	$⊢ ((φ \land A \neq 0) \land y \in ℝ) \to {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{y\}] = F^{-1} [\{\frac{y}{A}\}]$
63	61 62	syldan	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{y\}] = F^{-1} [\{\frac{y}{A}\}]$
64		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{\frac{y}{A}\}] \in dom vol$
65	1 64	syl	$⊢ φ \to F^{-1} [\{\frac{y}{A}\}] \in dom vol$
66	65	ad2antrr	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to F^{-1} [\{\frac{y}{A}\}] \in dom vol$
67	63 66	eqeltrd	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to {((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{y\}] \in dom vol$
68	63	fveq2d	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{y\}]) = vol (F^{-1} [\{\frac{y}{A}\}])$
69	1	ad2antrr	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to F \in dom \int^{1}$
70	2	ad2antrr	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \in ℝ$
71		simplr	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \neq 0$
72	61 70 71	redivcld	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{y}{A} \in ℝ$
73	61	recnd	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to y \in ℂ$
74	70	recnd	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to A \in ℂ$
75		eldifsni	$⊢ y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\}) \to y \neq 0$
76	75	adantl	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to y \neq 0$
77	73 74 76 71	divne0d	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{y}{A} \neq 0$
78		eldifsn	$⊢ \frac{y}{A} \in (ℝ ∖ \{0\}) \leftrightarrow (\frac{y}{A} \in ℝ \land \frac{y}{A} \neq 0)$
79	72 77 78	sylanbrc	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to \frac{y}{A} \in (ℝ ∖ \{0\})$
80		i1fima2sn	$⊢ (F \in dom \int^{1} \land \frac{y}{A} \in (ℝ ∖ \{0\})) \to vol (F^{-1} [\{\frac{y}{A}\}]) \in ℝ$
81	69 79 80	syl2anc	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to vol (F^{-1} [\{\frac{y}{A}\}]) \in ℝ$
82	68 81	eqeltrd	$⊢ ((φ \land A \neq 0) \land y \in (ran ((ℝ \times \{A\}) \times_{f} F) ∖ \{0\})) \to vol ({((ℝ \times \{A\}) \times_{f} F)}^{-1} [\{y\}]) \in ℝ$
83	25 57 67 82	i1fd	$⊢ (φ \land A \neq 0) \to (ℝ \times \{A\}) \times_{f} F \in dom \int^{1}$
84	17 83	pm2.61dane	$⊢ φ \to (ℝ \times \{A\}) \times_{f} F \in dom \int^{1}$

Metamath Proof Explorer

Theorem i1fmulc

Proof