itg1addlem4

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Hypotheses	i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
	i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
	itg1add.3	$⊢ I = (i \in ℝ, j \in ℝ ⟼ if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])))$
	itg1add.4	$⊢ P = {+ ↾}_{(ran F \times ran G)}$
Assertion	itg1addlem4	$⊢ φ \to \int^{1} (F +_{f} G) = \sum_{y \in ran F} \sum_{z \in ran G} (y + z) (y I z)$

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
2		i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
3		itg1add.3	$⊢ I = (i \in ℝ, j \in ℝ ⟼ if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])))$
4		itg1add.4	$⊢ P = {+ ↾}_{(ran F \times ran G)}$
5	1 2	i1fadd	$⊢ φ \to F +_{f} G \in dom \int^{1}$
6		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
7	1 6	syl	$⊢ φ \to ran F \in Fin$
8		i1frn	$⊢ G \in dom \int^{1} \to ran G \in Fin$
9	2 8	syl	$⊢ φ \to ran G \in Fin$
10		xpfi	$⊢ (ran F \in Fin \land ran G \in Fin) \to ran F \times ran G \in Fin$
11	7 9 10	syl2anc	$⊢ φ \to ran F \times ran G \in Fin$
12		ax-addf	$⊢ + : ℂ \times ℂ ⟶ ℂ$
13		ffn	$⊢ + : ℂ \times ℂ ⟶ ℂ \to + Fn (ℂ \times ℂ)$
14	12 13	ax-mp	$⊢ + Fn (ℂ \times ℂ)$
15		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
16	1 15	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
17	16	frnd	$⊢ φ \to ran F \subseteq ℝ$
18		ax-resscn	$⊢ ℝ \subseteq ℂ$
19	17 18	sstrdi	$⊢ φ \to ran F \subseteq ℂ$
20		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
21	2 20	syl	$⊢ φ \to G : ℝ ⟶ ℝ$
22	21	frnd	$⊢ φ \to ran G \subseteq ℝ$
23	22 18	sstrdi	$⊢ φ \to ran G \subseteq ℂ$
24		xpss12	$⊢ (ran F \subseteq ℂ \land ran G \subseteq ℂ) \to ran F \times ran G \subseteq ℂ \times ℂ$
25	19 23 24	syl2anc	$⊢ φ \to ran F \times ran G \subseteq ℂ \times ℂ$
26		fnssres	$⊢ (+ Fn (ℂ \times ℂ) \land ran F \times ran G \subseteq ℂ \times ℂ) \to ({+ ↾}_{(ran F \times ran G)}) Fn (ran F \times ran G)$
27	14 25 26	sylancr	$⊢ φ \to ({+ ↾}_{(ran F \times ran G)}) Fn (ran F \times ran G)$
28	4	fneq1i	$⊢ P Fn (ran F \times ran G) \leftrightarrow ({+ ↾}_{(ran F \times ran G)}) Fn (ran F \times ran G)$
29	27 28	sylibr	$⊢ φ \to P Fn (ran F \times ran G)$
30		dffn4	$⊢ P Fn (ran F \times ran G) \leftrightarrow P : ran F \times ran G \underset{onto}{⟶} ran P$
31	29 30	sylib	$⊢ φ \to P : ran F \times ran G \underset{onto}{⟶} ran P$
32		fofi	$⊢ (ran F \times ran G \in Fin \land P : ran F \times ran G \underset{onto}{⟶} ran P) \to ran P \in Fin$
33	11 31 32	syl2anc	$⊢ φ \to ran P \in Fin$
34		difss	$⊢ ran P ∖ \{0\} \subseteq ran P$
35		ssfi	$⊢ (ran P \in Fin \land ran P ∖ \{0\} \subseteq ran P) \to ran P ∖ \{0\} \in Fin$
36	33 34 35	sylancl	$⊢ φ \to ran P ∖ \{0\} \in Fin$
37		ffun	$⊢ + : ℂ \times ℂ ⟶ ℂ \to Fun +$
38	12 37	ax-mp	$⊢ Fun +$
39	12	fdmi	$⊢ dom + = ℂ \times ℂ$
40	25 39	sseqtrrdi	$⊢ φ \to ran F \times ran G \subseteq dom +$
41		funfvima2	$⊢ (Fun + \land ran F \times ran G \subseteq dom +) \to (⟨x, y⟩ \in (ran F \times ran G) \to + (⟨x, y⟩) \in + [ran F \times ran G])$
42	38 40 41	sylancr	$⊢ φ \to (⟨x, y⟩ \in (ran F \times ran G) \to + (⟨x, y⟩) \in + [ran F \times ran G])$
43		opelxpi	$⊢ (x \in ran F \land y \in ran G) \to ⟨x, y⟩ \in (ran F \times ran G)$
44	42 43	impel	$⊢ (φ \land (x \in ran F \land y \in ran G)) \to + (⟨x, y⟩) \in + [ran F \times ran G]$
45		df-ov	$⊢ x + y = + (⟨x, y⟩)$
46	4	rneqi	$⊢ ran P = ran ({+ ↾}_{(ran F \times ran G)})$
47		df-ima	$⊢ + [ran F \times ran G] = ran ({+ ↾}_{(ran F \times ran G)})$
48	46 47	eqtr4i	$⊢ ran P = + [ran F \times ran G]$
49	44 45 48	3eltr4g	$⊢ (φ \land (x \in ran F \land y \in ran G)) \to x + y \in ran P$
50	16	ffnd	$⊢ φ \to F Fn ℝ$
51		dffn3	$⊢ F Fn ℝ \leftrightarrow F : ℝ ⟶ ran F$
52	50 51	sylib	$⊢ φ \to F : ℝ ⟶ ran F$
53	21	ffnd	$⊢ φ \to G Fn ℝ$
54		dffn3	$⊢ G Fn ℝ \leftrightarrow G : ℝ ⟶ ran G$
55	53 54	sylib	$⊢ φ \to G : ℝ ⟶ ran G$
56		reex	$⊢ ℝ \in V$
57	56	a1i	$⊢ φ \to ℝ \in V$
58		inidm	$⊢ ℝ \cap ℝ = ℝ$
59	49 52 55 57 57 58	off	$⊢ φ \to (F +_{f} G) : ℝ ⟶ ran P$
60	59	frnd	$⊢ φ \to ran (F +_{f} G) \subseteq ran P$
61	60	ssdifd	$⊢ φ \to ran (F +_{f} G) ∖ \{0\} \subseteq ran P ∖ \{0\}$
62	17	sselda	$⊢ (φ \land y \in ran F) \to y \in ℝ$
63	22	sselda	$⊢ (φ \land z \in ran G) \to z \in ℝ$
64	62 63	anim12dan	$⊢ (φ \land (y \in ran F \land z \in ran G)) \to (y \in ℝ \land z \in ℝ)$
65		readdcl	$⊢ (y \in ℝ \land z \in ℝ) \to y + z \in ℝ$
66	64 65	syl	$⊢ (φ \land (y \in ran F \land z \in ran G)) \to y + z \in ℝ$
67	66	ralrimivva	$⊢ φ \to \forall y \in ran F \forall z \in ran G y + z \in ℝ$
68		funimassov	$⊢ (Fun + \land ran F \times ran G \subseteq dom +) \to (+ [ran F \times ran G] \subseteq ℝ \leftrightarrow \forall y \in ran F \forall z \in ran G y + z \in ℝ)$
69	38 40 68	sylancr	$⊢ φ \to (+ [ran F \times ran G] \subseteq ℝ \leftrightarrow \forall y \in ran F \forall z \in ran G y + z \in ℝ)$
70	67 69	mpbird	$⊢ φ \to + [ran F \times ran G] \subseteq ℝ$
71	48 70	eqsstrid	$⊢ φ \to ran P \subseteq ℝ$
72	71	ssdifd	$⊢ φ \to ran P ∖ \{0\} \subseteq ℝ ∖ \{0\}$
73		itg1val2	$⊢ (F +_{f} G \in dom \int^{1} \land (ran P ∖ \{0\} \in Fin \land ran (F +_{f} G) ∖ \{0\} \subseteq ran P ∖ \{0\} \land ran P ∖ \{0\} \subseteq ℝ ∖ \{0\})) \to \int^{1} (F +_{f} G) = \sum_{w \in ran P ∖ \{0\}} w vol ({(F +_{f} G)}^{-1} [\{w\}])$
74	5 36 61 72 73	syl13anc	$⊢ φ \to \int^{1} (F +_{f} G) = \sum_{w \in ran P ∖ \{0\}} w vol ({(F +_{f} G)}^{-1} [\{w\}])$
75	21	adantr	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to G : ℝ ⟶ ℝ$
76	9	adantr	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to ran G \in Fin$
77		inss2	$⊢ F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}] \subseteq G^{-1} [\{z\}]$
78	77	a1i	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}] \subseteq G^{-1} [\{z\}]$
79		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{w - z\}] \in dom vol$
80	1 79	syl	$⊢ φ \to F^{-1} [\{w - z\}] \in dom vol$
81		i1fima	$⊢ G \in dom \int^{1} \to G^{-1} [\{z\}] \in dom vol$
82	2 81	syl	$⊢ φ \to G^{-1} [\{z\}] \in dom vol$
83		inmbl	$⊢ (F^{-1} [\{w - z\}] \in dom vol \land G^{-1} [\{z\}] \in dom vol) \to F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}] \in dom vol$
84	80 82 83	syl2anc	$⊢ φ \to F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}] \in dom vol$
85	84	ad2antrr	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}] \in dom vol$
86	34 71	sstrid	$⊢ φ \to ran P ∖ \{0\} \subseteq ℝ$
87	86	sselda	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to w \in ℝ$
88	87	adantr	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to w \in ℝ$
89	63	adantlr	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to z \in ℝ$
90	88 89	resubcld	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to w - z \in ℝ$
91	88	recnd	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to w \in ℂ$
92	89	recnd	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to z \in ℂ$
93	91 92	npcand	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to w - z + z = w$
94		eldifsni	$⊢ w \in (ran P ∖ \{0\}) \to w \neq 0$
95	94	ad2antlr	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to w \neq 0$
96	93 95	eqnetrd	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to w - z + z \neq 0$
97		oveq12	$⊢ (w - z = 0 \land z = 0) \to w - z + z = 0 + 0$
98		00id	$⊢ 0 + 0 = 0$
99	97 98	eqtrdi	$⊢ (w - z = 0 \land z = 0) \to w - z + z = 0$
100	99	necon3ai	$⊢ w - z + z \neq 0 \to \neg (w - z = 0 \land z = 0)$
101	96 100	syl	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to \neg (w - z = 0 \land z = 0)$
102	1 2 3	itg1addlem3	$⊢ ((w - z \in ℝ \land z \in ℝ) \land \neg (w - z = 0 \land z = 0)) \to (w - z) I z = vol (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}])$
103	90 89 101 102	syl21anc	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to (w - z) I z = vol (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}])$
104	1 2 3	itg1addlem2	$⊢ φ \to I : ℝ^{2} ⟶ ℝ$
105	104	ad2antrr	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to I : ℝ^{2} ⟶ ℝ$
106	105 90 89	fovrnd	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to (w - z) I z \in ℝ$
107	103 106	eqeltrrd	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to vol (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}]) \in ℝ$
108	75 76 78 85 107	itg1addlem1	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to vol (⋃_{z \in ran G} (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}])) = \sum_{z \in ran G} vol (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}])$
109	87	recnd	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to w \in ℂ$
110	1 2	i1faddlem	$⊢ (φ \land w \in ℂ) \to {(F +_{f} G)}^{-1} [\{w\}] = ⋃_{z \in ran G} (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}])$
111	109 110	syldan	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to {(F +_{f} G)}^{-1} [\{w\}] = ⋃_{z \in ran G} (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}])$
112	111	fveq2d	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to vol ({(F +_{f} G)}^{-1} [\{w\}]) = vol (⋃_{z \in ran G} (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}]))$
113	103	sumeq2dv	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to \sum_{z \in ran G} ((w - z) I z) = \sum_{z \in ran G} vol (F^{-1} [\{w - z\}] \cap G^{-1} [\{z\}])$
114	108 112 113	3eqtr4d	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to vol ({(F +_{f} G)}^{-1} [\{w\}]) = \sum_{z \in ran G} ((w - z) I z)$
115	114	oveq2d	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to w vol ({(F +_{f} G)}^{-1} [\{w\}]) = w \sum_{z \in ran G} ((w - z) I z)$
116	106	recnd	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to (w - z) I z \in ℂ$
117	76 109 116	fsummulc2	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to w \sum_{z \in ran G} ((w - z) I z) = \sum_{z \in ran G} w ((w - z) I z)$
118	115 117	eqtrd	$⊢ (φ \land w \in (ran P ∖ \{0\})) \to w vol ({(F +_{f} G)}^{-1} [\{w\}]) = \sum_{z \in ran G} w ((w - z) I z)$
119	118	sumeq2dv	$⊢ φ \to \sum_{w \in ran P ∖ \{0\}} w vol ({(F +_{f} G)}^{-1} [\{w\}]) = \sum_{w \in ran P ∖ \{0\}} \sum_{z \in ran G} w ((w - z) I z)$
120	91 116	mulcld	$⊢ ((φ \land w \in (ran P ∖ \{0\})) \land z \in ran G) \to w ((w - z) I z) \in ℂ$
121	120	anasss	$⊢ (φ \land (w \in (ran P ∖ \{0\}) \land z \in ran G)) \to w ((w - z) I z) \in ℂ$
122	36 9 121	fsumcom	$⊢ φ \to \sum_{w \in ran P ∖ \{0\}} \sum_{z \in ran G} w ((w - z) I z) = \sum_{z \in ran G} \sum_{w \in ran P ∖ \{0\}} w ((w - z) I z)$
123	74 119 122	3eqtrd	$⊢ φ \to \int^{1} (F +_{f} G) = \sum_{z \in ran G} \sum_{w \in ran P ∖ \{0\}} w ((w - z) I z)$
124		oveq1	$⊢ y = w - z \to y + z = w - z + z$
125		oveq1	$⊢ y = w - z \to y I z = (w - z) I z$
126	124 125	oveq12d	$⊢ y = w - z \to (y + z) (y I z) = (w - z + z) ((w - z) I z)$
127	33	adantr	$⊢ (φ \land z \in ran G) \to ran P \in Fin$
128	71	adantr	$⊢ (φ \land z \in ran G) \to ran P \subseteq ℝ$
129	128	sselda	$⊢ ((φ \land z \in ran G) \land v \in ran P) \to v \in ℝ$
130	63	adantr	$⊢ ((φ \land z \in ran G) \land v \in ran P) \to z \in ℝ$
131	129 130	resubcld	$⊢ ((φ \land z \in ran G) \land v \in ran P) \to v - z \in ℝ$
132	131	ex	$⊢ (φ \land z \in ran G) \to (v \in ran P \to v - z \in ℝ)$
133	129	recnd	$⊢ ((φ \land z \in ran G) \land v \in ran P) \to v \in ℂ$
134	133	adantrr	$⊢ ((φ \land z \in ran G) \land (v \in ran P \land y \in ran P)) \to v \in ℂ$
135	71	sselda	$⊢ (φ \land y \in ran P) \to y \in ℝ$
136	135	ad2ant2rl	$⊢ ((φ \land z \in ran G) \land (v \in ran P \land y \in ran P)) \to y \in ℝ$
137	136	recnd	$⊢ ((φ \land z \in ran G) \land (v \in ran P \land y \in ran P)) \to y \in ℂ$
138	63	recnd	$⊢ (φ \land z \in ran G) \to z \in ℂ$
139	138	adantr	$⊢ ((φ \land z \in ran G) \land (v \in ran P \land y \in ran P)) \to z \in ℂ$
140	134 137 139	subcan2ad	$⊢ ((φ \land z \in ran G) \land (v \in ran P \land y \in ran P)) \to (v - z = y - z \leftrightarrow v = y)$
141	140	ex	$⊢ (φ \land z \in ran G) \to ((v \in ran P \land y \in ran P) \to (v - z = y - z \leftrightarrow v = y))$
142	132 141	dom2lem	$⊢ (φ \land z \in ran G) \to (v \in ran P ⟼ v - z) : ran P \underset{1-1}{⟶} ℝ$
143		f1f1orn	$⊢ (v \in ran P ⟼ v - z) : ran P \underset{1-1}{⟶} ℝ \to (v \in ran P ⟼ v - z) : ran P \underset{1-1 onto}{⟶} ran (v \in ran P ⟼ v - z)$
144	142 143	syl	$⊢ (φ \land z \in ran G) \to (v \in ran P ⟼ v - z) : ran P \underset{1-1 onto}{⟶} ran (v \in ran P ⟼ v - z)$
145		oveq1	$⊢ v = w \to v - z = w - z$
146		eqid	$⊢ (v \in ran P ⟼ v - z) = (v \in ran P ⟼ v - z)$
147		ovex	$⊢ w - z \in V$
148	145 146 147	fvmpt	$⊢ w \in ran P \to (v \in ran P ⟼ v - z) (w) = w - z$
149	148	adantl	$⊢ ((φ \land z \in ran G) \land w \in ran P) \to (v \in ran P ⟼ v - z) (w) = w - z$
150		f1f	$⊢ (v \in ran P ⟼ v - z) : ran P \underset{1-1}{⟶} ℝ \to (v \in ran P ⟼ v - z) : ran P ⟶ ℝ$
151		frn	$⊢ (v \in ran P ⟼ v - z) : ran P ⟶ ℝ \to ran (v \in ran P ⟼ v - z) \subseteq ℝ$
152	142 150 151	3syl	$⊢ (φ \land z \in ran G) \to ran (v \in ran P ⟼ v - z) \subseteq ℝ$
153	152	sselda	$⊢ ((φ \land z \in ran G) \land y \in ran (v \in ran P ⟼ v - z)) \to y \in ℝ$
154	63	adantr	$⊢ ((φ \land z \in ran G) \land y \in ran (v \in ran P ⟼ v - z)) \to z \in ℝ$
155	153 154	readdcld	$⊢ ((φ \land z \in ran G) \land y \in ran (v \in ran P ⟼ v - z)) \to y + z \in ℝ$
156	104	ad2antrr	$⊢ ((φ \land z \in ran G) \land y \in ran (v \in ran P ⟼ v - z)) \to I : ℝ^{2} ⟶ ℝ$
157	156 153 154	fovrnd	$⊢ ((φ \land z \in ran G) \land y \in ran (v \in ran P ⟼ v - z)) \to y I z \in ℝ$
158	155 157	remulcld	$⊢ ((φ \land z \in ran G) \land y \in ran (v \in ran P ⟼ v - z)) \to (y + z) (y I z) \in ℝ$
159	158	recnd	$⊢ ((φ \land z \in ran G) \land y \in ran (v \in ran P ⟼ v - z)) \to (y + z) (y I z) \in ℂ$
160	126 127 144 149 159	fsumf1o	$⊢ (φ \land z \in ran G) \to \sum_{y \in ran (v \in ran P ⟼ v - z)} (y + z) (y I z) = \sum_{w \in ran P} (w - z + z) ((w - z) I z)$
161	128	sselda	$⊢ ((φ \land z \in ran G) \land w \in ran P) \to w \in ℝ$
162	161	recnd	$⊢ ((φ \land z \in ran G) \land w \in ran P) \to w \in ℂ$
163	138	adantr	$⊢ ((φ \land z \in ran G) \land w \in ran P) \to z \in ℂ$
164	162 163	npcand	$⊢ ((φ \land z \in ran G) \land w \in ran P) \to w - z + z = w$
165	164	oveq1d	$⊢ ((φ \land z \in ran G) \land w \in ran P) \to (w - z + z) ((w - z) I z) = w ((w - z) I z)$
166	165	sumeq2dv	$⊢ (φ \land z \in ran G) \to \sum_{w \in ran P} (w - z + z) ((w - z) I z) = \sum_{w \in ran P} w ((w - z) I z)$
167	160 166	eqtrd	$⊢ (φ \land z \in ran G) \to \sum_{y \in ran (v \in ran P ⟼ v - z)} (y + z) (y I z) = \sum_{w \in ran P} w ((w - z) I z)$
168	40	ad2antrr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to ran F \times ran G \subseteq dom +$
169		simpr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y \in ran F$
170		simplr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to z \in ran G$
171	169 170	opelxpd	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to ⟨y, z⟩ \in (ran F \times ran G)$
172		funfvima2	$⊢ (Fun + \land ran F \times ran G \subseteq dom +) \to (⟨y, z⟩ \in (ran F \times ran G) \to + (⟨y, z⟩) \in + [ran F \times ran G])$
173	38 172	mpan	$⊢ ran F \times ran G \subseteq dom + \to (⟨y, z⟩ \in (ran F \times ran G) \to + (⟨y, z⟩) \in + [ran F \times ran G])$
174	168 171 173	sylc	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to + (⟨y, z⟩) \in + [ran F \times ran G]$
175		df-ov	$⊢ y + z = + (⟨y, z⟩)$
176	174 175 48	3eltr4g	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y + z \in ran P$
177	62	adantlr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y \in ℝ$
178	177	recnd	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y \in ℂ$
179	138	adantr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to z \in ℂ$
180	178 179	pncand	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y + z - z = y$
181	180	eqcomd	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y = y + z - z$
182		oveq1	$⊢ v = y + z \to v - z = y + z - z$
183	182	rspceeqv	$⊢ (y + z \in ran P \land y = y + z - z) \to \exists v \in ran P y = v - z$
184	176 181 183	syl2anc	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to \exists v \in ran P y = v - z$
185	184	ralrimiva	$⊢ (φ \land z \in ran G) \to \forall y \in ran F \exists v \in ran P y = v - z$
186		ssabral	$⊢ ran F \subseteq \{y \| \exists v \in ran P y = v - z\} \leftrightarrow \forall y \in ran F \exists v \in ran P y = v - z$
187	185 186	sylibr	$⊢ (φ \land z \in ran G) \to ran F \subseteq \{y \| \exists v \in ran P y = v - z\}$
188	146	rnmpt	$⊢ ran (v \in ran P ⟼ v - z) = \{y \| \exists v \in ran P y = v - z\}$
189	187 188	sseqtrrdi	$⊢ (φ \land z \in ran G) \to ran F \subseteq ran (v \in ran P ⟼ v - z)$
190	63	adantr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to z \in ℝ$
191	177 190	readdcld	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y + z \in ℝ$
192	104	ad2antrr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to I : ℝ^{2} ⟶ ℝ$
193	192 177 190	fovrnd	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y I z \in ℝ$
194	191 193	remulcld	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to (y + z) (y I z) \in ℝ$
195	194	recnd	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to (y + z) (y I z) \in ℂ$
196	152	ssdifd	$⊢ (φ \land z \in ran G) \to ran (v \in ran P ⟼ v - z) ∖ ran F \subseteq ℝ ∖ ran F$
197	196	sselda	$⊢ ((φ \land z \in ran G) \land y \in (ran (v \in ran P ⟼ v - z) ∖ ran F)) \to y \in (ℝ ∖ ran F)$
198		eldifi	$⊢ y \in (ℝ ∖ ran F) \to y \in ℝ$
199	198	ad2antrl	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to y \in ℝ$
200	63	adantr	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to z \in ℝ$
201		simprr	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to \neg (y = 0 \land z = 0)$
202	1 2 3	itg1addlem3	$⊢ ((y \in ℝ \land z \in ℝ) \land \neg (y = 0 \land z = 0)) \to y I z = vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
203	199 200 201 202	syl21anc	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to y I z = vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
204		inss1	$⊢ F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \subseteq F^{-1} [\{y\}]$
205		eldifn	$⊢ y \in (ℝ ∖ ran F) \to \neg y \in ran F$
206	205	ad2antrl	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to \neg y \in ran F$
207		vex	$⊢ v \in V$
208	207	eliniseg	$⊢ y \in V \to (v \in F^{-1} [\{y\}] \leftrightarrow v F y)$
209	208	elv	$⊢ v \in F^{-1} [\{y\}] \leftrightarrow v F y$
210		vex	$⊢ y \in V$
211	207 210	brelrn	$⊢ v F y \to y \in ran F$
212	209 211	sylbi	$⊢ v \in F^{-1} [\{y\}] \to y \in ran F$
213	206 212	nsyl	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to \neg v \in F^{-1} [\{y\}]$
214	213	pm2.21d	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to (v \in F^{-1} [\{y\}] \to v \in \emptyset)$
215	214	ssrdv	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to F^{-1} [\{y\}] \subseteq \emptyset$
216	204 215	sstrid	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \subseteq \emptyset$
217		ss0	$⊢ F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \subseteq \emptyset \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] = \emptyset$
218	216 217	syl	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] = \emptyset$
219	218	fveq2d	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]) = vol (\emptyset)$
220		0mbl	$⊢ \emptyset \in dom vol$
221		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
222	220 221	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
223		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
224	222 223	eqtri	$⊢ vol (\emptyset) = 0$
225	219 224	eqtrdi	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]) = 0$
226	203 225	eqtrd	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to y I z = 0$
227	226	oveq2d	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to (y + z) (y I z) = (y + z) \cdot 0$
228	199 200	readdcld	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to y + z \in ℝ$
229	228	recnd	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to y + z \in ℂ$
230	229	mul01d	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to (y + z) \cdot 0 = 0$
231	227 230	eqtrd	$⊢ ((φ \land z \in ran G) \land (y \in (ℝ ∖ ran F) \land \neg (y = 0 \land z = 0))) \to (y + z) (y I z) = 0$
232	231	expr	$⊢ ((φ \land z \in ran G) \land y \in (ℝ ∖ ran F)) \to (\neg (y = 0 \land z = 0) \to (y + z) (y I z) = 0)$
233		oveq12	$⊢ (y = 0 \land z = 0) \to y + z = 0 + 0$
234	233 98	eqtrdi	$⊢ (y = 0 \land z = 0) \to y + z = 0$
235		oveq12	$⊢ (y = 0 \land z = 0) \to y I z = 0 I 0$
236		0re	$⊢ 0 \in ℝ$
237		iftrue	$⊢ (i = 0 \land j = 0) \to if ((i = 0 \land j = 0), 0, vol (F^{-1} [\{i\}] \cap G^{-1} [\{j\}])) = 0$
238		c0ex	$⊢ 0 \in V$
239	237 3 238	ovmpoa	$⊢ (0 \in ℝ \land 0 \in ℝ) \to 0 I 0 = 0$
240	236 236 239	mp2an	$⊢ 0 I 0 = 0$
241	235 240	eqtrdi	$⊢ (y = 0 \land z = 0) \to y I z = 0$
242	234 241	oveq12d	$⊢ (y = 0 \land z = 0) \to (y + z) (y I z) = 0 \cdot 0$
243		0cn	$⊢ 0 \in ℂ$
244	243	mul01i	$⊢ 0 \cdot 0 = 0$
245	242 244	eqtrdi	$⊢ (y = 0 \land z = 0) \to (y + z) (y I z) = 0$
246	232 245	pm2.61d2	$⊢ ((φ \land z \in ran G) \land y \in (ℝ ∖ ran F)) \to (y + z) (y I z) = 0$
247	197 246	syldan	$⊢ ((φ \land z \in ran G) \land y \in (ran (v \in ran P ⟼ v - z) ∖ ran F)) \to (y + z) (y I z) = 0$
248		f1ofo	$⊢ (v \in ran P ⟼ v - z) : ran P \underset{1-1 onto}{⟶} ran (v \in ran P ⟼ v - z) \to (v \in ran P ⟼ v - z) : ran P \underset{onto}{⟶} ran (v \in ran P ⟼ v - z)$
249	144 248	syl	$⊢ (φ \land z \in ran G) \to (v \in ran P ⟼ v - z) : ran P \underset{onto}{⟶} ran (v \in ran P ⟼ v - z)$
250		fofi	$⊢ (ran P \in Fin \land (v \in ran P ⟼ v - z) : ran P \underset{onto}{⟶} ran (v \in ran P ⟼ v - z)) \to ran (v \in ran P ⟼ v - z) \in Fin$
251	127 249 250	syl2anc	$⊢ (φ \land z \in ran G) \to ran (v \in ran P ⟼ v - z) \in Fin$
252	189 195 247 251	fsumss	$⊢ (φ \land z \in ran G) \to \sum_{y \in ran F} (y + z) (y I z) = \sum_{y \in ran (v \in ran P ⟼ v - z)} (y + z) (y I z)$
253	34	a1i	$⊢ (φ \land z \in ran G) \to ran P ∖ \{0\} \subseteq ran P$
254	120	an32s	$⊢ ((φ \land z \in ran G) \land w \in (ran P ∖ \{0\})) \to w ((w - z) I z) \in ℂ$
255		dfin4	$⊢ ran P \cap \{0\} = ran P ∖ (ran P ∖ \{0\})$
256		inss2	$⊢ ran P \cap \{0\} \subseteq \{0\}$
257	255 256	eqsstrri	$⊢ ran P ∖ (ran P ∖ \{0\}) \subseteq \{0\}$
258	257	sseli	$⊢ w \in (ran P ∖ (ran P ∖ \{0\})) \to w \in \{0\}$
259		elsni	$⊢ w \in \{0\} \to w = 0$
260	259	adantl	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to w = 0$
261	260	oveq1d	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to w ((w - z) I z) = 0 \cdot ((w - z) I z)$
262	104	ad2antrr	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to I : ℝ^{2} ⟶ ℝ$
263	260 236	eqeltrdi	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to w \in ℝ$
264	63	adantr	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to z \in ℝ$
265	263 264	resubcld	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to w - z \in ℝ$
266	262 265 264	fovrnd	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to (w - z) I z \in ℝ$
267	266	recnd	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to (w - z) I z \in ℂ$
268	267	mul02d	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to 0 \cdot ((w - z) I z) = 0$
269	261 268	eqtrd	$⊢ ((φ \land z \in ran G) \land w \in \{0\}) \to w ((w - z) I z) = 0$
270	258 269	sylan2	$⊢ ((φ \land z \in ran G) \land w \in (ran P ∖ (ran P ∖ \{0\}))) \to w ((w - z) I z) = 0$
271	253 254 270 127	fsumss	$⊢ (φ \land z \in ran G) \to \sum_{w \in ran P ∖ \{0\}} w ((w - z) I z) = \sum_{w \in ran P} w ((w - z) I z)$
272	167 252 271	3eqtr4d	$⊢ (φ \land z \in ran G) \to \sum_{y \in ran F} (y + z) (y I z) = \sum_{w \in ran P ∖ \{0\}} w ((w - z) I z)$
273	272	sumeq2dv	$⊢ φ \to \sum_{z \in ran G} \sum_{y \in ran F} (y + z) (y I z) = \sum_{z \in ran G} \sum_{w \in ran P ∖ \{0\}} w ((w - z) I z)$
274	195	anasss	$⊢ (φ \land (z \in ran G \land y \in ran F)) \to (y + z) (y I z) \in ℂ$
275	9 7 274	fsumcom	$⊢ φ \to \sum_{z \in ran G} \sum_{y \in ran F} (y + z) (y I z) = \sum_{y \in ran F} \sum_{z \in ran G} (y + z) (y I z)$
276	123 273 275	3eqtr2d	$⊢ φ \to \int^{1} (F +_{f} G) = \sum_{y \in ran F} \sum_{z \in ran G} (y + z) (y I z)$

Metamath Proof Explorer

Theorem itg1addlem4

Proof