i1fmul

Description: The pointwise product of two simple functions is a simple function. (Contributed by Mario Carneiro, 5-Sep-2014)

	Ref	Expression
Hypotheses	i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
	i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
Assertion	i1fmul	$⊢ φ \to F \times_{f} G \in dom \int^{1}$

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
2		i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
3		remulcl	$⊢ (x \in ℝ \land y \in ℝ) \to x y \in ℝ$
4	3	adantl	$⊢ (φ \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
5		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
6	1 5	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
7		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
8	2 7	syl	$⊢ φ \to G : ℝ ⟶ ℝ$
9		reex	$⊢ ℝ \in V$
10	9	a1i	$⊢ φ \to ℝ \in V$
11		inidm	$⊢ ℝ \cap ℝ = ℝ$
12	4 6 8 10 10 11	off	$⊢ φ \to (F \times_{f} G) : ℝ ⟶ ℝ$
13		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
14	1 13	syl	$⊢ φ \to ran F \in Fin$
15		i1frn	$⊢ G \in dom \int^{1} \to ran G \in Fin$
16	2 15	syl	$⊢ φ \to ran G \in Fin$
17		xpfi	$⊢ (ran F \in Fin \land ran G \in Fin) \to ran F \times ran G \in Fin$
18	14 16 17	syl2anc	$⊢ φ \to ran F \times ran G \in Fin$
19		eqid	$⊢ (u \in ran F, v \in ran G ⟼ u v) = (u \in ran F, v \in ran G ⟼ u v)$
20		ovex	$⊢ u v \in V$
21	19 20	fnmpoi	$⊢ (u \in ran F, v \in ran G ⟼ u v) Fn (ran F \times ran G)$
22		dffn4	$⊢ (u \in ran F, v \in ran G ⟼ u v) Fn (ran F \times ran G) \leftrightarrow (u \in ran F, v \in ran G ⟼ u v) : ran F \times ran G \underset{onto}{⟶} ran (u \in ran F, v \in ran G ⟼ u v)$
23	21 22	mpbi	$⊢ (u \in ran F, v \in ran G ⟼ u v) : ran F \times ran G \underset{onto}{⟶} ran (u \in ran F, v \in ran G ⟼ u v)$
24		fofi	$⊢ (ran F \times ran G \in Fin \land (u \in ran F, v \in ran G ⟼ u v) : ran F \times ran G \underset{onto}{⟶} ran (u \in ran F, v \in ran G ⟼ u v)) \to ran (u \in ran F, v \in ran G ⟼ u v) \in Fin$
25	18 23 24	sylancl	$⊢ φ \to ran (u \in ran F, v \in ran G ⟼ u v) \in Fin$
26		eqid	$⊢ x y = x y$
27		rspceov	$⊢ (x \in ran F \land y \in ran G \land x y = x y) \to \exists u \in ran F \exists v \in ran G x y = u v$
28	26 27	mp3an3	$⊢ (x \in ran F \land y \in ran G) \to \exists u \in ran F \exists v \in ran G x y = u v$
29		ovex	$⊢ x y \in V$
30		eqeq1	$⊢ w = x y \to (w = u v \leftrightarrow x y = u v)$
31	30	2rexbidv	$⊢ w = x y \to (\exists u \in ran F \exists v \in ran G w = u v \leftrightarrow \exists u \in ran F \exists v \in ran G x y = u v)$
32	29 31	elab	$⊢ x y \in \{w \| \exists u \in ran F \exists v \in ran G w = u v\} \leftrightarrow \exists u \in ran F \exists v \in ran G x y = u v$
33	28 32	sylibr	$⊢ (x \in ran F \land y \in ran G) \to x y \in \{w \| \exists u \in ran F \exists v \in ran G w = u v\}$
34	33	adantl	$⊢ (φ \land (x \in ran F \land y \in ran G)) \to x y \in \{w \| \exists u \in ran F \exists v \in ran G w = u v\}$
35	6	ffnd	$⊢ φ \to F Fn ℝ$
36		dffn3	$⊢ F Fn ℝ \leftrightarrow F : ℝ ⟶ ran F$
37	35 36	sylib	$⊢ φ \to F : ℝ ⟶ ran F$
38	8	ffnd	$⊢ φ \to G Fn ℝ$
39		dffn3	$⊢ G Fn ℝ \leftrightarrow G : ℝ ⟶ ran G$
40	38 39	sylib	$⊢ φ \to G : ℝ ⟶ ran G$
41	34 37 40 10 10 11	off	$⊢ φ \to (F \times_{f} G) : ℝ ⟶ \{w \| \exists u \in ran F \exists v \in ran G w = u v\}$
42	41	frnd	$⊢ φ \to ran (F \times_{f} G) \subseteq \{w \| \exists u \in ran F \exists v \in ran G w = u v\}$
43	19	rnmpo	$⊢ ran (u \in ran F, v \in ran G ⟼ u v) = \{w \| \exists u \in ran F \exists v \in ran G w = u v\}$
44	42 43	sseqtrrdi	$⊢ φ \to ran (F \times_{f} G) \subseteq ran (u \in ran F, v \in ran G ⟼ u v)$
45	25 44	ssfid	$⊢ φ \to ran (F \times_{f} G) \in Fin$
46	12	frnd	$⊢ φ \to ran (F \times_{f} G) \subseteq ℝ$
47		ax-resscn	$⊢ ℝ \subseteq ℂ$
48	46 47	sstrdi	$⊢ φ \to ran (F \times_{f} G) \subseteq ℂ$
49	48	ssdifd	$⊢ φ \to ran (F \times_{f} G) ∖ \{0\} \subseteq ℂ ∖ \{0\}$
50	49	sselda	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to y \in (ℂ ∖ \{0\})$
51	1 2	i1fmullem	$⊢ (φ \land y \in (ℂ ∖ \{0\})) \to {(F \times_{f} G)}^{-1} [\{y\}] = ⋃_{z \in ran G ∖ \{0\}} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}])$
52	50 51	syldan	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to {(F \times_{f} G)}^{-1} [\{y\}] = ⋃_{z \in ran G ∖ \{0\}} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}])$
53		difss	$⊢ ran G ∖ \{0\} \subseteq ran G$
54		ssfi	$⊢ (ran G \in Fin \land ran G ∖ \{0\} \subseteq ran G) \to ran G ∖ \{0\} \in Fin$
55	16 53 54	sylancl	$⊢ φ \to ran G ∖ \{0\} \in Fin$
56		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{\frac{y}{z}\}] \in dom vol$
57	1 56	syl	$⊢ φ \to F^{-1} [\{\frac{y}{z}\}] \in dom vol$
58		i1fima	$⊢ G \in dom \int^{1} \to G^{-1} [\{z\}] \in dom vol$
59	2 58	syl	$⊢ φ \to G^{-1} [\{z\}] \in dom vol$
60		inmbl	$⊢ (F^{-1} [\{\frac{y}{z}\}] \in dom vol \land G^{-1} [\{z\}] \in dom vol) \to F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \in dom vol$
61	57 59 60	syl2anc	$⊢ φ \to F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \in dom vol$
62	61	ralrimivw	$⊢ φ \to \forall z \in (ran G ∖ \{0\}) F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \in dom vol$
63		finiunmbl	$⊢ (ran G ∖ \{0\} \in Fin \land \forall z \in (ran G ∖ \{0\}) F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \in dom vol) \to ⋃_{z \in ran G ∖ \{0\}} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in dom vol$
64	55 62 63	syl2anc	$⊢ φ \to ⋃_{z \in ran G ∖ \{0\}} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in dom vol$
65	64	adantr	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to ⋃_{z \in ran G ∖ \{0\}} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in dom vol$
66	52 65	eqeltrd	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to {(F \times_{f} G)}^{-1} [\{y\}] \in dom vol$
67		mblvol	$⊢ {(F \times_{f} G)}^{-1} [\{y\}] \in dom vol \to vol ({(F \times_{f} G)}^{-1} [\{y\}]) = {vol}^{*} ({(F \times_{f} G)}^{-1} [\{y\}])$
68	66 67	syl	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to vol ({(F \times_{f} G)}^{-1} [\{y\}]) = {vol}^{*} ({(F \times_{f} G)}^{-1} [\{y\}])$
69		mblss	$⊢ {(F \times_{f} G)}^{-1} [\{y\}] \in dom vol \to {(F \times_{f} G)}^{-1} [\{y\}] \subseteq ℝ$
70	66 69	syl	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to {(F \times_{f} G)}^{-1} [\{y\}] \subseteq ℝ$
71	55	adantr	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to ran G ∖ \{0\} \in Fin$
72		inss2	$⊢ F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq G^{-1} [\{z\}]$
73	72	a1i	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq G^{-1} [\{z\}]$
74	59	ad2antrr	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to G^{-1} [\{z\}] \in dom vol$
75		mblss	$⊢ G^{-1} [\{z\}] \in dom vol \to G^{-1} [\{z\}] \subseteq ℝ$
76	74 75	syl	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to G^{-1} [\{z\}] \subseteq ℝ$
77		mblvol	$⊢ G^{-1} [\{z\}] \in dom vol \to vol (G^{-1} [\{z\}]) = {vol}^{*} (G^{-1} [\{z\}])$
78	74 77	syl	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{z\}]) = {vol}^{*} (G^{-1} [\{z\}])$
79	2	adantr	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to G \in dom \int^{1}$
80		i1fima2sn	$⊢ (G \in dom \int^{1} \land z \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{z\}]) \in ℝ$
81	79 80	sylan	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{z\}]) \in ℝ$
82	78 81	eqeltrrd	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to {vol}^{*} (G^{-1} [\{z\}]) \in ℝ$
83		ovolsscl	$⊢ (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq G^{-1} [\{z\}] \land G^{-1} [\{z\}] \subseteq ℝ \land {vol}^{} (G^{-1} [\{z\}]) \in ℝ) \to {vol}^{} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in ℝ$
84	73 76 82 83	syl3anc	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to {vol}^{*} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in ℝ$
85	71 84	fsumrecl	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to \sum_{z \in ran G ∖ \{0\}} {vol}^{*} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in ℝ$
86	52	fveq2d	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to {vol}^{} ({(F \times_{f} G)}^{-1} [\{y\}]) = {vol}^{} (⋃_{z \in ran G ∖ \{0\}} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]))$
87		mblss	$⊢ F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \in dom vol \to F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq ℝ$
88	61 87	syl	$⊢ φ \to F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq ℝ$
89	88	ad2antrr	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq ℝ$
90	89 84	jca	$⊢ ((φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq ℝ \land {vol}^{*} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in ℝ)$
91	90	ralrimiva	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to \forall z \in (ran G ∖ \{0\}) (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq ℝ \land {vol}^{*} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in ℝ)$
92		ovolfiniun	$⊢ (ran G ∖ \{0\} \in Fin \land \forall z \in (ran G ∖ \{0\}) (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}] \subseteq ℝ \land {vol}^{} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in ℝ)) \to {vol}^{} (⋃_{z \in ran G ∖ \{0\}} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}])) \leq \sum_{z \in ran G ∖ \{0\}} {vol}^{*} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}])$
93	71 91 92	syl2anc	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to {vol}^{} (⋃_{z \in ran G ∖ \{0\}} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}])) \leq \sum_{z \in ran G ∖ \{0\}} {vol}^{} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}])$
94	86 93	eqbrtrd	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to {vol}^{} ({(F \times_{f} G)}^{-1} [\{y\}]) \leq \sum_{z \in ran G ∖ \{0\}} {vol}^{} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}])$
95		ovollecl	$⊢ ({(F \times_{f} G)}^{-1} [\{y\}] \subseteq ℝ \land \sum_{z \in ran G ∖ \{0\}} {vol}^{} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}]) \in ℝ \land {vol}^{} ({(F \times_{f} G)}^{-1} [\{y\}]) \leq \sum_{z \in ran G ∖ \{0\}} {vol}^{} (F^{-1} [\{\frac{y}{z}\}] \cap G^{-1} [\{z\}])) \to {vol}^{} ({(F \times_{f} G)}^{-1} [\{y\}]) \in ℝ$
96	70 85 94 95	syl3anc	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to {vol}^{*} ({(F \times_{f} G)}^{-1} [\{y\}]) \in ℝ$
97	68 96	eqeltrd	$⊢ (φ \land y \in (ran (F \times_{f} G) ∖ \{0\})) \to vol ({(F \times_{f} G)}^{-1} [\{y\}]) \in ℝ$
98	12 45 66 97	i1fd	$⊢ φ \to F \times_{f} G \in dom \int^{1}$

Metamath Proof Explorer

Theorem i1fmul

Proof