Proof of Theorem 1wlkiswwlks2lem4
Step | Hyp | Ref
| Expression |
1 | | 1wlkiswwlks2lem.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
2 | 1 | wlkiswwlk2lem1 26219 |
. . 3
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) |
3 | 2 | 3adant1 1072 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) |
4 | | lencl 13179 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
5 | 4 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝑃) ∈
ℕ0) |
6 | 1 | wlkiswwlk2lem2 26220 |
. . . . . . . . 9
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝑖
∈ (0..^((#‘𝑃)
− 1))) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
7 | 5, 6 | sylan 487 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
9 | 8 | fveq2d 6107 |
. . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝑖)) = (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
10 | | 1wlkiswwlks2lem.e |
. . . . . . . . . . 11
⊢ 𝐸 = (iEdg‘𝐺) |
11 | 10 | uspgrf1oedg 40403 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) |
12 | | edgaval 25794 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
13 | 10 | rneqi 5273 |
. . . . . . . . . . . 12
⊢ ran 𝐸 = ran (iEdg‘𝐺) |
14 | 12, 13 | syl6reqr 2663 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USPGraph → ran
𝐸 = (Edg‘𝐺)) |
15 | 14 | f1oeq3d 6047 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USPGraph → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))) |
16 | 11, 15 | mpbird 246 |
. . . . . . . . 9
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
17 | 16 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
18 | 17 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
19 | | f1ocnvfv2 6433 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
20 | 18, 19 | sylan 487 |
. . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
21 | 9, 20 | eqtrd 2644 |
. . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
22 | 21 | ex 449 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
23 | 22 | ralimdva 2945 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
24 | | oveq2 6557 |
. . . . 5
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ (0..^(#‘𝐹)) =
(0..^((#‘𝑃) −
1))) |
25 | 24 | raleqdv 3121 |
. . . 4
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
26 | 25 | imbi2d 329 |
. . 3
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ ((∀𝑖 ∈
(0..^((#‘𝑃) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
27 | 23, 26 | syl5ibr 235 |
. 2
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ ((𝐺 ∈ USPGraph
∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
28 | 3, 27 | mpcom 37 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |