Step |
Hyp |
Ref |
Expression |
1 |
|
wlkson.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
1
|
wlkson |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) = { 〈 𝑓 , 𝑝 〉 ∣ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑝 ∧ ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) } ) |
3 |
|
fveq1 |
⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 0 ) = ( 𝑃 ‘ 0 ) ) |
4 |
3
|
adantl |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ‘ 0 ) = ( 𝑃 ‘ 0 ) ) |
5 |
4
|
eqeq1d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑝 ‘ 0 ) = 𝐴 ↔ ( 𝑃 ‘ 0 ) = 𝐴 ) ) |
6 |
|
simpr |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 ) |
7 |
|
fveq2 |
⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) ) |
8 |
7
|
adantr |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) ) |
9 |
6 8
|
fveq12d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
10 |
9
|
eqeq1d |
⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑝 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) |
11 |
2 5 10
|
2rbropap |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ) |
12 |
11
|
3expb |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍 ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐵 ) ) ) |