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

Metamath Proof Explorer

Theorem swrd00

Description: A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion swrd00 ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅

Proof

Step Hyp Ref Expression
1 opelxp ⊢ ( ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ ( V × ( ℤ × ℤ ) ) ↔ ( 𝑆 ∈ V ∧ ⟨ 𝑋 , 𝑋 ⟩ ∈ ( ℤ × ℤ ) ) )
2 opelxp ⊢ ( ⟨ 𝑋 , 𝑋 ⟩ ∈ ( ℤ × ℤ ) ↔ ( 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) )
3 swrdval ⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = if ( ( 𝑋 ..^ 𝑋 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) , ∅ ) )
4 fzo0 ⊢ ( 𝑋 ..^ 𝑋 ) = ∅
5 0ss ⊢ ∅ ⊆ dom 𝑆
6 4 5 eqsstri ⊢ ( 𝑋 ..^ 𝑋 ) ⊆ dom 𝑆
7 6 iftruei ⊢ if ( ( 𝑋 ..^ 𝑋 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) , ∅ ) = ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) )
8 zcn ⊢ ( 𝑋 ∈ ℤ → 𝑋 ∈ ℂ )
9 8 subidd ⊢ ( 𝑋 ∈ ℤ → ( 𝑋 − 𝑋 ) = 0 )
10 9 oveq2d ⊢ ( 𝑋 ∈ ℤ → ( 0 ..^ ( 𝑋 − 𝑋 ) ) = ( 0 ..^ 0 ) )
11 10 3ad2ant2 ⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 0 ..^ ( 𝑋 − 𝑋 ) ) = ( 0 ..^ 0 ) )
12 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
13 11 12 eqtrdi ⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 0 ..^ ( 𝑋 − 𝑋 ) ) = ∅ )
14 13 mpteq1d ⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) = ( 𝑥 ∈ ∅ ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) )
15 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) = ∅
16 14 15 eqtrdi ⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) = ∅ )
17 7 16 eqtrid ⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → if ( ( 𝑋 ..^ 𝑋 ) ⊆ dom 𝑆 , ( 𝑥 ∈ ( 0 ..^ ( 𝑋 − 𝑋 ) ) ↦ ( 𝑆 ‘ ( 𝑥 + 𝑋 ) ) ) , ∅ ) = ∅ )
18 3 17 eqtrd ⊢ ( ( 𝑆 ∈ V ∧ 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
19 18 3expb ⊢ ( ( 𝑆 ∈ V ∧ ( 𝑋 ∈ ℤ ∧ 𝑋 ∈ ℤ ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
20 2 19 sylan2b ⊢ ( ( 𝑆 ∈ V ∧ ⟨ 𝑋 , 𝑋 ⟩ ∈ ( ℤ × ℤ ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
21 1 20 sylbi ⊢ ( ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ ( V × ( ℤ × ℤ ) ) → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
22 df-substr ⊢ substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) )
23 ovex ⊢ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ∈ V
24 23 mptex ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) ∈ V
25 0ex ⊢ ∅ ∈ V
26 24 25 ifex ⊢ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) ∈ V
27 22 26 dmmpo ⊢ dom substr = ( V × ( ℤ × ℤ ) )
28 21 27 eleq2s ⊢ ( ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ dom substr → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
29 df-ov ⊢ ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ( substr ‘ ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ )
30 ndmfv ⊢ ( ¬ ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ dom substr → ( substr ‘ ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ) = ∅ )
31 29 30 eqtrid ⊢ ( ¬ ⟨ 𝑆 , ⟨ 𝑋 , 𝑋 ⟩ ⟩ ∈ dom substr → ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅ )
32 28 31 pm2.61i ⊢ ( 𝑆 substr ⟨ 𝑋 , 𝑋 ⟩ ) = ∅