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

Metamath Proof Explorer

Theorem isewlk

Description: Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion isewlk ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ewlksfval.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 1 ewlksfval ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )
3 2 3adant3 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐺 EdgWalks 𝑆 ) = { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } )
4 3 eleq2d ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ) )
5 eleq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ∈ Word dom 𝐼 ↔ 𝐹 ∈ Word dom 𝐼 ) )
6 fveq2 ⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
7 6 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 1 ..^ ( ♯ ‘ 𝑓 ) ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
8 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑘 − 1 ) ) = ( 𝐹 ‘ ( 𝑘 − 1 ) ) )
9 8 fveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) )
10 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
11 10 fveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
12 9 11 ineq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) = ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
13 12 fveq2d ⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) = ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) )
14 13 breq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
15 7 14 raleqbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) )
16 5 15 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
17 16 elabg ⊢ ( 𝐹 ∈ 𝑈 → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
18 17 3ad2ant3 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝑓 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝑓 ‘ 𝑘 ) ) ) ) ) } ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )
19 4 18 bitrd ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈 ) → ( 𝐹 ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) 𝑆 ≤ ( ♯ ‘ ( ( 𝐼 ‘ ( 𝐹 ‘ ( 𝑘 − 1 ) ) ) ∩ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ) ) ) )