itg1addlem4

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 28-Jun-2014) (Proof shortened by SN, 3-Oct-2024)

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