Step |
Hyp |
Ref |
Expression |
1 |
|
3wlkd.p |
⊢ 𝑃 = 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 |
2 |
|
3wlkd.f |
⊢ 𝐹 = 〈“ 𝐽 𝐾 𝐿 ”〉 |
3 |
|
3wlkd.s |
⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) ) |
4 |
|
3wlkd.n |
⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) ) |
5 |
|
3wlkd.e |
⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ∧ { 𝐶 , 𝐷 } ⊆ ( 𝐼 ‘ 𝐿 ) ) ) |
6 |
|
3wlkd.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
7 |
|
3wlkd.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
8 |
|
3trld.n |
⊢ ( 𝜑 → ( 𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿 ) ) |
9 |
1 2 3 4 5 6 7 8
|
3trlond |
⊢ ( 𝜑 → 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) |
10 |
1 2 3 4 5 6 7 8
|
3pthd |
⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) |
11 |
3
|
simplld |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
12 |
3
|
simprrd |
⊢ ( 𝜑 → 𝐷 ∈ 𝑉 ) |
13 |
|
s3cli |
⊢ 〈“ 𝐽 𝐾 𝐿 ”〉 ∈ Word V |
14 |
2 13
|
eqeltri |
⊢ 𝐹 ∈ Word V |
15 |
|
s4cli |
⊢ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 ∈ Word V |
16 |
1 15
|
eqeltri |
⊢ 𝑃 ∈ Word V |
17 |
14 16
|
pm3.2i |
⊢ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) |
18 |
17
|
a1i |
⊢ ( 𝜑 → ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) |
19 |
6
|
ispthson |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
20 |
11 12 18 19
|
syl21anc |
⊢ ( 𝜑 → ( 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ↔ ( 𝐹 ( 𝐴 ( TrailsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ∧ 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ) ) ) |
21 |
9 10 20
|
mpbir2and |
⊢ ( 𝜑 → 𝐹 ( 𝐴 ( PathsOn ‘ 𝐺 ) 𝐷 ) 𝑃 ) |