ovnovollem3

Description: The 1-dimensional Lebesgue outer measure agrees with the Lebesgue outer measure on subsets of Real numbers. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnovollem3.a	$⊢ φ \to A \in V$
	ovnovollem3.b	$⊢ φ \to B \subseteq ℝ$
	ovnovollem3.m	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))\}$
	ovnovollem3.n	$⊢ N = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))\}$
Assertion	ovnovollem3	$⊢ φ \to voln* (\{A\}) (B^{\{A\}}) = {vol}^{*} (B)$

Proof

Step	Hyp	Ref	Expression
1		ovnovollem3.a	$⊢ φ \to A \in V$
2		ovnovollem3.b	$⊢ φ \to B \subseteq ℝ$
3		ovnovollem3.m	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))\}$
4		ovnovollem3.n	$⊢ N = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))\}$
5	1	snn0d	$⊢ φ \to \{A\} \neq \emptyset$
6	5	neneqd	$⊢ φ \to \neg \{A\} = \emptyset$
7	6	iffalsed	$⊢ φ \to if (\{A\} = \emptyset, 0, inf (M ℝ^{} <)) = inf (M ℝ^{} <)$
8		snfi	$⊢ \{A\} \in Fin$
9	8	a1i	$⊢ φ \to \{A\} \in Fin$
10		reex	$⊢ ℝ \in V$
11	10	a1i	$⊢ φ \to ℝ \in V$
12		mapss	$⊢ (ℝ \in V \land B \subseteq ℝ) \to B^{\{A\}} \subseteq ℝ^{\{A\}}$
13	11 2 12	syl2anc	$⊢ φ \to B^{\{A\}} \subseteq ℝ^{\{A\}}$
14	9 13 3	ovnval2	$⊢ φ \to voln* (\{A\}) (B^{\{A\}}) = if (\{A\} = \emptyset, 0, inf (M ℝ^{*} <))$
15	2 4	ovolval5	$⊢ φ \to {vol}^{} (B) = inf (N ℝ^{} <)$
16	1	ad2antrr	$⊢ ((φ \land f \in ({ℝ^{2}}^{ℕ})) \land (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))) \to A \in V$
17		simplr	$⊢ ((φ \land f \in ({ℝ^{2}}^{ℕ})) \land (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))) \to f \in ({ℝ^{2}}^{ℕ})$
18		fveq2	$⊢ n = j \to f (n) = f (j)$
19	18	opeq2d	$⊢ n = j \to ⟨A, f (n)⟩ = ⟨A, f (j)⟩$
20	19	sneqd	$⊢ n = j \to \{⟨A, f (n)⟩\} = \{⟨A, f (j)⟩\}$
21	20	cbvmptv	$⊢ (n \in ℕ ⟼ \{⟨A, f (n)⟩\}) = (j \in ℕ ⟼ \{⟨A, f (j)⟩\})$
22		simprl	$⊢ ((φ \land f \in ({ℝ^{2}}^{ℕ})) \land (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))) \to B \subseteq ⋃ ran ([.) \circ f)$
23	11 2	ssexd	$⊢ φ \to B \in V$
24	23	adantr	$⊢ (φ \land f \in ({ℝ^{2}}^{ℕ})) \to B \in V$
25	24	adantr	$⊢ ((φ \land f \in ({ℝ^{2}}^{ℕ})) \land (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))) \to B \in V$
26		simprr	$⊢ ((φ \land f \in ({ℝ^{2}}^{ℕ})) \land (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))) \to z = sum^((vol \circ [.)) \circ f)$
27	16 17 21 22 25 26	ovnovollem1	$⊢ ((φ \land f \in ({ℝ^{2}}^{ℕ})) \land (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))) \to \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))$
28	27	rexlimdva2	$⊢ φ \to (\exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f)) \to \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k))))))$
29	1	3ad2ant1	$⊢ (φ \land i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))) \to A \in V$
30	23	3ad2ant1	$⊢ (φ \land i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))) \to B \in V$
31		simp2	$⊢ (φ \land i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))) \to i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ})$
32		simp3l	$⊢ (φ \land i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))) \to B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k)$
33		fveq2	$⊢ j = n \to i (j) = i (n)$
34	33	coeq2d	$⊢ j = n \to [.) \circ i (j) = [.) \circ i (n)$
35	34	fveq1d	$⊢ j = n \to ([.) \circ i (j)) (k) = ([.) \circ i (n)) (k)$
36	35	ixpeq2dv	$⊢ j = n \to \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) = \underset{k \in \{A\}}{⨉} ([.) \circ i (n)) (k)$
37		fveq2	$⊢ k = l \to ([.) \circ i (n)) (k) = ([.) \circ i (n)) (l)$
38	37	cbvixpv	$⊢ \underset{k \in \{A\}}{⨉} ([.) \circ i (n)) (k) = \underset{l \in \{A\}}{⨉} ([.) \circ i (n)) (l)$
39	38	a1i	$⊢ j = n \to \underset{k \in \{A\}}{⨉} ([.) \circ i (n)) (k) = \underset{l \in \{A\}}{⨉} ([.) \circ i (n)) (l)$
40	36 39	eqtrd	$⊢ j = n \to \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) = \underset{l \in \{A\}}{⨉} ([.) \circ i (n)) (l)$
41	40	cbviunv	$⊢ ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) = ⋃_{n \in ℕ} \underset{l \in \{A\}}{⨉} ([.) \circ i (n)) (l)$
42	41	sseq2i	$⊢ B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \leftrightarrow B^{\{A\}} \subseteq ⋃_{n \in ℕ} \underset{l \in \{A\}}{⨉} ([.) \circ i (n)) (l)$
43	42	biimpi	$⊢ B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \to B^{\{A\}} \subseteq ⋃_{n \in ℕ} \underset{l \in \{A\}}{⨉} ([.) \circ i (n)) (l)$
44	32 43	syl	$⊢ (φ \land i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))) \to B^{\{A\}} \subseteq ⋃_{n \in ℕ} \underset{l \in \{A\}}{⨉} ([.) \circ i (n)) (l)$
45		simp3r	$⊢ (φ \land i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))) \to z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k))))$
46	35	fveq2d	$⊢ j = n \to vol (([.) \circ i (j)) (k)) = vol (([.) \circ i (n)) (k))$
47	46	prodeq2ad	$⊢ j = n \to \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)) = \prod_{k \in \{A\}} vol (([.) \circ i (n)) (k))$
48	37	fveq2d	$⊢ k = l \to vol (([.) \circ i (n)) (k)) = vol (([.) \circ i (n)) (l))$
49	48	cbvprodv	$⊢ \prod_{k \in \{A\}} vol (([.) \circ i (n)) (k)) = \prod_{l \in \{A\}} vol (([.) \circ i (n)) (l))$
50	49	a1i	$⊢ j = n \to \prod_{k \in \{A\}} vol (([.) \circ i (n)) (k)) = \prod_{l \in \{A\}} vol (([.) \circ i (n)) (l))$
51	47 50	eqtrd	$⊢ j = n \to \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)) = \prod_{l \in \{A\}} vol (([.) \circ i (n)) (l))$
52	51	cbvmptv	$⊢ (j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k))) = (n \in ℕ ⟼ \prod_{l \in \{A\}} vol (([.) \circ i (n)) (l)))$
53	52	fveq2i	$⊢ sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))) = sum^((n \in ℕ ⟼ \prod_{l \in \{A\}} vol (([.) \circ i (n)) (l))))$
54	53	eqeq2i	$⊢ z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))) \leftrightarrow z = sum^((n \in ℕ ⟼ \prod_{l \in \{A\}} vol (([.) \circ i (n)) (l))))$
55	54	biimpi	$⊢ z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))) \to z = sum^((n \in ℕ ⟼ \prod_{l \in \{A\}} vol (([.) \circ i (n)) (l))))$
56	45 55	syl	$⊢ (φ \land i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))) \to z = sum^((n \in ℕ ⟼ \prod_{l \in \{A\}} vol (([.) \circ i (n)) (l))))$
57		fveq2	$⊢ m = n \to i (m) = i (n)$
58	57	fveq1d	$⊢ m = n \to i (m) (A) = i (n) (A)$
59	58	cbvmptv	$⊢ (m \in ℕ ⟼ i (m) (A)) = (n \in ℕ ⟼ i (n) (A))$
60	29 30 31 44 56 59	ovnovollem2	$⊢ (φ \land i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \land (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))) \to \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))$
61	60	3exp	$⊢ φ \to (i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \to ((B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k))))) \to \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))))$
62	61	rexlimdv	$⊢ φ \to (\exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k))))) \to \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f)))$
63	28 62	impbid	$⊢ φ \to (\exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f)) \leftrightarrow \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k))))))$
64	63	rabbidv	$⊢ φ \to \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))\} = \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))\}$
65	4	a1i	$⊢ φ \to N = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land z = sum^((vol \circ [.)) \circ f))\}$
66	3	a1i	$⊢ φ \to M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) (B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ i (j)) (k)))))\}$
67	64 65 66	3eqtr4d	$⊢ φ \to N = M$
68	67	infeq1d	$⊢ φ \to inf (N ℝ^{} <) = inf (M ℝ^{} <)$
69	15 68	eqtrd	$⊢ φ \to {vol}^{} (B) = inf (M ℝ^{} <)$
70	7 14 69	3eqtr4d	$⊢ φ \to voln* (\{A\}) (B^{\{A\}}) = {vol}^{*} (B)$

Metamath Proof Explorer

Theorem ovnovollem3

Proof