Proof of Theorem wlksoneq1eq2
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | 1 | wlkonprop 26554 |
. 2
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) |
3 | 1 | wlkonprop 26554 |
. 2
⊢ (𝐻(𝐶(WalksOn‘𝐺)𝐷)𝑃 → ((𝐺 ∈ V ∧ 𝐶 ∈ (Vtx‘𝐺) ∧ 𝐷 ∈ (Vtx‘𝐺)) ∧ (𝐻 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷))) |
4 | | simp2 1062 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘0) = 𝐴) |
5 | 4 | eqcomd 2628 |
. . . . . . . . 9
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → 𝐴 = (𝑃‘0)) |
6 | | simp2 1062 |
. . . . . . . . 9
⊢ ((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) → (𝑃‘0) = 𝐶) |
7 | 5, 6 | sylan9eqr 2678 |
. . . . . . . 8
⊢ (((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → 𝐴 = 𝐶) |
8 | | simp3 1063 |
. . . . . . . . . . 11
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘(#‘𝐹)) = 𝐵) |
9 | 8 | eqcomd 2628 |
. . . . . . . . . 10
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → 𝐵 = (𝑃‘(#‘𝐹))) |
10 | 9 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → 𝐵 = (𝑃‘(#‘𝐹))) |
11 | | wlklenvm1 26517 |
. . . . . . . . . . . 12
⊢ (𝐻(Walks‘𝐺)𝑃 → (#‘𝐻) = ((#‘𝑃) − 1)) |
12 | | wlklenvm1 26517 |
. . . . . . . . . . . . . . 15
⊢ (𝐹(Walks‘𝐺)𝑃 → (#‘𝐹) = ((#‘𝑃) − 1)) |
13 | | eqtr3 2643 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) =
((#‘𝑃) − 1)
∧ (#‘𝐻) =
((#‘𝑃) − 1))
→ (#‘𝐹) =
(#‘𝐻)) |
14 | 13 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) =
((#‘𝑃) − 1)
∧ (#‘𝐻) =
((#‘𝑃) − 1))
→ (𝑃‘(#‘𝐹)) = (𝑃‘(#‘𝐻))) |
15 | 14 | ex 450 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) =
((#‘𝑃) − 1)
→ ((#‘𝐻) =
((#‘𝑃) − 1)
→ (𝑃‘(#‘𝐹)) = (𝑃‘(#‘𝐻)))) |
16 | 12, 15 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐹(Walks‘𝐺)𝑃 → ((#‘𝐻) = ((#‘𝑃) − 1) → (𝑃‘(#‘𝐹)) = (𝑃‘(#‘𝐻)))) |
17 | 16 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → ((#‘𝐻) = ((#‘𝑃) − 1) → (𝑃‘(#‘𝐹)) = (𝑃‘(#‘𝐻)))) |
18 | 17 | com12 32 |
. . . . . . . . . . . 12
⊢
((#‘𝐻) =
((#‘𝑃) − 1)
→ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘(#‘𝐹)) = (𝑃‘(#‘𝐻)))) |
19 | 11, 18 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐻(Walks‘𝐺)𝑃 → ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘(#‘𝐹)) = (𝑃‘(#‘𝐻)))) |
20 | 19 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) → ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝑃‘(#‘𝐹)) = (𝑃‘(#‘𝐻)))) |
21 | 20 | imp 445 |
. . . . . . . . 9
⊢ (((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝑃‘(#‘𝐹)) = (𝑃‘(#‘𝐻))) |
22 | | simpl3 1066 |
. . . . . . . . 9
⊢ (((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝑃‘(#‘𝐻)) = 𝐷) |
23 | 10, 21, 22 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → 𝐵 = 𝐷) |
24 | 7, 23 | jca 554 |
. . . . . . 7
⊢ (((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
25 | 24 | ex 450 |
. . . . . 6
⊢ ((𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷) → ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
26 | 25 | 3ad2ant3 1084 |
. . . . 5
⊢ (((𝐺 ∈ V ∧ 𝐶 ∈ (Vtx‘𝐺) ∧ 𝐷 ∈ (Vtx‘𝐺)) ∧ (𝐻 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷)) → ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
27 | 26 | com12 32 |
. . . 4
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵) → (((𝐺 ∈ V ∧ 𝐶 ∈ (Vtx‘𝐺) ∧ 𝐷 ∈ (Vtx‘𝐺)) ∧ (𝐻 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
28 | 27 | 3ad2ant3 1084 |
. . 3
⊢ (((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) → (((𝐺 ∈ V ∧ 𝐶 ∈ (Vtx‘𝐺) ∧ 𝐷 ∈ (Vtx‘𝐺)) ∧ (𝐻 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
29 | 28 | imp 445 |
. 2
⊢ ((((𝐺 ∈ V ∧ 𝐴 ∈ (Vtx‘𝐺) ∧ 𝐵 ∈ (Vtx‘𝐺)) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵)) ∧ ((𝐺 ∈ V ∧ 𝐶 ∈ (Vtx‘𝐺) ∧ 𝐷 ∈ (Vtx‘𝐺)) ∧ (𝐻 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐻(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐶 ∧ (𝑃‘(#‘𝐻)) = 𝐷))) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
30 | 2, 3, 29 | syl2an 494 |
1
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐻(𝐶(WalksOn‘𝐺)𝐷)𝑃) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |