Proof of Theorem wlkiswwlk2lem4
Step | Hyp | Ref
| Expression |
1 | | wlkiswwlk2lem.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
2 | 1 | wlkiswwlk2lem1 26219 |
. . 3
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) |
3 | 2 | 3adant1 1072 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) |
4 | | lencl 13179 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
5 | 4 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝑃) ∈
ℕ0) |
6 | 1 | wlkiswwlk2lem2 26220 |
. . . . . . . . 9
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝑖
∈ (0..^((#‘𝑃)
− 1))) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
7 | 5, 6 | sylan 487 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
9 | 8 | fveq2d 6107 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝑖)) = (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
10 | | usgraf1o 25887 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
11 | 10 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
13 | | f1ocnvfv2 6433 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
14 | 12, 13 | sylan 487 |
. . . . . 6
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
15 | 9, 14 | eqtrd 2644 |
. . . . 5
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
16 | 15 | ex 449 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
17 | 16 | ralimdva 2945 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
18 | | oveq2 6557 |
. . . . 5
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ (0..^(#‘𝐹)) =
(0..^((#‘𝑃) −
1))) |
19 | 18 | raleqdv 3121 |
. . . 4
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
20 | 19 | imbi2d 329 |
. . 3
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ ((∀𝑖 ∈
(0..^((#‘𝑃) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
21 | 17, 20 | syl5ibr 235 |
. 2
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
22 | 3, 21 | mpcom 37 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |