i1fadd

Description: The sum of two simple functions is a simple function. (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Hypotheses	i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
	i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
Assertion	i1fadd	$⊢ φ \to F +_{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		readdcl	$⊢ (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 +_{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 +_{f} G) : ℝ ⟶ \{w \| \exists u \in ran F \exists v \in ran G w = u + v\}$
42	41	frnd	$⊢ φ \to ran (F +_{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 +_{f} G) \subseteq ran (u \in ran F, v \in ran G ⟼ u + v)$
45	25 44	ssfid	$⊢ φ \to ran (F +_{f} G) \in Fin$
46	12	frnd	$⊢ φ \to ran (F +_{f} G) \subseteq ℝ$
47	46	ssdifssd	$⊢ φ \to ran (F +_{f} G) ∖ \{0\} \subseteq ℝ$
48	47	sselda	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to y \in ℝ$
49	48	recnd	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to y \in ℂ$
50	1 2	i1faddlem	$⊢ (φ \land y \in ℂ) \to {(F +_{f} G)}^{-1} [\{y\}] = ⋃_{z \in ran G} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}])$
51	49 50	syldan	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to {(F +_{f} G)}^{-1} [\{y\}] = ⋃_{z \in ran G} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}])$
52	16	adantr	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to ran G \in Fin$
53	1	ad2antrr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to F \in dom \int^{1}$
54		i1fmbf	$⊢ F \in dom \int^{1} \to F \in MblFn$
55	53 54	syl	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to F \in MblFn$
56	6	ad2antrr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to F : ℝ ⟶ ℝ$
57	12	ad2antrr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to (F +_{f} G) : ℝ ⟶ ℝ$
58	57	frnd	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to ran (F +_{f} G) \subseteq ℝ$
59		eldifi	$⊢ y \in (ran (F +_{f} G) ∖ \{0\}) \to y \in ran (F +_{f} G)$
60	59	ad2antlr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to y \in ran (F +_{f} G)$
61	58 60	sseldd	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to y \in ℝ$
62	8	adantr	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to G : ℝ ⟶ ℝ$
63	62	frnd	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to ran G \subseteq ℝ$
64	63	sselda	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to z \in ℝ$
65	61 64	resubcld	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to y - z \in ℝ$
66		mbfimasn	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ \land y - z \in ℝ) \to F^{-1} [\{y - z\}] \in dom vol$
67	55 56 65 66	syl3anc	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to F^{-1} [\{y - z\}] \in dom vol$
68	2	ad2antrr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to G \in dom \int^{1}$
69		i1fmbf	$⊢ G \in dom \int^{1} \to G \in MblFn$
70	68 69	syl	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to G \in MblFn$
71	8	ad2antrr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to G : ℝ ⟶ ℝ$
72		mbfimasn	$⊢ (G \in MblFn \land G : ℝ ⟶ ℝ \land z \in ℝ) \to G^{-1} [\{z\}] \in dom vol$
73	70 71 64 72	syl3anc	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to G^{-1} [\{z\}] \in dom vol$
74		inmbl	$⊢ (F^{-1} [\{y - z\}] \in dom vol \land G^{-1} [\{z\}] \in dom vol) \to F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \in dom vol$
75	67 73 74	syl2anc	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \in dom vol$
76	75	ralrimiva	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to \forall z \in ran G F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \in dom vol$
77		finiunmbl	$⊢ (ran G \in Fin \land \forall z \in ran G F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \in dom vol) \to ⋃_{z \in ran G} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in dom vol$
78	52 76 77	syl2anc	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to ⋃_{z \in ran G} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in dom vol$
79	51 78	eqeltrd	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to {(F +_{f} G)}^{-1} [\{y\}] \in dom vol$
80		mblvol	$⊢ {(F +_{f} G)}^{-1} [\{y\}] \in dom vol \to vol ({(F +_{f} G)}^{-1} [\{y\}]) = {vol}^{*} ({(F +_{f} G)}^{-1} [\{y\}])$
81	79 80	syl	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to vol ({(F +_{f} G)}^{-1} [\{y\}]) = {vol}^{*} ({(F +_{f} G)}^{-1} [\{y\}])$
82		mblss	$⊢ {(F +_{f} G)}^{-1} [\{y\}] \in dom vol \to {(F +_{f} G)}^{-1} [\{y\}] \subseteq ℝ$
83	79 82	syl	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to {(F +_{f} G)}^{-1} [\{y\}] \subseteq ℝ$
84		inss1	$⊢ F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \subseteq F^{-1} [\{y - z\}]$
85	67	adantrr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to F^{-1} [\{y - z\}] \in dom vol$
86		mblss	$⊢ F^{-1} [\{y - z\}] \in dom vol \to F^{-1} [\{y - z\}] \subseteq ℝ$
87	85 86	syl	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to F^{-1} [\{y - z\}] \subseteq ℝ$
88		mblvol	$⊢ F^{-1} [\{y - z\}] \in dom vol \to vol (F^{-1} [\{y - z\}]) = {vol}^{*} (F^{-1} [\{y - z\}])$
89	85 88	syl	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to vol (F^{-1} [\{y - z\}]) = {vol}^{*} (F^{-1} [\{y - z\}])$
90		simprr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to z = 0$
91	90	oveq2d	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to y - z = y - 0$
92	49	adantr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to y \in ℂ$
93	92	subid1d	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to y - 0 = y$
94	91 93	eqtrd	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to y - z = y$
95	94	sneqd	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to \{y - z\} = \{y\}$
96	95	imaeq2d	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to F^{-1} [\{y - z\}] = F^{-1} [\{y\}]$
97	96	fveq2d	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to vol (F^{-1} [\{y - z\}]) = vol (F^{-1} [\{y\}])$
98		i1fima2sn	$⊢ (F \in dom \int^{1} \land y \in (ran (F +_{f} G) ∖ \{0\})) \to vol (F^{-1} [\{y\}]) \in ℝ$
99	1 98	sylan	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to vol (F^{-1} [\{y\}]) \in ℝ$
100	99	adantr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to vol (F^{-1} [\{y\}]) \in ℝ$
101	97 100	eqeltrd	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to vol (F^{-1} [\{y - z\}]) \in ℝ$
102	89 101	eqeltrrd	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to {vol}^{*} (F^{-1} [\{y - z\}]) \in ℝ$
103		ovolsscl	$⊢ (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \subseteq F^{-1} [\{y - z\}] \land F^{-1} [\{y - z\}] \subseteq ℝ \land {vol}^{} (F^{-1} [\{y - z\}]) \in ℝ) \to {vol}^{} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ$
104	84 87 102 103	mp3an2i	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z = 0)) \to {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ$
105	104	expr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to (z = 0 \to {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ)$
106		eldifsn	$⊢ z \in (ran G ∖ \{0\}) \leftrightarrow (z \in ran G \land z \neq 0)$
107		inss2	$⊢ F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \subseteq G^{-1} [\{z\}]$
108		eldifi	$⊢ z \in (ran G ∖ \{0\}) \to z \in ran G$
109		mblss	$⊢ G^{-1} [\{z\}] \in dom vol \to G^{-1} [\{z\}] \subseteq ℝ$
110	73 109	syl	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to G^{-1} [\{z\}] \subseteq ℝ$
111	108 110	sylan2	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to G^{-1} [\{z\}] \subseteq ℝ$
112		i1fima	$⊢ G \in dom \int^{1} \to G^{-1} [\{z\}] \in dom vol$
113	2 112	syl	$⊢ φ \to G^{-1} [\{z\}] \in dom vol$
114	113	ad2antrr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to G^{-1} [\{z\}] \in dom vol$
115		mblvol	$⊢ G^{-1} [\{z\}] \in dom vol \to vol (G^{-1} [\{z\}]) = {vol}^{*} (G^{-1} [\{z\}])$
116	114 115	syl	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{z\}]) = {vol}^{*} (G^{-1} [\{z\}])$
117	2	adantr	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to G \in dom \int^{1}$
118		i1fima2sn	$⊢ (G \in dom \int^{1} \land z \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{z\}]) \in ℝ$
119	117 118	sylan	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{z\}]) \in ℝ$
120	116 119	eqeltrrd	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to {vol}^{*} (G^{-1} [\{z\}]) \in ℝ$
121		ovolsscl	$⊢ (F^{-1} [\{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} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ$
122	107 111 120 121	mp3an2i	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in (ran G ∖ \{0\})) \to {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ$
123	106 122	sylan2br	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land (z \in ran G \land z \neq 0)) \to {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ$
124	123	expr	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to (z \neq 0 \to {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ)$
125	105 124	pm2.61dne	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ$
126	52 125	fsumrecl	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to \sum_{z \in ran G} {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ$
127	51	fveq2d	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to {vol}^{} ({(F +_{f} G)}^{-1} [\{y\}]) = {vol}^{} (⋃_{z \in ran G} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]))$
128	107 110	sstrid	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \subseteq ℝ$
129	128 125	jca	$⊢ ((φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \land z \in ran G) \to (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \subseteq ℝ \land {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ)$
130	129	ralrimiva	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to \forall z \in ran G (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \subseteq ℝ \land {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ)$
131		ovolfiniun	$⊢ (ran G \in Fin \land \forall z \in ran G (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}] \subseteq ℝ \land {vol}^{} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ)) \to {vol}^{} (⋃_{z \in ran G} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}])) \leq \sum_{z \in ran G} {vol}^{*} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}])$
132	52 130 131	syl2anc	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to {vol}^{} (⋃_{z \in ran G} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}])) \leq \sum_{z \in ran G} {vol}^{} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}])$
133	127 132	eqbrtrd	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to {vol}^{} ({(F +_{f} G)}^{-1} [\{y\}]) \leq \sum_{z \in ran G} {vol}^{} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}])$
134		ovollecl	$⊢ ({(F +_{f} G)}^{-1} [\{y\}] \subseteq ℝ \land \sum_{z \in ran G} {vol}^{} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}]) \in ℝ \land {vol}^{} ({(F +_{f} G)}^{-1} [\{y\}]) \leq \sum_{z \in ran G} {vol}^{} (F^{-1} [\{y - z\}] \cap G^{-1} [\{z\}])) \to {vol}^{} ({(F +_{f} G)}^{-1} [\{y\}]) \in ℝ$
135	83 126 133 134	syl3anc	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to {vol}^{*} ({(F +_{f} G)}^{-1} [\{y\}]) \in ℝ$
136	81 135	eqeltrd	$⊢ (φ \land y \in (ran (F +_{f} G) ∖ \{0\})) \to vol ({(F +_{f} G)}^{-1} [\{y\}]) \in ℝ$
137	12 45 79 136	i1fd	$⊢ φ \to F +_{f} G \in dom \int^{1}$

Metamath Proof Explorer

Theorem i1fadd

Proof