Proof of Theorem uspgr2wlkeqi
Step | Hyp | Ref
| Expression |
1 | | 1wlkcpr 40833 |
. . . . 5
⊢ (𝐴 ∈ (1Walks‘𝐺) ↔ (1st
‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴)) |
2 | | 1wlkcpr 40833 |
. . . . . 6
⊢ (𝐵 ∈ (1Walks‘𝐺) ↔ (1st
‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵)) |
3 | | 1wlkcl 40820 |
. . . . . . 7
⊢
((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) → (#‘(1st
‘𝐴)) ∈
ℕ0) |
4 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝐴) = (2nd ‘𝐵) → (#‘(2nd
‘𝐴)) =
(#‘(2nd ‘𝐵))) |
5 | 4 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝐴) = (2nd ‘𝐵) → ((#‘(2nd
‘𝐴)) − 1) =
((#‘(2nd ‘𝐵)) − 1)) |
6 | 5 | eqcomd 2616 |
. . . . . . . . . . 11
⊢
((2nd ‘𝐴) = (2nd ‘𝐵) → ((#‘(2nd
‘𝐵)) − 1) =
((#‘(2nd ‘𝐴)) − 1)) |
7 | 6 | adantl 481 |
. . . . . . . . . 10
⊢
((((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) ∧ (1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) →
((#‘(2nd ‘𝐵)) − 1) = ((#‘(2nd
‘𝐴)) −
1)) |
8 | | 1wlklenvm1 40826 |
. . . . . . . . . . . 12
⊢
((1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵) → (#‘(1st
‘𝐵)) =
((#‘(2nd ‘𝐵)) − 1)) |
9 | | 1wlklenvm1 40826 |
. . . . . . . . . . . 12
⊢
((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) → (#‘(1st
‘𝐴)) =
((#‘(2nd ‘𝐴)) − 1)) |
10 | 8, 9 | eqeqan12rd 2628 |
. . . . . . . . . . 11
⊢
(((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) ∧ (1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵)) → ((#‘(1st
‘𝐵)) =
(#‘(1st ‘𝐴)) ↔ ((#‘(2nd
‘𝐵)) − 1) =
((#‘(2nd ‘𝐴)) − 1))) |
11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢
((((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) ∧ (1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) →
((#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)) ↔
((#‘(2nd ‘𝐵)) − 1) = ((#‘(2nd
‘𝐴)) −
1))) |
12 | 7, 11 | mpbird 246 |
. . . . . . . . 9
⊢
((((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) ∧ (1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) →
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))) |
13 | 12 | anim2i 591 |
. . . . . . . 8
⊢
(((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) ∧ (1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵))) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))) |
14 | 13 | exp44 639 |
. . . . . . 7
⊢
((#‘(1st ‘𝐴)) ∈ ℕ0 →
((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) → ((1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵) → ((2nd ‘𝐴) = (2nd ‘𝐵) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))))))) |
15 | 3, 14 | mpcom 37 |
. . . . . 6
⊢
((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) → ((1st ‘𝐵)(1Walks‘𝐺)(2nd ‘𝐵) → ((2nd ‘𝐴) = (2nd ‘𝐵) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))))) |
16 | 2, 15 | syl5bi 231 |
. . . . 5
⊢
((1st ‘𝐴)(1Walks‘𝐺)(2nd ‘𝐴) → (𝐵 ∈ (1Walks‘𝐺) → ((2nd ‘𝐴) = (2nd ‘𝐵) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))))) |
17 | 1, 16 | sylbi 206 |
. . . 4
⊢ (𝐴 ∈ (1Walks‘𝐺) → (𝐵 ∈ (1Walks‘𝐺) → ((2nd ‘𝐴) = (2nd ‘𝐵) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))))) |
18 | 17 | imp31 447 |
. . 3
⊢ (((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))) |
19 | 18 | 3adant1 1072 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) →
((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))) |
20 | | simpl 472 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) → 𝐺 ∈ USPGraph ) |
21 | | simpl 472 |
. . . . . . 7
⊢
(((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))) →
(#‘(1st ‘𝐴)) ∈
ℕ0) |
22 | 20, 21 | anim12i 588 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) ∧ ((#‘(1st
‘𝐴)) ∈
ℕ0 ∧ (#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))) → (𝐺 ∈ USPGraph ∧
(#‘(1st ‘𝐴)) ∈
ℕ0)) |
23 | | simpl 472 |
. . . . . . . 8
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) → 𝐴 ∈ (1Walks‘𝐺)) |
24 | 23 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) → 𝐴 ∈ (1Walks‘𝐺)) |
25 | | eqidd 2611 |
. . . . . . 7
⊢
(((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))) →
(#‘(1st ‘𝐴)) = (#‘(1st ‘𝐴))) |
26 | 24, 25 | anim12i 588 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) ∧ ((#‘(1st
‘𝐴)) ∈
ℕ0 ∧ (#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))) → (𝐴 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐴)))) |
27 | | simpr 476 |
. . . . . . . 8
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) → 𝐵 ∈ (1Walks‘𝐺)) |
28 | 27 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) → 𝐵 ∈ (1Walks‘𝐺)) |
29 | | simpr 476 |
. . . . . . 7
⊢
(((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))) →
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))) |
30 | 28, 29 | anim12i 588 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) ∧ ((#‘(1st
‘𝐴)) ∈
ℕ0 ∧ (#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))) → (𝐵 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝐵)) =
(#‘(1st ‘𝐴)))) |
31 | | uspgr2wlkeq2 40855 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧
(#‘(1st ‘𝐴)) ∈ ℕ0) ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝐴)) =
(#‘(1st ‘𝐴))) ∧ (𝐵 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝐵)) =
(#‘(1st ‘𝐴)))) → ((2nd ‘𝐴) = (2nd ‘𝐵) → 𝐴 = 𝐵)) |
32 | 22, 26, 30, 31 | syl3anc 1318 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) ∧ ((#‘(1st
‘𝐴)) ∈
ℕ0 ∧ (#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴)))) → ((2nd
‘𝐴) = (2nd
‘𝐵) → 𝐴 = 𝐵)) |
33 | 32 | ex 449 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) → (((#‘(1st
‘𝐴)) ∈
ℕ0 ∧ (#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))) → ((2nd
‘𝐴) = (2nd
‘𝐵) → 𝐴 = 𝐵))) |
34 | 33 | com23 84 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺))) → ((2nd ‘𝐴) = (2nd ‘𝐵) →
(((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))) → 𝐴 = 𝐵))) |
35 | 34 | 3impia 1253 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) →
(((#‘(1st ‘𝐴)) ∈ ℕ0 ∧
(#‘(1st ‘𝐵)) = (#‘(1st ‘𝐴))) → 𝐴 = 𝐵)) |
36 | 19, 35 | mpd 15 |
1
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) → 𝐴 = 𝐵) |