Step |
Hyp |
Ref |
Expression |
1 |
|
umgr2adedgwlk.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
2 |
|
umgr2adedgwlk.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
3 |
|
umgr2adedgwlk.f |
⊢ 𝐹 = 〈“ 𝐽 𝐾 ”〉 |
4 |
|
umgr2adedgwlk.p |
⊢ 𝑃 = 〈“ 𝐴 𝐵 𝐶 ”〉 |
5 |
|
umgr2adedgwlk.g |
⊢ ( 𝜑 → 𝐺 ∈ UMGraph ) |
6 |
|
umgr2adedgwlk.a |
⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) |
7 |
|
umgr2adedgwlk.j |
⊢ ( 𝜑 → ( 𝐼 ‘ 𝐽 ) = { 𝐴 , 𝐵 } ) |
8 |
|
umgr2adedgwlk.k |
⊢ ( 𝜑 → ( 𝐼 ‘ 𝐾 ) = { 𝐵 , 𝐶 } ) |
9 |
1 2 3 4 5 6 7 8
|
umgr2adedgwlk |
⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) ) |
10 |
|
simp1 |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) |
11 |
|
id |
⊢ ( ( 𝑃 ‘ 0 ) = 𝐴 → ( 𝑃 ‘ 0 ) = 𝐴 ) |
12 |
11
|
eqcoms |
⊢ ( 𝐴 = ( 𝑃 ‘ 0 ) → ( 𝑃 ‘ 0 ) = 𝐴 ) |
13 |
12
|
3ad2ant1 |
⊢ ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ 0 ) = 𝐴 ) |
14 |
13
|
3ad2ant3 |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) → ( 𝑃 ‘ 0 ) = 𝐴 ) |
15 |
|
fveq2 |
⊢ ( 2 = ( ♯ ‘ 𝐹 ) → ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
16 |
15
|
eqcoms |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 2 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
17 |
16
|
eqeq1d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝑃 ‘ 2 ) = 𝐶 ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) |
18 |
17
|
biimpcd |
⊢ ( ( 𝑃 ‘ 2 ) = 𝐶 → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) |
19 |
18
|
eqcoms |
⊢ ( 𝐶 = ( 𝑃 ‘ 2 ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) |
20 |
19
|
3ad2ant3 |
⊢ ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) |
21 |
20
|
com12 |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) |
22 |
21
|
a1i |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) ) |
23 |
22
|
3imp |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) |
24 |
10 14 23
|
3jca |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 2 ∧ ( 𝐴 = ( 𝑃 ‘ 0 ) ∧ 𝐵 = ( 𝑃 ‘ 1 ) ∧ 𝐶 = ( 𝑃 ‘ 2 ) ) ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) |
25 |
9 24
|
syl |
⊢ ( 𝜑 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) |
26 |
|
3anass |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ↔ ( 𝐺 ∈ UMGraph ∧ ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) ) |
27 |
5 6 26
|
sylanbrc |
⊢ ( 𝜑 → ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ) |
28 |
1
|
umgr2adedgwlklem |
⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
29 |
|
3simpb |
⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
30 |
29
|
adantl |
⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
31 |
27 28 30
|
3syl |
⊢ ( 𝜑 → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
32 |
|
3anass |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ↔ ( 𝐺 ∈ UMGraph ∧ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) ) |
33 |
5 31 32
|
sylanbrc |
⊢ ( 𝜑 → ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
34 |
|
s2cli |
⊢ 〈“ 𝐽 𝐾 ”〉 ∈ Word V |
35 |
3 34
|
eqeltri |
⊢ 𝐹 ∈ Word V |
36 |
|
s3cli |
⊢ 〈“ 𝐴 𝐵 𝐶 ”〉 ∈ Word V |
37 |
4 36
|
eqeltri |
⊢ 𝑃 ∈ Word V |
38 |
35 37
|
pm3.2i |
⊢ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) |
39 |
|
id |
⊢ ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
40 |
39
|
3adant1 |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ) |
41 |
40
|
anim1i |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) → ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) ) |
42 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
43 |
42
|
iswlkon |
⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) ) |
44 |
41 43
|
syl |
⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐶 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ Word V ∧ 𝑃 ∈ Word V ) ) → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) ) |
45 |
33 38 44
|
sylancl |
⊢ ( 𝜑 → ( 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = 𝐶 ) ) ) |
46 |
25 45
|
mpbird |
⊢ ( 𝜑 → 𝐹 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐶 ) 𝑃 ) |