Step |
Hyp |
Ref |
Expression |
1 |
|
lfgrn1cycl.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
lfgrn1cycl.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
3 |
|
cyclprop |
⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
4 |
|
cycliswlk |
⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) |
5 |
2 1
|
lfgrwlknloop |
⊢ ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ) |
6 |
|
1nn |
⊢ 1 ∈ ℕ |
7 |
|
eleq1 |
⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ ↔ 1 ∈ ℕ ) ) |
8 |
6 7
|
mpbiri |
⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ♯ ‘ 𝐹 ) ∈ ℕ ) |
9 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ♯ ‘ 𝐹 ) ∈ ℕ ) |
10 |
8 9
|
sylibr |
⊢ ( ( ♯ ‘ 𝐹 ) = 1 → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) |
11 |
|
fveq2 |
⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) ) |
12 |
|
fv0p1e1 |
⊢ ( 𝑘 = 0 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 1 ) ) |
13 |
11 12
|
neeq12d |
⊢ ( 𝑘 = 0 → ( ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) |
14 |
13
|
rspcv |
⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) |
15 |
10 14
|
syl |
⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) |
16 |
15
|
impcom |
⊢ ( ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) |
17 |
|
fveq2 |
⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 1 ) ) |
18 |
17
|
neeq2d |
⊢ ( ( ♯ ‘ 𝐹 ) = 1 → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) |
19 |
18
|
adantl |
⊢ ( ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) |
20 |
16 19
|
mpbird |
⊢ ( ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∧ ( ♯ ‘ 𝐹 ) = 1 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
21 |
20
|
ex |
⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( ♯ ‘ 𝐹 ) = 1 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
22 |
21
|
necon2d |
⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ≠ ( 𝑃 ‘ ( 𝑘 + 1 ) ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) |
23 |
5 22
|
syl |
⊢ ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ∧ 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ) → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) |
24 |
23
|
ex |
⊢ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) ) |
25 |
24
|
com13 |
⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) ) |
26 |
25
|
adantl |
⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) ) |
27 |
3 4 26
|
sylc |
⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) |
28 |
27
|
com12 |
⊢ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≠ 1 ) ) |