ovollb

Description: The outer volume is a lower bound on the sum of all interval coverings of A . (Contributed by Mario Carneiro, 15-Jun-2014)

		Ref	Expression
	Hypothesis	ovollb.1	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
	Assertion	ovollb	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovollb.1	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
2		simpr	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) )
3		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
4		simpl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
5		inss2	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
6		rexpssxrxp	⊢ ( ℝ × ℝ ) ⊆ ( ℝ^* × ℝ^* )
7	5 6	sstri	⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* )
8		fss	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ^* × ℝ^* ) ) → 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
9	4 7 8	sylancl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) )
10		fco	⊢ ( ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ ∧ 𝐹 : ℕ ⟶ ( ℝ^* × ℝ^* ) ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
11	3 9 10	sylancr	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ( (,) ∘ 𝐹 ) : ℕ ⟶ 𝒫 ℝ )
12	11	frnd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ran ( (,) ∘ 𝐹 ) ⊆ 𝒫 ℝ )
13		sspwuni	⊢ ( ran ( (,) ∘ 𝐹 ) ⊆ 𝒫 ℝ ↔ ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
14	12 13	sylib	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ∪ ran ( (,) ∘ 𝐹 ) ⊆ ℝ )
15	2 14	sstrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → 𝐴 ⊆ ℝ )
16		eqid	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } = { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) }
17	16	ovolval	⊢ ( 𝐴 ⊆ ℝ → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) )
18	15 17	syl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ( vol* ‘ 𝐴 ) = inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) )
19		ssrab2	⊢ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } ⊆ ℝ^*
20	16 1	elovolmr	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → sup ( ran 𝑆 , ℝ^* , < ) ∈ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } )
21		infxrlb	⊢ ( ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } ⊆ ℝ^* ∧ sup ( ran 𝑆 , ℝ^* , < ) ∈ { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } ) → inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
22	19 20 21	sylancr	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → inf ( { 𝑦 ∈ ℝ^* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑_m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ^* , < ) ) } , ℝ^* , < ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
23	18 22	eqbrtrd	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ( vol* ‘ 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem ovollb

Proof