uniioombllem5

	Ref	Expression
Hypotheses	uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
	uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	uniioombl.a	$⊢ A = ⋃ ran ((.) \circ F)$
	uniioombl.e	$⊢ φ \to {vol}^{*} (E) \in ℝ$
	uniioombl.c	$⊢ φ \to C \in ℝ^{+}$
	uniioombl.g	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.s	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ G)$
	uniioombl.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
	uniioombl.v	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (E) + C$
	uniioombl.m	$⊢ φ \to M \in ℕ$
	uniioombl.m2	$⊢ φ \to \|T (M) - sup (ran T ℝ^{*} <)\| < C$
	uniioombl.k	$⊢ K = ⋃ ((.) \circ G) [(1 \dots M)]$
	uniioombl.n	$⊢ φ \to N \in ℕ$
	uniioombl.n2	$⊢ φ \to \forall j \in (1 \dots M) \|\sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{M}$
	uniioombl.l	$⊢ L = ⋃ ((.) \circ F) [(1 \dots N)]$
Assertion	uniioombllem5	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \leq {vol}^{*} (E) + 4 C$

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
2		uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
3		uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
4		uniioombl.a	$⊢ A = ⋃ ran ((.) \circ F)$
5		uniioombl.e	$⊢ φ \to {vol}^{*} (E) \in ℝ$
6		uniioombl.c	$⊢ φ \to C \in ℝ^{+}$
7		uniioombl.g	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
8		uniioombl.s	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ G)$
9		uniioombl.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
10		uniioombl.v	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (E) + C$
11		uniioombl.m	$⊢ φ \to M \in ℕ$
12		uniioombl.m2	$⊢ φ \to \|T (M) - sup (ran T ℝ^{*} <)\| < C$
13		uniioombl.k	$⊢ K = ⋃ ((.) \circ G) [(1 \dots M)]$
14		uniioombl.n	$⊢ φ \to N \in ℕ$
15		uniioombl.n2	$⊢ φ \to \forall j \in (1 \dots M) \|\sum_{i = 1}^{N} {vol}^{} ((.) (F (i)) \cap (.) (G (j))) - {vol}^{} ((.) (G (j)) \cap A)\| < \frac{C}{M}$
16		uniioombl.l	$⊢ L = ⋃ ((.) \circ F) [(1 \dots N)]$
17		inss1	$⊢ E \cap A \subseteq E$
18	7	uniiccdif	$⊢ φ \to (⋃ ran ((.) \circ G) \subseteq ⋃ ran ([.] \circ G) \land {vol}^{*} (⋃ ran ([.] \circ G) ∖ ⋃ ran ((.) \circ G)) = 0)$
19	18	simpld	$⊢ φ \to ⋃ ran ((.) \circ G) \subseteq ⋃ ran ([.] \circ G)$
20		ovolficcss	$⊢ G : ℕ ⟶ \leq \cap ℝ^{2} \to ⋃ ran ([.] \circ G) \subseteq ℝ$
21	7 20	syl	$⊢ φ \to ⋃ ran ([.] \circ G) \subseteq ℝ$
22	19 21	sstrd	$⊢ φ \to ⋃ ran ((.) \circ G) \subseteq ℝ$
23	8 22	sstrd	$⊢ φ \to E \subseteq ℝ$
24		ovolsscl	$⊢ (E \cap A \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E \cap A) \in ℝ$
25	17 23 5 24	mp3an2i	$⊢ φ \to {vol}^{*} (E \cap A) \in ℝ$
26		difssd	$⊢ φ \to E ∖ A \subseteq E$
27		ovolsscl	$⊢ (E ∖ A \subseteq E \land E \subseteq ℝ \land {vol}^{} (E) \in ℝ) \to {vol}^{} (E ∖ A) \in ℝ$
28	26 23 5 27	syl3anc	$⊢ φ \to {vol}^{*} (E ∖ A) \in ℝ$
29	25 28	readdcld	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \in ℝ$
30		inss1	$⊢ K \cap A \subseteq K$
31		imassrn	$⊢ ((.) \circ G) [(1 \dots M)] \subseteq ran ((.) \circ G)$
32	31	unissi	$⊢ ⋃ ((.) \circ G) [(1 \dots M)] \subseteq ⋃ ran ((.) \circ G)$
33	13 32	eqsstri	$⊢ K \subseteq ⋃ ran ((.) \circ G)$
34	33 22	sstrid	$⊢ φ \to K \subseteq ℝ$
35	1 2 3 4 5 6 7 8 9 10	uniioombllem1	$⊢ φ \to sup (ran T ℝ^{*} <) \in ℝ$
36		ssid	$⊢ ⋃ ran ((.) \circ G) \subseteq ⋃ ran ((.) \circ G)$
37	9	ovollb	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land ⋃ ran ((.) \circ G) \subseteq ⋃ ran ((.) \circ G)) \to {vol}^{} (⋃ ran ((.) \circ G)) \leq sup (ran T ℝ^{} <)$
38	7 36 37	sylancl	$⊢ φ \to {vol}^{} (⋃ ran ((.) \circ G)) \leq sup (ran T ℝ^{} <)$
39		ovollecl	$⊢ (⋃ ran ((.) \circ G) \subseteq ℝ \land sup (ran T ℝ^{} <) \in ℝ \land {vol}^{} (⋃ ran ((.) \circ G)) \leq sup (ran T ℝ^{} <)) \to {vol}^{} (⋃ ran ((.) \circ G)) \in ℝ$
40	22 35 38 39	syl3anc	$⊢ φ \to {vol}^{*} (⋃ ran ((.) \circ G)) \in ℝ$
41		ovolsscl	$⊢ (K \subseteq ⋃ ran ((.) \circ G) \land ⋃ ran ((.) \circ G) \subseteq ℝ \land {vol}^{} (⋃ ran ((.) \circ G)) \in ℝ) \to {vol}^{} (K) \in ℝ$
42	33 22 40 41	mp3an2i	$⊢ φ \to {vol}^{*} (K) \in ℝ$
43		ovolsscl	$⊢ (K \cap A \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K \cap A) \in ℝ$
44	30 34 42 43	mp3an2i	$⊢ φ \to {vol}^{*} (K \cap A) \in ℝ$
45		difssd	$⊢ φ \to K ∖ A \subseteq K$
46		ovolsscl	$⊢ (K ∖ A \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K ∖ A) \in ℝ$
47	45 34 42 46	syl3anc	$⊢ φ \to {vol}^{*} (K ∖ A) \in ℝ$
48	44 47	readdcld	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) \in ℝ$
49	6	rpred	$⊢ φ \to C \in ℝ$
50	49 49	readdcld	$⊢ φ \to C + C \in ℝ$
51	48 50	readdcld	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) + C + C \in ℝ$
52		4re	$⊢ 4 \in ℝ$
53		remulcl	$⊢ (4 \in ℝ \land C \in ℝ) \to 4 C \in ℝ$
54	52 49 53	sylancr	$⊢ φ \to 4 C \in ℝ$
55	5 54	readdcld	$⊢ φ \to {vol}^{*} (E) + 4 C \in ℝ$
56	1 2 3 4 5 6 7 8 9 10 11 12 13	uniioombllem3	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) < {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) + C + C$
57	29 51 56	ltled	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \leq {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) + C + C$
58	5 50	readdcld	$⊢ φ \to {vol}^{*} (E) + C + C \in ℝ$
59	42 49	readdcld	$⊢ φ \to {vol}^{*} (K) + C \in ℝ$
60		inss1	$⊢ K \cap L \subseteq K$
61		ovolsscl	$⊢ (K \cap L \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K \cap L) \in ℝ$
62	60 34 42 61	mp3an2i	$⊢ φ \to {vol}^{*} (K \cap L) \in ℝ$
63	62 49	readdcld	$⊢ φ \to {vol}^{*} (K \cap L) + C \in ℝ$
64		difssd	$⊢ φ \to K ∖ L \subseteq K$
65		ovolsscl	$⊢ (K ∖ L \subseteq K \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K ∖ L) \in ℝ$
66	64 34 42 65	syl3anc	$⊢ φ \to {vol}^{*} (K ∖ L) \in ℝ$
67	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	uniioombllem4	$⊢ φ \to {vol}^{} (K \cap A) \leq {vol}^{} (K \cap L) + C$
68		imassrn	$⊢ ((.) \circ F) [(1 \dots N)] \subseteq ran ((.) \circ F)$
69	68	unissi	$⊢ ⋃ ((.) \circ F) [(1 \dots N)] \subseteq ⋃ ran ((.) \circ F)$
70	69 16 4	3sstr4i	$⊢ L \subseteq A$
71		sscon	$⊢ L \subseteq A \to K ∖ A \subseteq K ∖ L$
72	70 71	mp1i	$⊢ φ \to K ∖ A \subseteq K ∖ L$
73	64 34	sstrd	$⊢ φ \to K ∖ L \subseteq ℝ$
74		ovolss	$⊢ (K ∖ A \subseteq K ∖ L \land K ∖ L \subseteq ℝ) \to {vol}^{} (K ∖ A) \leq {vol}^{} (K ∖ L)$
75	72 73 74	syl2anc	$⊢ φ \to {vol}^{} (K ∖ A) \leq {vol}^{} (K ∖ L)$
76	44 47 63 66 67 75	le2addd	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) \leq {vol}^{} (K \cap L) + C + {vol}^{} (K ∖ L)$
77	62	recnd	$⊢ φ \to {vol}^{*} (K \cap L) \in ℂ$
78	49	recnd	$⊢ φ \to C \in ℂ$
79	66	recnd	$⊢ φ \to {vol}^{*} (K ∖ L) \in ℂ$
80	77 78 79	add32d	$⊢ φ \to {vol}^{} (K \cap L) + C + {vol}^{} (K ∖ L) = {vol}^{} (K \cap L) + {vol}^{} (K ∖ L) + C$
81		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
82		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
83		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
84	82 83	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
85		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
86	1 84 85	sylancl	$⊢ φ \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
87		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
88	81 86 87	sylancr	$⊢ φ \to ((.) \circ F) : ℕ ⟶ 𝒫 ℝ$
89		ffun	$⊢ ((.) \circ F) : ℕ ⟶ 𝒫 ℝ \to Fun ((.) \circ F)$
90		funiunfv	$⊢ Fun ((.) \circ F) \to ⋃_{n = 1}^{N} ((.) \circ F) (n) = ⋃ ((.) \circ F) [(1 \dots N)]$
91	88 89 90	3syl	$⊢ φ \to ⋃_{n = 1}^{N} ((.) \circ F) (n) = ⋃ ((.) \circ F) [(1 \dots N)]$
92	91 16	eqtr4di	$⊢ φ \to ⋃_{n = 1}^{N} ((.) \circ F) (n) = L$
93		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
94		elfznn	$⊢ n \in (1 \dots N) \to n \in ℕ$
95		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to ((.) \circ F) (n) = (.) (F (n))$
96	1 94 95	syl2an	$⊢ (φ \land n \in (1 \dots N)) \to ((.) \circ F) (n) = (.) (F (n))$
97		ffvelcdm	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land n \in ℕ) \to F (n) \in (\leq \cap ℝ^{2})$
98	1 94 97	syl2an	$⊢ (φ \land n \in (1 \dots N)) \to F (n) \in (\leq \cap ℝ^{2})$
99	98	elin2d	$⊢ (φ \land n \in (1 \dots N)) \to F (n) \in ℝ^{2}$
100		1st2nd2	$⊢ F (n) \in ℝ^{2} \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
101	99 100	syl	$⊢ (φ \land n \in (1 \dots N)) \to F (n) = ⟨1^{st} (F (n)), 2^{nd} (F (n))⟩$
102	101	fveq2d	$⊢ (φ \land n \in (1 \dots N)) \to (.) (F (n)) = (.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
103		df-ov	$⊢ (1^{st} (F (n)), 2^{nd} (F (n))) = (.) (⟨1^{st} (F (n)), 2^{nd} (F (n))⟩)$
104	102 103	eqtr4di	$⊢ (φ \land n \in (1 \dots N)) \to (.) (F (n)) = (1^{st} (F (n)), 2^{nd} (F (n)))$
105	96 104	eqtrd	$⊢ (φ \land n \in (1 \dots N)) \to ((.) \circ F) (n) = (1^{st} (F (n)), 2^{nd} (F (n)))$
106		ioombl	$⊢ (1^{st} (F (n)), 2^{nd} (F (n))) \in dom vol$
107	105 106	eqeltrdi	$⊢ (φ \land n \in (1 \dots N)) \to ((.) \circ F) (n) \in dom vol$
108	107	ralrimiva	$⊢ φ \to \forall n \in (1 \dots N) ((.) \circ F) (n) \in dom vol$
109		finiunmbl	$⊢ ((1 \dots N) \in Fin \land \forall n \in (1 \dots N) ((.) \circ F) (n) \in dom vol) \to ⋃_{n = 1}^{N} ((.) \circ F) (n) \in dom vol$
110	93 108 109	syl2anc	$⊢ φ \to ⋃_{n = 1}^{N} ((.) \circ F) (n) \in dom vol$
111	92 110	eqeltrrd	$⊢ φ \to L \in dom vol$
112		mblsplit	$⊢ (L \in dom vol \land K \subseteq ℝ \land {vol}^{} (K) \in ℝ) \to {vol}^{} (K) = {vol}^{} (K \cap L) + {vol}^{} (K ∖ L)$
113	111 34 42 112	syl3anc	$⊢ φ \to {vol}^{} (K) = {vol}^{} (K \cap L) + {vol}^{*} (K ∖ L)$
114	113	oveq1d	$⊢ φ \to {vol}^{} (K) + C = {vol}^{} (K \cap L) + {vol}^{*} (K ∖ L) + C$
115	80 114	eqtr4d	$⊢ φ \to {vol}^{} (K \cap L) + C + {vol}^{} (K ∖ L) = {vol}^{*} (K) + C$
116	76 115	breqtrd	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) \leq {vol}^{*} (K) + C$
117	5 49	readdcld	$⊢ φ \to {vol}^{*} (E) + C \in ℝ$
118	9	ovollb	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land K \subseteq ⋃ ran ((.) \circ G)) \to {vol}^{} (K) \leq sup (ran T ℝ^{} <)$
119	7 33 118	sylancl	$⊢ φ \to {vol}^{} (K) \leq sup (ran T ℝ^{} <)$
120	42 35 117 119 10	letrd	$⊢ φ \to {vol}^{} (K) \leq {vol}^{} (E) + C$
121	42 117 49 120	leadd1dd	$⊢ φ \to {vol}^{} (K) + C \leq {vol}^{} (E) + C + C$
122	5	recnd	$⊢ φ \to {vol}^{*} (E) \in ℂ$
123	122 78 78	addassd	$⊢ φ \to {vol}^{} (E) + C + C = {vol}^{} (E) + C + C$
124	121 123	breqtrd	$⊢ φ \to {vol}^{} (K) + C \leq {vol}^{} (E) + C + C$
125	48 59 58 116 124	letrd	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) \leq {vol}^{*} (E) + C + C$
126	48 58 50 125	leadd1dd	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) + C + C \leq {vol}^{*} (E) + (C + C) + C + C$
127	50	recnd	$⊢ φ \to C + C \in ℂ$
128	122 127 127	addassd	$⊢ φ \to {vol}^{} (E) + (C + C) + C + C = {vol}^{} (E) + (C + C) + (C + C)$
129		2t2e4	$⊢ 2 \cdot 2 = 4$
130	129	oveq1i	$⊢ 2 \cdot 2 C = 4 C$
131		2cnd	$⊢ φ \to 2 \in ℂ$
132	131 131 78	mulassd	$⊢ φ \to 2 \cdot 2 C = 2 2 C$
133	78	2timesd	$⊢ φ \to 2 C = C + C$
134	133	oveq2d	$⊢ φ \to 2 2 C = 2 (C + C)$
135	127	2timesd	$⊢ φ \to 2 (C + C) = C + C + C + C$
136	132 134 135	3eqtrd	$⊢ φ \to 2 \cdot 2 C = C + C + C + C$
137	130 136	eqtr3id	$⊢ φ \to 4 C = C + C + C + C$
138	137	oveq2d	$⊢ φ \to {vol}^{} (E) + 4 C = {vol}^{} (E) + (C + C) + (C + C)$
139	128 138	eqtr4d	$⊢ φ \to {vol}^{} (E) + (C + C) + C + C = {vol}^{} (E) + 4 C$
140	126 139	breqtrd	$⊢ φ \to {vol}^{} (K \cap A) + {vol}^{} (K ∖ A) + C + C \leq {vol}^{*} (E) + 4 C$
141	29 51 55 57 140	letrd	$⊢ φ \to {vol}^{} (E \cap A) + {vol}^{} (E ∖ A) \leq {vol}^{*} (E) + 4 C$

Metamath Proof Explorer

Theorem uniioombllem5

Proof