itg1addlem5

Description: Lemma for itg1add . (Contributed by Mario Carneiro, 27-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	itg1addlem5	$⊢ φ \to \int^{1} (F +_{f} G) = \int^{1} (F) + \int^{1} (G)$

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		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
6	1 5	syl	$⊢ φ \to ran F \in Fin$
7		i1frn	$⊢ G \in dom \int^{1} \to ran G \in Fin$
8	2 7	syl	$⊢ φ \to ran G \in Fin$
9	8	adantr	$⊢ (φ \land y \in ran F) \to ran G \in Fin$
10		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
11	1 10	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
12	11	frnd	$⊢ φ \to ran F \subseteq ℝ$
13	12	sselda	$⊢ (φ \land y \in ran F) \to y \in ℝ$
14	13	adantr	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to y \in ℝ$
15	14	recnd	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to y \in ℂ$
16	1 2 3	itg1addlem2	$⊢ φ \to I : ℝ^{2} ⟶ ℝ$
17	16	ad2antrr	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to I : ℝ^{2} ⟶ ℝ$
18		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
19	2 18	syl	$⊢ φ \to G : ℝ ⟶ ℝ$
20	19	frnd	$⊢ φ \to ran G \subseteq ℝ$
21	20	sselda	$⊢ (φ \land z \in ran G) \to z \in ℝ$
22	21	adantlr	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to z \in ℝ$
23	17 14 22	fovrnd	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to y I z \in ℝ$
24	23	recnd	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to y I z \in ℂ$
25	15 24	mulcld	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to y (y I z) \in ℂ$
26	9 25	fsumcl	$⊢ (φ \land y \in ran F) \to \sum_{z \in ran G} y (y I z) \in ℂ$
27	22	recnd	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to z \in ℂ$
28	27 24	mulcld	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to z (y I z) \in ℂ$
29	9 28	fsumcl	$⊢ (φ \land y \in ran F) \to \sum_{z \in ran G} z (y I z) \in ℂ$
30	6 26 29	fsumadd	$⊢ φ \to \sum_{y \in ran F} (\sum_{z \in ran G} y (y I z) + \sum_{z \in ran G} z (y I z)) = \sum_{y \in ran F} \sum_{z \in ran G} y (y I z) + \sum_{y \in ran F} \sum_{z \in ran G} z (y I z)$
31	1 2 3 4	itg1addlem4	$⊢ φ \to \int^{1} (F +_{f} G) = \sum_{y \in ran F} \sum_{z \in ran G} (y + z) (y I z)$
32	15 27 24	adddird	$⊢ ((φ \land y \in ran F) \land z \in ran G) \to (y + z) (y I z) = y (y I z) + z (y I z)$
33	32	sumeq2dv	$⊢ (φ \land y \in ran F) \to \sum_{z \in ran G} (y + z) (y I z) = \sum_{z \in ran G} (y (y I z) + z (y I z))$
34	9 25 28	fsumadd	$⊢ (φ \land y \in ran F) \to \sum_{z \in ran G} (y (y I z) + z (y I z)) = \sum_{z \in ran G} y (y I z) + \sum_{z \in ran G} z (y I z)$
35	33 34	eqtrd	$⊢ (φ \land y \in ran F) \to \sum_{z \in ran G} (y + z) (y I z) = \sum_{z \in ran G} y (y I z) + \sum_{z \in ran G} z (y I z)$
36	35	sumeq2dv	$⊢ φ \to \sum_{y \in ran F} \sum_{z \in ran G} (y + z) (y I z) = \sum_{y \in ran F} (\sum_{z \in ran G} y (y I z) + \sum_{z \in ran G} z (y I z))$
37	31 36	eqtrd	$⊢ φ \to \int^{1} (F +_{f} G) = \sum_{y \in ran F} (\sum_{z \in ran G} y (y I z) + \sum_{z \in ran G} z (y I z))$
38		itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{y \in ran F ∖ \{0\}} y vol (F^{-1} [\{y\}])$
39	1 38	syl	$⊢ φ \to \int^{1} (F) = \sum_{y \in ran F ∖ \{0\}} y vol (F^{-1} [\{y\}])$
40	19	adantr	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to G : ℝ ⟶ ℝ$
41	8	adantr	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to ran G \in Fin$
42		inss2	$⊢ F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \subseteq G^{-1} [\{z\}]$
43	42	a1i	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \subseteq G^{-1} [\{z\}]$
44		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{y\}] \in dom vol$
45	1 44	syl	$⊢ φ \to F^{-1} [\{y\}] \in dom vol$
46	45	ad2antrr	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to F^{-1} [\{y\}] \in dom vol$
47		i1fima	$⊢ G \in dom \int^{1} \to G^{-1} [\{z\}] \in dom vol$
48	2 47	syl	$⊢ φ \to G^{-1} [\{z\}] \in dom vol$
49	48	ad2antrr	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to G^{-1} [\{z\}] \in dom vol$
50		inmbl	$⊢ (F^{-1} [\{y\}] \in dom vol \land G^{-1} [\{z\}] \in dom vol) \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \in dom vol$
51	46 49 50	syl2anc	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \in dom vol$
52	12	ssdifssd	$⊢ φ \to ran F ∖ \{0\} \subseteq ℝ$
53	52	sselda	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to y \in ℝ$
54	53	adantr	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to y \in ℝ$
55	20	adantr	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to ran G \subseteq ℝ$
56	55	sselda	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to z \in ℝ$
57		eldifsni	$⊢ y \in (ran F ∖ \{0\}) \to y \neq 0$
58	57	ad2antlr	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to y \neq 0$
59		simpl	$⊢ (y = 0 \land z = 0) \to y = 0$
60	59	necon3ai	$⊢ y \neq 0 \to \neg (y = 0 \land z = 0)$
61	58 60	syl	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to \neg (y = 0 \land z = 0)$
62	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\}])$
63	54 56 61 62	syl21anc	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to y I z = vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
64	16	ad2antrr	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to I : ℝ^{2} ⟶ ℝ$
65	64 54 56	fovrnd	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to y I z \in ℝ$
66	63 65	eqeltrrd	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]) \in ℝ$
67	40 41 43 51 66	itg1addlem1	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to vol (⋃_{z \in ran G} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])) = \sum_{z \in ran G} vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
68		iunin2	$⊢ ⋃_{z \in ran G} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]) = F^{-1} [\{y\}] \cap ⋃_{z \in ran G} G^{-1} [\{z\}]$
69	1	adantr	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to F \in dom \int^{1}$
70	69 44	syl	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to F^{-1} [\{y\}] \in dom vol$
71		mblss	$⊢ F^{-1} [\{y\}] \in dom vol \to F^{-1} [\{y\}] \subseteq ℝ$
72	70 71	syl	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to F^{-1} [\{y\}] \subseteq ℝ$
73		iunid	$⊢ ⋃_{z \in ran G} \{z\} = ran G$
74	73	imaeq2i	$⊢ G^{-1} [⋃_{z \in ran G} \{z\}] = G^{-1} [ran G]$
75		imaiun	$⊢ G^{-1} [⋃_{z \in ran G} \{z\}] = ⋃_{z \in ran G} G^{-1} [\{z\}]$
76		cnvimarndm	$⊢ G^{-1} [ran G] = dom G$
77	74 75 76	3eqtr3i	$⊢ ⋃_{z \in ran G} G^{-1} [\{z\}] = dom G$
78	40	fdmd	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to dom G = ℝ$
79	77 78	syl5eq	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to ⋃_{z \in ran G} G^{-1} [\{z\}] = ℝ$
80	72 79	sseqtrrd	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to F^{-1} [\{y\}] \subseteq ⋃_{z \in ran G} G^{-1} [\{z\}]$
81		df-ss	$⊢ F^{-1} [\{y\}] \subseteq ⋃_{z \in ran G} G^{-1} [\{z\}] \leftrightarrow F^{-1} [\{y\}] \cap ⋃_{z \in ran G} G^{-1} [\{z\}] = F^{-1} [\{y\}]$
82	80 81	sylib	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to F^{-1} [\{y\}] \cap ⋃_{z \in ran G} G^{-1} [\{z\}] = F^{-1} [\{y\}]$
83	68 82	syl5req	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to F^{-1} [\{y\}] = ⋃_{z \in ran G} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
84	83	fveq2d	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{y\}]) = vol (⋃_{z \in ran G} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]))$
85	63	sumeq2dv	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to \sum_{z \in ran G} (y I z) = \sum_{z \in ran G} vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
86	67 84 85	3eqtr4d	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{y\}]) = \sum_{z \in ran G} (y I z)$
87	86	oveq2d	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to y vol (F^{-1} [\{y\}]) = y \sum_{z \in ran G} (y I z)$
88	53	recnd	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to y \in ℂ$
89	65	recnd	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to y I z \in ℂ$
90	41 88 89	fsummulc2	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to y \sum_{z \in ran G} (y I z) = \sum_{z \in ran G} y (y I z)$
91	87 90	eqtrd	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to y vol (F^{-1} [\{y\}]) = \sum_{z \in ran G} y (y I z)$
92	91	sumeq2dv	$⊢ φ \to \sum_{y \in ran F ∖ \{0\}} y vol (F^{-1} [\{y\}]) = \sum_{y \in ran F ∖ \{0\}} \sum_{z \in ran G} y (y I z)$
93		difssd	$⊢ φ \to ran F ∖ \{0\} \subseteq ran F$
94	54	recnd	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to y \in ℂ$
95	94 89	mulcld	$⊢ ((φ \land y \in (ran F ∖ \{0\})) \land z \in ran G) \to y (y I z) \in ℂ$
96	41 95	fsumcl	$⊢ (φ \land y \in (ran F ∖ \{0\})) \to \sum_{z \in ran G} y (y I z) \in ℂ$
97		dfin4	$⊢ ran F \cap \{0\} = ran F ∖ (ran F ∖ \{0\})$
98		inss2	$⊢ ran F \cap \{0\} \subseteq \{0\}$
99	97 98	eqsstrri	$⊢ ran F ∖ (ran F ∖ \{0\}) \subseteq \{0\}$
100	99	sseli	$⊢ y \in (ran F ∖ (ran F ∖ \{0\})) \to y \in \{0\}$
101		elsni	$⊢ y \in \{0\} \to y = 0$
102	101	ad2antlr	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to y = 0$
103	102	oveq1d	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to y (y I z) = 0 \cdot (y I z)$
104	16	ad2antrr	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to I : ℝ^{2} ⟶ ℝ$
105		0re	$⊢ 0 \in ℝ$
106	102 105	eqeltrdi	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to y \in ℝ$
107	21	adantlr	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to z \in ℝ$
108	104 106 107	fovrnd	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to y I z \in ℝ$
109	108	recnd	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to y I z \in ℂ$
110	109	mul02d	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to 0 \cdot (y I z) = 0$
111	103 110	eqtrd	$⊢ ((φ \land y \in \{0\}) \land z \in ran G) \to y (y I z) = 0$
112	111	sumeq2dv	$⊢ (φ \land y \in \{0\}) \to \sum_{z \in ran G} y (y I z) = \sum_{z \in ran G} 0$
113	8	adantr	$⊢ (φ \land y \in \{0\}) \to ran G \in Fin$
114	113	olcd	$⊢ (φ \land y \in \{0\}) \to (ran G \subseteq ℤ_{\geq 0} \lor ran G \in Fin)$
115		sumz	$⊢ (ran G \subseteq ℤ_{\geq 0} \lor ran G \in Fin) \to \sum_{z \in ran G} 0 = 0$
116	114 115	syl	$⊢ (φ \land y \in \{0\}) \to \sum_{z \in ran G} 0 = 0$
117	112 116	eqtrd	$⊢ (φ \land y \in \{0\}) \to \sum_{z \in ran G} y (y I z) = 0$
118	100 117	sylan2	$⊢ (φ \land y \in (ran F ∖ (ran F ∖ \{0\}))) \to \sum_{z \in ran G} y (y I z) = 0$
119	93 96 118 6	fsumss	$⊢ φ \to \sum_{y \in ran F ∖ \{0\}} \sum_{z \in ran G} y (y I z) = \sum_{y \in ran F} \sum_{z \in ran G} y (y I z)$
120	39 92 119	3eqtrd	$⊢ φ \to \int^{1} (F) = \sum_{y \in ran F} \sum_{z \in ran G} y (y I z)$
121		itg1val	$⊢ G \in dom \int^{1} \to \int^{1} (G) = \sum_{z \in ran G ∖ \{0\}} z vol (G^{-1} [\{z\}])$
122	2 121	syl	$⊢ φ \to \int^{1} (G) = \sum_{z \in ran G ∖ \{0\}} z vol (G^{-1} [\{z\}])$
123	11	adantr	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to F : ℝ ⟶ ℝ$
124	6	adantr	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to ran F \in Fin$
125		inss1	$⊢ F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \subseteq F^{-1} [\{y\}]$
126	125	a1i	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \subseteq F^{-1} [\{y\}]$
127	45	ad2antrr	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to F^{-1} [\{y\}] \in dom vol$
128	48	ad2antrr	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to G^{-1} [\{z\}] \in dom vol$
129	127 128 50	syl2anc	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] \in dom vol$
130	12	adantr	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to ran F \subseteq ℝ$
131	130	sselda	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to y \in ℝ$
132	20	ssdifssd	$⊢ φ \to ran G ∖ \{0\} \subseteq ℝ$
133	132	sselda	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to z \in ℝ$
134	133	adantr	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to z \in ℝ$
135		eldifsni	$⊢ z \in (ran G ∖ \{0\}) \to z \neq 0$
136	135	ad2antlr	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to z \neq 0$
137		simpr	$⊢ (y = 0 \land z = 0) \to z = 0$
138	137	necon3ai	$⊢ z \neq 0 \to \neg (y = 0 \land z = 0)$
139	136 138	syl	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to \neg (y = 0 \land z = 0)$
140	131 134 139 62	syl21anc	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to y I z = vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
141	16	ad2antrr	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to I : ℝ^{2} ⟶ ℝ$
142	141 131 134	fovrnd	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to y I z \in ℝ$
143	140 142	eqeltrrd	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]) \in ℝ$
144	123 124 126 129 143	itg1addlem1	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to vol (⋃_{y \in ran F} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])) = \sum_{y \in ran F} vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
145		incom	$⊢ F^{-1} [\{y\}] \cap G^{-1} [\{z\}] = G^{-1} [\{z\}] \cap F^{-1} [\{y\}]$
146	145	a1i	$⊢ y \in ran F \to F^{-1} [\{y\}] \cap G^{-1} [\{z\}] = G^{-1} [\{z\}] \cap F^{-1} [\{y\}]$
147	146	iuneq2i	$⊢ ⋃_{y \in ran F} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]) = ⋃_{y \in ran F} (G^{-1} [\{z\}] \cap F^{-1} [\{y\}])$
148		iunin2	$⊢ ⋃_{y \in ran F} (G^{-1} [\{z\}] \cap F^{-1} [\{y\}]) = G^{-1} [\{z\}] \cap ⋃_{y \in ran F} F^{-1} [\{y\}]$
149	147 148	eqtri	$⊢ ⋃_{y \in ran F} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]) = G^{-1} [\{z\}] \cap ⋃_{y \in ran F} F^{-1} [\{y\}]$
150		cnvimass	$⊢ G^{-1} [\{z\}] \subseteq dom G$
151	19	fdmd	$⊢ φ \to dom G = ℝ$
152	151	adantr	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to dom G = ℝ$
153	150 152	sseqtrid	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to G^{-1} [\{z\}] \subseteq ℝ$
154		iunid	$⊢ ⋃_{y \in ran F} \{y\} = ran F$
155	154	imaeq2i	$⊢ F^{-1} [⋃_{y \in ran F} \{y\}] = F^{-1} [ran F]$
156		imaiun	$⊢ F^{-1} [⋃_{y \in ran F} \{y\}] = ⋃_{y \in ran F} F^{-1} [\{y\}]$
157		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
158	155 156 157	3eqtr3i	$⊢ ⋃_{y \in ran F} F^{-1} [\{y\}] = dom F$
159	11	fdmd	$⊢ φ \to dom F = ℝ$
160	159	adantr	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to dom F = ℝ$
161	158 160	syl5eq	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to ⋃_{y \in ran F} F^{-1} [\{y\}] = ℝ$
162	153 161	sseqtrrd	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to G^{-1} [\{z\}] \subseteq ⋃_{y \in ran F} F^{-1} [\{y\}]$
163		df-ss	$⊢ G^{-1} [\{z\}] \subseteq ⋃_{y \in ran F} F^{-1} [\{y\}] \leftrightarrow G^{-1} [\{z\}] \cap ⋃_{y \in ran F} F^{-1} [\{y\}] = G^{-1} [\{z\}]$
164	162 163	sylib	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to G^{-1} [\{z\}] \cap ⋃_{y \in ran F} F^{-1} [\{y\}] = G^{-1} [\{z\}]$
165	149 164	syl5req	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to G^{-1} [\{z\}] = ⋃_{y \in ran F} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
166	165	fveq2d	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{z\}]) = vol (⋃_{y \in ran F} (F^{-1} [\{y\}] \cap G^{-1} [\{z\}]))$
167	140	sumeq2dv	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to \sum_{y \in ran F} (y I z) = \sum_{y \in ran F} vol (F^{-1} [\{y\}] \cap G^{-1} [\{z\}])$
168	144 166 167	3eqtr4d	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to vol (G^{-1} [\{z\}]) = \sum_{y \in ran F} (y I z)$
169	168	oveq2d	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to z vol (G^{-1} [\{z\}]) = z \sum_{y \in ran F} (y I z)$
170	133	recnd	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to z \in ℂ$
171	142	recnd	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to y I z \in ℂ$
172	124 170 171	fsummulc2	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to z \sum_{y \in ran F} (y I z) = \sum_{y \in ran F} z (y I z)$
173	169 172	eqtrd	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to z vol (G^{-1} [\{z\}]) = \sum_{y \in ran F} z (y I z)$
174	173	sumeq2dv	$⊢ φ \to \sum_{z \in ran G ∖ \{0\}} z vol (G^{-1} [\{z\}]) = \sum_{z \in ran G ∖ \{0\}} \sum_{y \in ran F} z (y I z)$
175		difssd	$⊢ φ \to ran G ∖ \{0\} \subseteq ran G$
176	170	adantr	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to z \in ℂ$
177	176 171	mulcld	$⊢ ((φ \land z \in (ran G ∖ \{0\})) \land y \in ran F) \to z (y I z) \in ℂ$
178	124 177	fsumcl	$⊢ (φ \land z \in (ran G ∖ \{0\})) \to \sum_{y \in ran F} z (y I z) \in ℂ$
179		dfin4	$⊢ ran G \cap \{0\} = ran G ∖ (ran G ∖ \{0\})$
180		inss2	$⊢ ran G \cap \{0\} \subseteq \{0\}$
181	179 180	eqsstrri	$⊢ ran G ∖ (ran G ∖ \{0\}) \subseteq \{0\}$
182	181	sseli	$⊢ z \in (ran G ∖ (ran G ∖ \{0\})) \to z \in \{0\}$
183		elsni	$⊢ z \in \{0\} \to z = 0$
184	183	ad2antlr	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to z = 0$
185	184	oveq1d	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to z (y I z) = 0 \cdot (y I z)$
186	16	ad2antrr	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to I : ℝ^{2} ⟶ ℝ$
187	13	adantlr	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to y \in ℝ$
188	184 105	eqeltrdi	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to z \in ℝ$
189	186 187 188	fovrnd	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to y I z \in ℝ$
190	189	recnd	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to y I z \in ℂ$
191	190	mul02d	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to 0 \cdot (y I z) = 0$
192	185 191	eqtrd	$⊢ ((φ \land z \in \{0\}) \land y \in ran F) \to z (y I z) = 0$
193	192	sumeq2dv	$⊢ (φ \land z \in \{0\}) \to \sum_{y \in ran F} z (y I z) = \sum_{y \in ran F} 0$
194	6	adantr	$⊢ (φ \land z \in \{0\}) \to ran F \in Fin$
195	194	olcd	$⊢ (φ \land z \in \{0\}) \to (ran F \subseteq ℤ_{\geq 0} \lor ran F \in Fin)$
196		sumz	$⊢ (ran F \subseteq ℤ_{\geq 0} \lor ran F \in Fin) \to \sum_{y \in ran F} 0 = 0$
197	195 196	syl	$⊢ (φ \land z \in \{0\}) \to \sum_{y \in ran F} 0 = 0$
198	193 197	eqtrd	$⊢ (φ \land z \in \{0\}) \to \sum_{y \in ran F} z (y I z) = 0$
199	182 198	sylan2	$⊢ (φ \land z \in (ran G ∖ (ran G ∖ \{0\}))) \to \sum_{y \in ran F} z (y I z) = 0$
200	175 178 199 8	fsumss	$⊢ φ \to \sum_{z \in ran G ∖ \{0\}} \sum_{y \in ran F} z (y I z) = \sum_{z \in ran G} \sum_{y \in ran F} z (y I z)$
201	21	adantr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to z \in ℝ$
202	201	recnd	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to z \in ℂ$
203	16	ad2antrr	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to I : ℝ^{2} ⟶ ℝ$
204	12	adantr	$⊢ (φ \land z \in ran G) \to ran F \subseteq ℝ$
205	204	sselda	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y \in ℝ$
206	203 205 201	fovrnd	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y I z \in ℝ$
207	206	recnd	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to y I z \in ℂ$
208	202 207	mulcld	$⊢ ((φ \land z \in ran G) \land y \in ran F) \to z (y I z) \in ℂ$
209	208	anasss	$⊢ (φ \land (z \in ran G \land y \in ran F)) \to z (y I z) \in ℂ$
210	8 6 209	fsumcom	$⊢ φ \to \sum_{z \in ran G} \sum_{y \in ran F} z (y I z) = \sum_{y \in ran F} \sum_{z \in ran G} z (y I z)$
211	200 210	eqtrd	$⊢ φ \to \sum_{z \in ran G ∖ \{0\}} \sum_{y \in ran F} z (y I z) = \sum_{y \in ran F} \sum_{z \in ran G} z (y I z)$
212	122 174 211	3eqtrd	$⊢ φ \to \int^{1} (G) = \sum_{y \in ran F} \sum_{z \in ran G} z (y I z)$
213	120 212	oveq12d	$⊢ φ \to \int^{1} (F) + \int^{1} (G) = \sum_{y \in ran F} \sum_{z \in ran G} y (y I z) + \sum_{y \in ran F} \sum_{z \in ran G} z (y I z)$
214	30 37 213	3eqtr4d	$⊢ φ \to \int^{1} (F +_{f} G) = \int^{1} (F) + \int^{1} (G)$

Metamath Proof Explorer

Theorem itg1addlem5

Proof