Proof of Theorem cyclispthon
Step | Hyp | Ref
| Expression |
1 | | cycliswlk 26160 |
. . . . 5
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
2 | | wlkonwlk 26065 |
. . . . 5
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → 𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘(#‘𝐹)))𝑃) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘(#‘𝐹)))𝑃) |
4 | | wlkbprop 26051 |
. . . . . . . 8
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
6 | | iscycl 26153 |
. . . . . . . . 9
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
7 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑃‘0) = (𝑃‘(#‘𝐹))) |
8 | 6, 7 | syl6bi 242 |
. . . . . . . 8
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
9 | 8 | 3adant1 1072 |
. . . . . . 7
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
10 | 5, 9 | mpcom 37 |
. . . . . 6
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑃‘0) = (𝑃‘(#‘𝐹))) |
11 | 10 | oveq2d 6565 |
. . . . 5
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → ((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘0)) = ((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘(#‘𝐹)))) |
12 | 11 | breqd 4594 |
. . . 4
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘0))𝑃 ↔ 𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘(#‘𝐹)))𝑃)) |
13 | 3, 12 | mpbird 246 |
. . 3
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘0))𝑃) |
14 | | cyclispth 26157 |
. . 3
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Paths 𝐸)𝑃) |
15 | 13, 14 | jca 553 |
. 2
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘0))𝑃 ∧ 𝐹(𝑉 Paths 𝐸)𝑃)) |
16 | | simpl2 1058 |
. . . . 5
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝐹(𝑉 Walks 𝐸)𝑃) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
17 | | simpl3 1059 |
. . . . 5
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝐹(𝑉 Walks 𝐸)𝑃) → (𝐹 ∈ V ∧ 𝑃 ∈ V)) |
18 | | 2mwlk 26049 |
. . . . . . . . 9
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
19 | | 0elfz 12305 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) ∈
ℕ0 → 0 ∈ (0...(#‘𝐹))) |
20 | 19 | anim2i 591 |
. . . . . . . . . . . 12
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (#‘𝐹) ∈ ℕ0) → (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 0 ∈ (0...(#‘𝐹)))) |
21 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 0 ∈ (0...(#‘𝐹))) → (𝑃‘0) ∈ 𝑉) |
22 | | id 22 |
. . . . . . . . . . . . 13
⊢ ((𝑃‘0) ∈ 𝑉 → (𝑃‘0) ∈ 𝑉) |
23 | 22, 22 | jca 553 |
. . . . . . . . . . . 12
⊢ ((𝑃‘0) ∈ 𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉)) |
24 | 20, 21, 23 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝑃:(0...(#‘𝐹))⟶𝑉 ∧ (#‘𝐹) ∈ ℕ0) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉)) |
25 | 24 | ex 449 |
. . . . . . . . . 10
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝐹) ∈ ℕ0 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉))) |
26 | 25 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((#‘𝐹) ∈ ℕ0 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉))) |
27 | 18, 26 | syl 17 |
. . . . . . . 8
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉))) |
28 | 27 | com12 32 |
. . . . . . 7
⊢
((#‘𝐹) ∈
ℕ0 → (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉))) |
29 | 28 | 3ad2ant1 1075 |
. . . . . 6
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉))) |
30 | 29 | imp 444 |
. . . . 5
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝐹(𝑉 Walks 𝐸)𝑃) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉)) |
31 | 16, 17, 30 | 3jca 1235 |
. . . 4
⊢
((((#‘𝐹)
∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ 𝐹(𝑉 Walks 𝐸)𝑃) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉))) |
32 | 4, 31 | mpancom 700 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉))) |
33 | | ispthon 26106 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘0) ∈ 𝑉)) → (𝐹((𝑃‘0)(𝑉 PathOn 𝐸)(𝑃‘0))𝑃 ↔ (𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘0))𝑃 ∧ 𝐹(𝑉 Paths 𝐸)𝑃))) |
34 | 1, 32, 33 | 3syl 18 |
. 2
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝐹((𝑃‘0)(𝑉 PathOn 𝐸)(𝑃‘0))𝑃 ↔ (𝐹((𝑃‘0)(𝑉 WalkOn 𝐸)(𝑃‘0))𝑃 ∧ 𝐹(𝑉 Paths 𝐸)𝑃))) |
35 | 15, 34 | mpbird 246 |
1
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹((𝑃‘0)(𝑉 PathOn 𝐸)(𝑃‘0))𝑃) |