Proof of Theorem wlkiswwlks2lem4
Step | Hyp | Ref
| Expression |
1 | | wlkiswwlks2lem.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) |
2 | 1 | wlkiswwlks2lem1 26755 |
. . 3
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) |
3 | 2 | 3adant1 1079 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) |
4 | | lencl 13324 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
5 | 4 | 3ad2ant2 1083 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝑃) ∈
ℕ0) |
6 | 1 | wlkiswwlks2lem2 26756 |
. . . . . . . . 9
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝑖
∈ (0..^((#‘𝑃)
− 1))) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
7 | 5, 6 | sylan 488 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
8 | 7 | adantr 481 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐹‘𝑖) = (◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
9 | 8 | fveq2d 6195 |
. . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝑖)) = (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
10 | | wlkiswwlks2lem.e |
. . . . . . . . . . 11
⊢ 𝐸 = (iEdg‘𝐺) |
11 | 10 | uspgrf1oedg 26068 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) |
12 | 10 | rneqi 5352 |
. . . . . . . . . . . 12
⊢ ran 𝐸 = ran (iEdg‘𝐺) |
13 | | edgval 25941 |
. . . . . . . . . . . 12
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
14 | 12, 13 | eqtr4i 2647 |
. . . . . . . . . . 11
⊢ ran 𝐸 = (Edg‘𝐺) |
15 | | f1oeq3 6129 |
. . . . . . . . . . 11
⊢ (ran
𝐸 = (Edg‘𝐺) → (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺))) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝐸:dom 𝐸–1-1-onto→ran
𝐸 ↔ 𝐸:dom 𝐸–1-1-onto→(Edg‘𝐺)) |
17 | 11, 16 | sylibr 224 |
. . . . . . . . 9
⊢ (𝐺 ∈ USPGraph → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
18 | 17 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
19 | 18 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → 𝐸:dom 𝐸–1-1-onto→ran
𝐸) |
20 | | f1ocnvfv2 6533 |
. . . . . . 7
⊢ ((𝐸:dom 𝐸–1-1-onto→ran
𝐸 ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
21 | 19, 20 | sylan 488 |
. . . . . 6
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(◡𝐸‘{(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
22 | 9, 21 | eqtrd 2656 |
. . . . 5
⊢ ((((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) ∧ {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸) → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) |
23 | 22 | ex 450 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) ∧ 𝑖 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
24 | 23 | ralimdva 2962 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
25 | | oveq2 6658 |
. . . . 5
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ (0..^(#‘𝐹)) =
(0..^((#‘𝑃) −
1))) |
26 | 25 | raleqdv 3144 |
. . . 4
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ (∀𝑖 ∈
(0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ↔ ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |
27 | 26 | imbi2d 330 |
. . 3
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ ((∀𝑖 ∈
(0..^((#‘𝑃) −
1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ↔ (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^((#‘𝑃) − 1))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
28 | 24, 27 | syl5ibr 236 |
. 2
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ ((𝐺 ∈ USPGraph
∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) |
29 | 3, 28 | mpcom 38 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) |