This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovolshftlem2

Description: Lemma for ovolshft . (Contributed by Mario Carneiro, 22-Mar-2014)

Ref Expression
Hypotheses ovolshft.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
ovolshft.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
ovolshft.3 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
ovolshft.4 ⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
Assertion ovolshftlem2 ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ 𝑀 )

Proof

Step Hyp Ref Expression
1 ovolshft.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 ovolshft.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3 ovolshft.3 ⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
4 ovolshft.4 ⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
5 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝐴 ⊆ ℝ )
6 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝐶 ∈ ℝ )
7 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
8 eqid ⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) )
9 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 1st ‘ ( 𝑔 ‘ 𝑚 ) ) = ( 1st ‘ ( 𝑔 ‘ 𝑛 ) ) )
10 9 oveq1d ⊢ ( 𝑚 = 𝑛 → ( ( 1st ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) = ( ( 1st ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) )
11 2fveq3 ⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) )
12 11 oveq1d ⊢ ( 𝑚 = 𝑛 → ( ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) = ( ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) )
13 10 12 opeq12d ⊢ ( 𝑚 = 𝑛 → ⟨ ( ( 1st ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) ⟩ = ⟨ ( ( 1st ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) ⟩ )
14 13 cbvmptv ⊢ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) ⟩ )
15 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
16 elovolmlem ⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝑔 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
17 15 16 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝑔 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
18 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) )
19 5 6 7 4 8 14 17 18 ovolshftlem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ∈ 𝑀 )
20 eleq1a ⊢ ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ∈ 𝑀 → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) → 𝑧 ∈ 𝑀 ) )
21 19 20 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) → 𝑧 ∈ 𝑀 ) )
22 21 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) → 𝑧 ∈ 𝑀 ) )
23 22 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) → ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) → 𝑧 ∈ 𝑀 ) )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ* ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) → 𝑧 ∈ 𝑀 ) )
25 rabss ⊢ ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ 𝑀 ↔ ∀ 𝑧 ∈ ℝ* ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) → 𝑧 ∈ 𝑀 ) )
26 24 25 sylibr ⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ 𝑀 )