ovolval2lem

Description: The value of the Lebesgue outer measure for subsets of the reals, expressed using sum^ . (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Hypothesis	ovolval2lem.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	Assertion	ovolval2lem	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ F)) = ran (n \in ℕ ⟼ \sum_{k = 1}^{n} vol (([.) \circ F) (k)))$

Proof

Step	Hyp	Ref	Expression
1		ovolval2lem.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
2		reex	$⊢ ℝ \in V$
3	2 2	xpex	$⊢ ℝ^{2} \in V$
4		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
5		mapss	$⊢ (ℝ^{2} \in V \land \leq \cap ℝ^{2} \subseteq ℝ^{2}) \to {(\leq \cap ℝ^{2})}^{ℕ} \subseteq {ℝ^{2}}^{ℕ}$
6	3 4 5	mp2an	$⊢ {(\leq \cap ℝ^{2})}^{ℕ} \subseteq {ℝ^{2}}^{ℕ}$
7	3	inex2	$⊢ \leq \cap ℝ^{2} \in V$
8	7	a1i	$⊢ φ \to \leq \cap ℝ^{2} \in V$
9		nnex	$⊢ ℕ \in V$
10	9	a1i	$⊢ φ \to ℕ \in V$
11	8 10	elmapd	$⊢ φ \to (F \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F : ℕ ⟶ \leq \cap ℝ^{2})$
12	1 11	mpbird	$⊢ φ \to F \in ({(\leq \cap ℝ^{2})}^{ℕ})$
13	6 12	sselid	$⊢ φ \to F \in ({ℝ^{2}}^{ℕ})$
14		1zzd	$⊢ F \in ({ℝ^{2}}^{ℕ}) \to 1 \in ℤ$
15		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
16		elmapi	$⊢ F \in ({ℝ^{2}}^{ℕ}) \to F : ℕ ⟶ ℝ^{2}$
17	16	adantr	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to F : ℕ ⟶ ℝ^{2}$
18		simpr	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to k \in ℕ$
19	17 18	fvovco	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to ([.) \circ F) (k) = [1^{st} (F (k)), 2^{nd} (F (k)))$
20	19	fveq2d	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to vol (([.) \circ F) (k)) = vol ([1^{st} (F (k)), 2^{nd} (F (k))))$
21	16	ffvelcdmda	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to F (k) \in ℝ^{2}$
22		xp1st	$⊢ F (k) \in ℝ^{2} \to 1^{st} (F (k)) \in ℝ$
23	21 22	syl	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to 1^{st} (F (k)) \in ℝ$
24		xp2nd	$⊢ F (k) \in ℝ^{2} \to 2^{nd} (F (k)) \in ℝ$
25	21 24	syl	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to 2^{nd} (F (k)) \in ℝ$
26		volicore	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ) \to vol ([1^{st} (F (k)), 2^{nd} (F (k)))) \in ℝ$
27	23 25 26	syl2anc	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to vol ([1^{st} (F (k)), 2^{nd} (F (k)))) \in ℝ$
28	20 27	eqeltrd	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to vol (([.) \circ F) (k)) \in ℝ$
29	28	recnd	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to vol (([.) \circ F) (k)) \in ℂ$
30		eqid	$⊢ (n \in ℕ ⟼ \sum_{k = 1}^{n} vol (([.) \circ F) (k))) = (n \in ℕ ⟼ \sum_{k = 1}^{n} vol (([.) \circ F) (k)))$
31		eqid	$⊢ seq 1 (+ (k \in ℕ ⟼ vol (([.) \circ F) (k)))) = seq 1 (+ (k \in ℕ ⟼ vol (([.) \circ F) (k))))$
32	14 15 29 30 31	fsumsermpt	$⊢ F \in ({ℝ^{2}}^{ℕ}) \to (n \in ℕ ⟼ \sum_{k = 1}^{n} vol (([.) \circ F) (k))) = seq 1 (+ (k \in ℕ ⟼ vol (([.) \circ F) (k))))$
33	13 32	syl	$⊢ φ \to (n \in ℕ ⟼ \sum_{k = 1}^{n} vol (([.) \circ F) (k))) = seq 1 (+ (k \in ℕ ⟼ vol (([.) \circ F) (k))))$
34		simpr	$⊢ ((φ \land k \in ℕ) \land 1^{st} (F (k)) < 2^{nd} (F (k))) \to 1^{st} (F (k)) < 2^{nd} (F (k))$
35	34	iftrued	$⊢ ((φ \land k \in ℕ) \land 1^{st} (F (k)) < 2^{nd} (F (k))) \to if (1^{st} (F (k)) < 2^{nd} (F (k)), 2^{nd} (F (k)) - 1^{st} (F (k)), 0) = 2^{nd} (F (k)) - 1^{st} (F (k))$
36	13 23	sylan	$⊢ (φ \land k \in ℕ) \to 1^{st} (F (k)) \in ℝ$
37	36	adantr	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to 1^{st} (F (k)) \in ℝ$
38	13 25	sylan	$⊢ (φ \land k \in ℕ) \to 2^{nd} (F (k)) \in ℝ$
39	38	adantr	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to 2^{nd} (F (k)) \in ℝ$
40		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
41	40 37	sselid	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to 1^{st} (F (k)) \in ℝ^{*}$
42	40 39	sselid	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to 2^{nd} (F (k)) \in ℝ^{*}$
43		xpss	$⊢ ℝ^{2} \subseteq V \times V$
44	43 21	sselid	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to F (k) \in (V \times V)$
45		1st2ndb	$⊢ F (k) \in (V \times V) \leftrightarrow F (k) = ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩$
46	44 45	sylib	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to F (k) = ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩$
47	13 46	sylan	$⊢ (φ \land k \in ℕ) \to F (k) = ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩$
48	47	eqcomd	$⊢ (φ \land k \in ℕ) \to ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩ = F (k)$
49		inss1	$⊢ \leq \cap ℝ^{2} \subseteq \leq$
50	49	a1i	$⊢ φ \to \leq \cap ℝ^{2} \subseteq \leq$
51	1 50	fssd	$⊢ φ \to F : ℕ ⟶ \leq$
52	51	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to F (k) \in \leq$
53	48 52	eqeltrd	$⊢ (φ \land k \in ℕ) \to ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩ \in \leq$
54		df-br	$⊢ 1^{st} (F (k)) \leq 2^{nd} (F (k)) \leftrightarrow ⟨1^{st} (F (k)), 2^{nd} (F (k))⟩ \in \leq$
55	53 54	sylibr	$⊢ (φ \land k \in ℕ) \to 1^{st} (F (k)) \leq 2^{nd} (F (k))$
56	55	adantr	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to 1^{st} (F (k)) \leq 2^{nd} (F (k))$
57		simpr	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to \neg 1^{st} (F (k)) < 2^{nd} (F (k))$
58	39 37	lenltd	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to (2^{nd} (F (k)) \leq 1^{st} (F (k)) \leftrightarrow \neg 1^{st} (F (k)) < 2^{nd} (F (k)))$
59	57 58	mpbird	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to 2^{nd} (F (k)) \leq 1^{st} (F (k))$
60	41 42 56 59	xrletrid	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to 1^{st} (F (k)) = 2^{nd} (F (k))$
61		simp3	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to 1^{st} (F (k)) = 2^{nd} (F (k))$
62		simp1	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to 1^{st} (F (k)) \in ℝ$
63		simp2	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to 2^{nd} (F (k)) \in ℝ$
64	62 63	eqleltd	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to (1^{st} (F (k)) = 2^{nd} (F (k)) \leftrightarrow (1^{st} (F (k)) \leq 2^{nd} (F (k)) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))))$
65	61 64	mpbid	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to (1^{st} (F (k)) \leq 2^{nd} (F (k)) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k)))$
66	65	simprd	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to \neg 1^{st} (F (k)) < 2^{nd} (F (k))$
67	66	iffalsed	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to if (1^{st} (F (k)) < 2^{nd} (F (k)), 2^{nd} (F (k)) - 1^{st} (F (k)), 0) = 0$
68	63	recnd	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to 2^{nd} (F (k)) \in ℂ$
69	61	eqcomd	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to 2^{nd} (F (k)) = 1^{st} (F (k))$
70	68 69	subeq0bd	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to 2^{nd} (F (k)) - 1^{st} (F (k)) = 0$
71	67 70	eqtr4d	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ \land 1^{st} (F (k)) = 2^{nd} (F (k))) \to if (1^{st} (F (k)) < 2^{nd} (F (k)), 2^{nd} (F (k)) - 1^{st} (F (k)), 0) = 2^{nd} (F (k)) - 1^{st} (F (k))$
72	37 39 60 71	syl3anc	$⊢ ((φ \land k \in ℕ) \land \neg 1^{st} (F (k)) < 2^{nd} (F (k))) \to if (1^{st} (F (k)) < 2^{nd} (F (k)), 2^{nd} (F (k)) - 1^{st} (F (k)), 0) = 2^{nd} (F (k)) - 1^{st} (F (k))$
73	35 72	pm2.61dan	$⊢ (φ \land k \in ℕ) \to if (1^{st} (F (k)) < 2^{nd} (F (k)), 2^{nd} (F (k)) - 1^{st} (F (k)), 0) = 2^{nd} (F (k)) - 1^{st} (F (k))$
74		volico	$⊢ (1^{st} (F (k)) \in ℝ \land 2^{nd} (F (k)) \in ℝ) \to vol ([1^{st} (F (k)), 2^{nd} (F (k)))) = if (1^{st} (F (k)) < 2^{nd} (F (k)), 2^{nd} (F (k)) - 1^{st} (F (k)), 0)$
75	36 38 74	syl2anc	$⊢ (φ \land k \in ℕ) \to vol ([1^{st} (F (k)), 2^{nd} (F (k)))) = if (1^{st} (F (k)) < 2^{nd} (F (k)), 2^{nd} (F (k)) - 1^{st} (F (k)), 0)$
76	36 38 55	abssuble0d	$⊢ (φ \land k \in ℕ) \to \|1^{st} (F (k)) - 2^{nd} (F (k))\| = 2^{nd} (F (k)) - 1^{st} (F (k))$
77	73 75 76	3eqtr4d	$⊢ (φ \land k \in ℕ) \to vol ([1^{st} (F (k)), 2^{nd} (F (k)))) = \|1^{st} (F (k)) - 2^{nd} (F (k))\|$
78	13	adantr	$⊢ (φ \land k \in ℕ) \to F \in ({ℝ^{2}}^{ℕ})$
79		simpr	$⊢ (φ \land k \in ℕ) \to k \in ℕ$
80	78 79 20	syl2anc	$⊢ (φ \land k \in ℕ) \to vol (([.) \circ F) (k)) = vol ([1^{st} (F (k)), 2^{nd} (F (k))))$
81	46	fveq2d	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to (abs \circ -) (F (k)) = (abs \circ -) (⟨1^{st} (F (k)), 2^{nd} (F (k))⟩)$
82		df-ov	$⊢ 1^{st} (F (k)) (abs \circ -) 2^{nd} (F (k)) = (abs \circ -) (⟨1^{st} (F (k)), 2^{nd} (F (k))⟩)$
83	82	eqcomi	$⊢ (abs \circ -) (⟨1^{st} (F (k)), 2^{nd} (F (k))⟩) = 1^{st} (F (k)) (abs \circ -) 2^{nd} (F (k))$
84	83	a1i	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to (abs \circ -) (⟨1^{st} (F (k)), 2^{nd} (F (k))⟩) = 1^{st} (F (k)) (abs \circ -) 2^{nd} (F (k))$
85	23	recnd	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to 1^{st} (F (k)) \in ℂ$
86	25	recnd	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to 2^{nd} (F (k)) \in ℂ$
87		eqid	$⊢ abs \circ - = abs \circ -$
88	87	cnmetdval	$⊢ (1^{st} (F (k)) \in ℂ \land 2^{nd} (F (k)) \in ℂ) \to 1^{st} (F (k)) (abs \circ -) 2^{nd} (F (k)) = \|1^{st} (F (k)) - 2^{nd} (F (k))\|$
89	85 86 88	syl2anc	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to 1^{st} (F (k)) (abs \circ -) 2^{nd} (F (k)) = \|1^{st} (F (k)) - 2^{nd} (F (k))\|$
90	81 84 89	3eqtrd	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land k \in ℕ) \to (abs \circ -) (F (k)) = \|1^{st} (F (k)) - 2^{nd} (F (k))\|$
91	78 79 90	syl2anc	$⊢ (φ \land k \in ℕ) \to (abs \circ -) (F (k)) = \|1^{st} (F (k)) - 2^{nd} (F (k))\|$
92	77 80 91	3eqtr4d	$⊢ (φ \land k \in ℕ) \to vol (([.) \circ F) (k)) = (abs \circ -) (F (k))$
93	92	mpteq2dva	$⊢ φ \to (k \in ℕ ⟼ vol (([.) \circ F) (k))) = (k \in ℕ ⟼ (abs \circ -) (F (k)))$
94	13 16	syl	$⊢ φ \to F : ℕ ⟶ ℝ^{2}$
95		rr2sscn2	$⊢ ℝ^{2} \subseteq ℂ \times ℂ$
96	95	a1i	$⊢ φ \to ℝ^{2} \subseteq ℂ \times ℂ$
97		absf	$⊢ abs : ℂ ⟶ ℝ$
98		subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
99		fco	$⊢ (abs : ℂ ⟶ ℝ \land - : ℂ \times ℂ ⟶ ℂ) \to (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
100	97 98 99	mp2an	$⊢ (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
101	100	a1i	$⊢ φ \to (abs \circ -) : ℂ \times ℂ ⟶ ℝ$
102	94 96 101	fcomptss	$⊢ φ \to (abs \circ -) \circ F = (k \in ℕ ⟼ (abs \circ -) (F (k)))$
103	93 102	eqtr4d	$⊢ φ \to (k \in ℕ ⟼ vol (([.) \circ F) (k))) = (abs \circ -) \circ F$
104	103	seqeq3d	$⊢ φ \to seq 1 (+ (k \in ℕ ⟼ vol (([.) \circ F) (k)))) = seq 1 (+ ((abs \circ -) \circ F))$
105	33 104	eqtr2d	$⊢ φ \to seq 1 (+ ((abs \circ -) \circ F)) = (n \in ℕ ⟼ \sum_{k = 1}^{n} vol (([.) \circ F) (k)))$
106	105	rneqd	$⊢ φ \to ran seq 1 (+ ((abs \circ -) \circ F)) = ran (n \in ℕ ⟼ \sum_{k = 1}^{n} vol (([.) \circ F) (k)))$

Metamath Proof Explorer

Theorem ovolval2lem

Proof