ovnovollem2

Description: if I is a cover of ( B ^m { A } ) in RR^ 1 , then F is the corresponding cover in the reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovnovollem2.a	$⊢ φ \to A \in V$
	ovnovollem2.b	$⊢ φ \to B \in W$
	ovnovollem2.i	$⊢ φ \to I \in ({({ℝ^{2}}^{\{A\}})}^{ℕ})$
	ovnovollem2.s	$⊢ φ \to B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k)$
	ovnovollem2.z	$⊢ φ \to Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))))$
	ovnovollem2.f	$⊢ F = (j \in ℕ ⟼ I (j) (A))$
Assertion	ovnovollem2	$⊢ φ \to \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land Z = sum^((vol \circ [.)) \circ f))$

Proof

Step	Hyp	Ref	Expression
1		ovnovollem2.a	$⊢ φ \to A \in V$
2		ovnovollem2.b	$⊢ φ \to B \in W$
3		ovnovollem2.i	$⊢ φ \to I \in ({({ℝ^{2}}^{\{A\}})}^{ℕ})$
4		ovnovollem2.s	$⊢ φ \to B^{\{A\}} \subseteq ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k)$
5		ovnovollem2.z	$⊢ φ \to Z = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))))$
6		ovnovollem2.f	$⊢ F = (j \in ℕ ⟼ I (j) (A))$
7		elmapi	$⊢ I \in ({({ℝ^{2}}^{\{A\}})}^{ℕ}) \to I : ℕ ⟶ {ℝ^{2}}^{\{A\}}$
8	3 7	syl	$⊢ φ \to I : ℕ ⟶ {ℝ^{2}}^{\{A\}}$
9	8	adantr	$⊢ (φ \land j \in ℕ) \to I : ℕ ⟶ {ℝ^{2}}^{\{A\}}$
10		simpr	$⊢ (φ \land j \in ℕ) \to j \in ℕ$
11	9 10	ffvelcdmd	$⊢ (φ \land j \in ℕ) \to I (j) \in ({ℝ^{2}}^{\{A\}})$
12		elmapi	$⊢ I (j) \in ({ℝ^{2}}^{\{A\}}) \to I (j) : \{A\} ⟶ ℝ^{2}$
13	11 12	syl	$⊢ (φ \land j \in ℕ) \to I (j) : \{A\} ⟶ ℝ^{2}$
14		snidg	$⊢ A \in V \to A \in \{A\}$
15	1 14	syl	$⊢ φ \to A \in \{A\}$
16	15	adantr	$⊢ (φ \land j \in ℕ) \to A \in \{A\}$
17	13 16	ffvelcdmd	$⊢ (φ \land j \in ℕ) \to I (j) (A) \in ℝ^{2}$
18	17 6	fmptd	$⊢ φ \to F : ℕ ⟶ ℝ^{2}$
19		reex	$⊢ ℝ \in V$
20	19 19	xpex	$⊢ ℝ^{2} \in V$
21		nnex	$⊢ ℕ \in V$
22	20 21	elmap	$⊢ F \in ({ℝ^{2}}^{ℕ}) \leftrightarrow F : ℕ ⟶ ℝ^{2}$
23	22	a1i	$⊢ φ \to (F \in ({ℝ^{2}}^{ℕ}) \leftrightarrow F : ℕ ⟶ ℝ^{2})$
24	18 23	mpbird	$⊢ φ \to F \in ({ℝ^{2}}^{ℕ})$
25		elsni	$⊢ k \in \{A\} \to k = A$
26	25	fveq2d	$⊢ k \in \{A\} \to ([.) \circ I (j)) (k) = ([.) \circ I (j)) (A)$
27	26	adantl	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to ([.) \circ I (j)) (k) = ([.) \circ I (j)) (A)$
28		elmapfun	$⊢ I (j) \in ({ℝ^{2}}^{\{A\}}) \to Fun I (j)$
29	11 28	syl	$⊢ (φ \land j \in ℕ) \to Fun I (j)$
30	13	fdmd	$⊢ (φ \land j \in ℕ) \to dom I (j) = \{A\}$
31	30	eqcomd	$⊢ (φ \land j \in ℕ) \to \{A\} = dom I (j)$
32	16 31	eleqtrd	$⊢ (φ \land j \in ℕ) \to A \in dom I (j)$
33		fvco	$⊢ (Fun I (j) \land A \in dom I (j)) \to ([.) \circ I (j)) (A) = [.) (I (j) (A))$
34	29 32 33	syl2anc	$⊢ (φ \land j \in ℕ) \to ([.) \circ I (j)) (A) = [.) (I (j) (A))$
35	34	adantr	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to ([.) \circ I (j)) (A) = [.) (I (j) (A))$
36		id	$⊢ j \in ℕ \to j \in ℕ$
37		fvexd	$⊢ j \in ℕ \to I (j) (A) \in V$
38	6	fvmpt2	$⊢ (j \in ℕ \land I (j) (A) \in V) \to F (j) = I (j) (A)$
39	36 37 38	syl2anc	$⊢ j \in ℕ \to F (j) = I (j) (A)$
40	39	eqcomd	$⊢ j \in ℕ \to I (j) (A) = F (j)$
41	40	fveq2d	$⊢ j \in ℕ \to [.) (I (j) (A)) = [.) (F (j))$
42	41	adantl	$⊢ (φ \land j \in ℕ) \to [.) (I (j) (A)) = [.) (F (j))$
43	18	ffund	$⊢ φ \to Fun F$
44	43	adantr	$⊢ (φ \land j \in ℕ) \to Fun F$
45	6 17	dmmptd	$⊢ φ \to dom F = ℕ$
46	45	eqcomd	$⊢ φ \to ℕ = dom F$
47	46	adantr	$⊢ (φ \land j \in ℕ) \to ℕ = dom F$
48	10 47	eleqtrd	$⊢ (φ \land j \in ℕ) \to j \in dom F$
49		fvco	$⊢ (Fun F \land j \in dom F) \to ([.) \circ F) (j) = [.) (F (j))$
50	44 48 49	syl2anc	$⊢ (φ \land j \in ℕ) \to ([.) \circ F) (j) = [.) (F (j))$
51	50	eqcomd	$⊢ (φ \land j \in ℕ) \to [.) (F (j)) = ([.) \circ F) (j)$
52	42 51	eqtrd	$⊢ (φ \land j \in ℕ) \to [.) (I (j) (A)) = ([.) \circ F) (j)$
53	52	adantr	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to [.) (I (j) (A)) = ([.) \circ F) (j)$
54	27 35 53	3eqtrd	$⊢ ((φ \land j \in ℕ) \land k \in \{A\}) \to ([.) \circ I (j)) (k) = ([.) \circ F) (j)$
55	54	ixpeq2dva	$⊢ (φ \land j \in ℕ) \to \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) = \underset{k \in \{A\}}{⨉} ([.) \circ F) (j)$
56		snex	$⊢ \{A\} \in V$
57		fvex	$⊢ ([.) \circ F) (j) \in V$
58	56 57	ixpconst	$⊢ \underset{k \in \{A\}}{⨉} ([.) \circ F) (j) = {([.) \circ F) (j)}^{\{A\}}$
59	58	a1i	$⊢ (φ \land j \in ℕ) \to \underset{k \in \{A\}}{⨉} ([.) \circ F) (j) = {([.) \circ F) (j)}^{\{A\}}$
60	55 59	eqtrd	$⊢ (φ \land j \in ℕ) \to \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) = {([.) \circ F) (j)}^{\{A\}}$
61	60	iuneq2dv	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) = ⋃_{j \in ℕ} ({([.) \circ F) (j)}^{\{A\}})$
62		nfv	$⊢ Ⅎ j φ$
63	21	a1i	$⊢ φ \to ℕ \in V$
64		fvexd	$⊢ (φ \land j \in ℕ) \to ([.) \circ F) (j) \in V$
65	62 63 64 1	iunmapsn	$⊢ φ \to ⋃_{j \in ℕ} ({([.) \circ F) (j)}^{\{A\}}) = {⋃_{j \in ℕ} ([.) \circ F) (j)}^{\{A\}}$
66	61 65	eqtrd	$⊢ φ \to ⋃_{j \in ℕ} \underset{k \in \{A\}}{⨉} ([.) \circ I (j)) (k) = {⋃_{j \in ℕ} ([.) \circ F) (j)}^{\{A\}}$
67	4 66	sseqtrd	$⊢ φ \to B^{\{A\}} \subseteq {⋃_{j \in ℕ} ([.) \circ F) (j)}^{\{A\}}$
68	21 57	iunex	$⊢ ⋃_{j \in ℕ} ([.) \circ F) (j) \in V$
69	68	a1i	$⊢ φ \to ⋃_{j \in ℕ} ([.) \circ F) (j) \in V$
70	56	a1i	$⊢ φ \to \{A\} \in V$
71	15	ne0d	$⊢ φ \to \{A\} \neq \emptyset$
72	2 69 70 71	mapss2	$⊢ φ \to (B \subseteq ⋃_{j \in ℕ} ([.) \circ F) (j) \leftrightarrow B^{\{A\}} \subseteq {⋃_{j \in ℕ} ([.) \circ F) (j)}^{\{A\}})$
73	67 72	mpbird	$⊢ φ \to B \subseteq ⋃_{j \in ℕ} ([.) \circ F) (j)$
74		icof	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
75	74	a1i	$⊢ φ \to [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
76		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
77	76	a1i	$⊢ φ \to ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
78	75 77 18	fcoss	$⊢ φ \to ([.) \circ F) : ℕ ⟶ 𝒫 ℝ^{*}$
79	78	ffnd	$⊢ φ \to ([.) \circ F) Fn ℕ$
80		fniunfv	$⊢ ([.) \circ F) Fn ℕ \to ⋃_{j \in ℕ} ([.) \circ F) (j) = ⋃ ran ([.) \circ F)$
81	79 80	syl	$⊢ φ \to ⋃_{j \in ℕ} ([.) \circ F) (j) = ⋃ ran ([.) \circ F)$
82	73 81	sseqtrd	$⊢ φ \to B \subseteq ⋃ ran ([.) \circ F)$
83		nfcv	$⊢ \underline{Ⅎ} j F$
84		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
85		xpss2	$⊢ ℝ \subseteq ℝ^{} \to ℝ^{2} \subseteq ℝ \times ℝ^{}$
86	84 85	ax-mp	$⊢ ℝ^{2} \subseteq ℝ \times ℝ^{*}$
87	86	a1i	$⊢ φ \to ℝ^{2} \subseteq ℝ \times ℝ^{*}$
88	18 87	fssd	$⊢ φ \to F : ℕ ⟶ ℝ \times ℝ^{*}$
89	83 88	volicofmpt	$⊢ φ \to (vol \circ [.)) \circ F = (j \in ℕ ⟼ vol ([1^{st} (F (j)), 2^{nd} (F (j)))))$
90	1	adantr	$⊢ (φ \land j \in ℕ) \to A \in V$
91		fvexd	$⊢ (φ \land j \in ℕ) \to I (j) (A) \in V$
92	10 91 38	syl2anc	$⊢ (φ \land j \in ℕ) \to F (j) = I (j) (A)$
93	92 17	eqeltrd	$⊢ (φ \land j \in ℕ) \to F (j) \in ℝ^{2}$
94		1st2nd2	$⊢ F (j) \in ℝ^{2} \to F (j) = ⟨1^{st} (F (j)), 2^{nd} (F (j))⟩$
95	93 94	syl	$⊢ (φ \land j \in ℕ) \to F (j) = ⟨1^{st} (F (j)), 2^{nd} (F (j))⟩$
96	95	fveq2d	$⊢ (φ \land j \in ℕ) \to [.) (F (j)) = [.) (⟨1^{st} (F (j)), 2^{nd} (F (j))⟩)$
97		df-ov	$⊢ [1^{st} (F (j)), 2^{nd} (F (j))) = [.) (⟨1^{st} (F (j)), 2^{nd} (F (j))⟩)$
98	97	eqcomi	$⊢ [.) (⟨1^{st} (F (j)), 2^{nd} (F (j))⟩) = [1^{st} (F (j)), 2^{nd} (F (j)))$
99	98	a1i	$⊢ (φ \land j \in ℕ) \to [.) (⟨1^{st} (F (j)), 2^{nd} (F (j))⟩) = [1^{st} (F (j)), 2^{nd} (F (j)))$
100	50 96 99	3eqtrd	$⊢ (φ \land j \in ℕ) \to ([.) \circ F) (j) = [1^{st} (F (j)), 2^{nd} (F (j)))$
101	34 52 100	3eqtrd	$⊢ (φ \land j \in ℕ) \to ([.) \circ I (j)) (A) = [1^{st} (F (j)), 2^{nd} (F (j)))$
102	101	fveq2d	$⊢ (φ \land j \in ℕ) \to vol (([.) \circ I (j)) (A)) = vol ([1^{st} (F (j)), 2^{nd} (F (j))))$
103		xp1st	$⊢ F (j) \in ℝ^{2} \to 1^{st} (F (j)) \in ℝ$
104	93 103	syl	$⊢ (φ \land j \in ℕ) \to 1^{st} (F (j)) \in ℝ$
105		xp2nd	$⊢ F (j) \in ℝ^{2} \to 2^{nd} (F (j)) \in ℝ$
106	93 105	syl	$⊢ (φ \land j \in ℕ) \to 2^{nd} (F (j)) \in ℝ$
107		volicore	$⊢ (1^{st} (F (j)) \in ℝ \land 2^{nd} (F (j)) \in ℝ) \to vol ([1^{st} (F (j)), 2^{nd} (F (j)))) \in ℝ$
108	104 106 107	syl2anc	$⊢ (φ \land j \in ℕ) \to vol ([1^{st} (F (j)), 2^{nd} (F (j)))) \in ℝ$
109	102 108	eqeltrd	$⊢ (φ \land j \in ℕ) \to vol (([.) \circ I (j)) (A)) \in ℝ$
110	109	recnd	$⊢ (φ \land j \in ℕ) \to vol (([.) \circ I (j)) (A)) \in ℂ$
111		2fveq3	$⊢ k = A \to vol (([.) \circ I (j)) (k)) = vol (([.) \circ I (j)) (A))$
112	111	prodsn	$⊢ (A \in V \land vol (([.) \circ I (j)) (A)) \in ℂ) \to \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)) = vol (([.) \circ I (j)) (A))$
113	90 110 112	syl2anc	$⊢ (φ \land j \in ℕ) \to \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)) = vol (([.) \circ I (j)) (A))$
114	113 102	eqtr2d	$⊢ (φ \land j \in ℕ) \to vol ([1^{st} (F (j)), 2^{nd} (F (j)))) = \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))$
115	114	mpteq2dva	$⊢ φ \to (j \in ℕ ⟼ vol ([1^{st} (F (j)), 2^{nd} (F (j))))) = (j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)))$
116	89 115	eqtrd	$⊢ φ \to (vol \circ [.)) \circ F = (j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k)))$
117	116	fveq2d	$⊢ φ \to sum^((vol \circ [.)) \circ F) = sum^((j \in ℕ ⟼ \prod_{k \in \{A\}} vol (([.) \circ I (j)) (k))))$
118	5 117	eqtr4d	$⊢ φ \to Z = sum^((vol \circ [.)) \circ F)$
119	82 118	jca	$⊢ φ \to (B \subseteq ⋃ ran ([.) \circ F) \land Z = sum^((vol \circ [.)) \circ F))$
120		coeq2	$⊢ f = F \to [.) \circ f = [.) \circ F$
121	120	rneqd	$⊢ f = F \to ran ([.) \circ f) = ran ([.) \circ F)$
122	121	unieqd	$⊢ f = F \to ⋃ ran ([.) \circ f) = ⋃ ran ([.) \circ F)$
123	122	sseq2d	$⊢ f = F \to (B \subseteq ⋃ ran ([.) \circ f) \leftrightarrow B \subseteq ⋃ ran ([.) \circ F))$
124		coeq2	$⊢ f = F \to (vol \circ [.)) \circ f = (vol \circ [.)) \circ F$
125	124	fveq2d	$⊢ f = F \to sum^((vol \circ [.)) \circ f) = sum^((vol \circ [.)) \circ F)$
126	125	eqeq2d	$⊢ f = F \to (Z = sum^((vol \circ [.)) \circ f) \leftrightarrow Z = sum^((vol \circ [.)) \circ F))$
127	123 126	anbi12d	$⊢ f = F \to ((B \subseteq ⋃ ran ([.) \circ f) \land Z = sum^((vol \circ [.)) \circ f)) \leftrightarrow (B \subseteq ⋃ ran ([.) \circ F) \land Z = sum^((vol \circ [.)) \circ F)))$
128	127	rspcev	$⊢ (F \in ({ℝ^{2}}^{ℕ}) \land (B \subseteq ⋃ ran ([.) \circ F) \land Z = sum^((vol \circ [.)) \circ F))) \to \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land Z = sum^((vol \circ [.)) \circ f))$
129	24 119 128	syl2anc	$⊢ φ \to \exists f \in ({ℝ^{2}}^{ℕ}) (B \subseteq ⋃ ran ([.) \circ f) \land Z = sum^((vol \circ [.)) \circ f))$

Metamath Proof Explorer

Theorem ovnovollem2

Proof