Step | Hyp | Ref
| Expression |
1 | | wlkcpr 29154 |
. . . . 5
β’ (π΄ β (WalksβπΊ) β (1st
βπ΄)(WalksβπΊ)(2nd βπ΄)) |
2 | | wlkcpr 29154 |
. . . . . 6
β’ (π΅ β (WalksβπΊ) β (1st
βπ΅)(WalksβπΊ)(2nd βπ΅)) |
3 | | wlkcl 29140 |
. . . . . . 7
β’
((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β (β―β(1st
βπ΄)) β
β0) |
4 | | fveq2 6891 |
. . . . . . . . . . . . 13
β’
((2nd βπ΄) = (2nd βπ΅) β (β―β(2nd
βπ΄)) =
(β―β(2nd βπ΅))) |
5 | 4 | oveq1d 7427 |
. . . . . . . . . . . 12
β’
((2nd βπ΄) = (2nd βπ΅) β ((β―β(2nd
βπ΄)) β 1) =
((β―β(2nd βπ΅)) β 1)) |
6 | 5 | eqcomd 2737 |
. . . . . . . . . . 11
β’
((2nd βπ΄) = (2nd βπ΅) β ((β―β(2nd
βπ΅)) β 1) =
((β―β(2nd βπ΄)) β 1)) |
7 | 6 | adantl 481 |
. . . . . . . . . 10
β’
((((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β§ (1st βπ΅)(WalksβπΊ)(2nd βπ΅)) β§ (2nd βπ΄) = (2nd βπ΅)) β
((β―β(2nd βπ΅)) β 1) =
((β―β(2nd βπ΄)) β 1)) |
8 | | wlklenvm1 29147 |
. . . . . . . . . . . 12
β’
((1st βπ΅)(WalksβπΊ)(2nd βπ΅) β (β―β(1st
βπ΅)) =
((β―β(2nd βπ΅)) β 1)) |
9 | | wlklenvm1 29147 |
. . . . . . . . . . . 12
β’
((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β (β―β(1st
βπ΄)) =
((β―β(2nd βπ΄)) β 1)) |
10 | 8, 9 | eqeqan12rd 2746 |
. . . . . . . . . . 11
β’
(((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β§ (1st βπ΅)(WalksβπΊ)(2nd βπ΅)) β ((β―β(1st
βπ΅)) =
(β―β(1st βπ΄)) β ((β―β(2nd
βπ΅)) β 1) =
((β―β(2nd βπ΄)) β 1))) |
11 | 10 | adantr 480 |
. . . . . . . . . 10
β’
((((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β§ (1st βπ΅)(WalksβπΊ)(2nd βπ΅)) β§ (2nd βπ΄) = (2nd βπ΅)) β
((β―β(1st βπ΅)) = (β―β(1st
βπ΄)) β
((β―β(2nd βπ΅)) β 1) =
((β―β(2nd βπ΄)) β 1))) |
12 | 7, 11 | mpbird 257 |
. . . . . . . . 9
β’
((((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β§ (1st βπ΅)(WalksβπΊ)(2nd βπ΅)) β§ (2nd βπ΄) = (2nd βπ΅)) β
(β―β(1st βπ΅)) = (β―β(1st
βπ΄))) |
13 | 12 | anim2i 616 |
. . . . . . . 8
β’
(((β―β(1st βπ΄)) β β0 β§
(((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β§ (1st βπ΅)(WalksβπΊ)(2nd βπ΅)) β§ (2nd βπ΄) = (2nd βπ΅))) β
((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄)))) |
14 | 13 | exp44 437 |
. . . . . . 7
β’
((β―β(1st βπ΄)) β β0 β
((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β ((1st βπ΅)(WalksβπΊ)(2nd βπ΅) β ((2nd βπ΄) = (2nd βπ΅) β
((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄))))))) |
15 | 3, 14 | mpcom 38 |
. . . . . 6
β’
((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β ((1st βπ΅)(WalksβπΊ)(2nd βπ΅) β ((2nd βπ΄) = (2nd βπ΅) β
((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄)))))) |
16 | 2, 15 | biimtrid 241 |
. . . . 5
β’
((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β (π΅ β (WalksβπΊ) β ((2nd βπ΄) = (2nd βπ΅) β
((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄)))))) |
17 | 1, 16 | sylbi 216 |
. . . 4
β’ (π΄ β (WalksβπΊ) β (π΅ β (WalksβπΊ) β ((2nd βπ΄) = (2nd βπ΅) β
((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄)))))) |
18 | 17 | imp31 417 |
. . 3
β’ (((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β§ (2nd βπ΄) = (2nd βπ΅)) β
((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄)))) |
19 | 18 | 3adant1 1129 |
. 2
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β§ (2nd βπ΄) = (2nd βπ΅)) β
((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄)))) |
20 | | simpl 482 |
. . . . . . 7
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β πΊ β USPGraph) |
21 | | simpl 482 |
. . . . . . 7
β’
(((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄))) β
(β―β(1st βπ΄)) β
β0) |
22 | 20, 21 | anim12i 612 |
. . . . . 6
β’ (((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β§ ((β―β(1st
βπ΄)) β
β0 β§ (β―β(1st βπ΅)) =
(β―β(1st βπ΄)))) β (πΊ β USPGraph β§
(β―β(1st βπ΄)) β
β0)) |
23 | | simpl 482 |
. . . . . . . 8
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β π΄ β (WalksβπΊ)) |
24 | 23 | adantl 481 |
. . . . . . 7
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β π΄ β (WalksβπΊ)) |
25 | | eqidd 2732 |
. . . . . . 7
β’
(((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄))) β
(β―β(1st βπ΄)) = (β―β(1st
βπ΄))) |
26 | 24, 25 | anim12i 612 |
. . . . . 6
β’ (((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β§ ((β―β(1st
βπ΄)) β
β0 β§ (β―β(1st βπ΅)) =
(β―β(1st βπ΄)))) β (π΄ β (WalksβπΊ) β§ (β―β(1st
βπ΄)) =
(β―β(1st βπ΄)))) |
27 | | simpr 484 |
. . . . . . . 8
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β π΅ β (WalksβπΊ)) |
28 | 27 | adantl 481 |
. . . . . . 7
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β π΅ β (WalksβπΊ)) |
29 | | simpr 484 |
. . . . . . 7
β’
(((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄))) β
(β―β(1st βπ΅)) = (β―β(1st
βπ΄))) |
30 | 28, 29 | anim12i 612 |
. . . . . 6
β’ (((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β§ ((β―β(1st
βπ΄)) β
β0 β§ (β―β(1st βπ΅)) =
(β―β(1st βπ΄)))) β (π΅ β (WalksβπΊ) β§ (β―β(1st
βπ΅)) =
(β―β(1st βπ΄)))) |
31 | | uspgr2wlkeq2 29172 |
. . . . . 6
β’ (((πΊ β USPGraph β§
(β―β(1st βπ΄)) β β0) β§ (π΄ β (WalksβπΊ) β§
(β―β(1st βπ΄)) = (β―β(1st
βπ΄))) β§ (π΅ β (WalksβπΊ) β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄)))) β
((2nd βπ΄)
= (2nd βπ΅)
β π΄ = π΅)) |
32 | 22, 26, 30, 31 | syl3anc 1370 |
. . . . 5
β’ (((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β§ ((β―β(1st
βπ΄)) β
β0 β§ (β―β(1st βπ΅)) =
(β―β(1st βπ΄)))) β ((2nd βπ΄) = (2nd βπ΅) β π΄ = π΅)) |
33 | 32 | ex 412 |
. . . 4
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β (((β―β(1st
βπ΄)) β
β0 β§ (β―β(1st βπ΅)) =
(β―β(1st βπ΄))) β ((2nd βπ΄) = (2nd βπ΅) β π΄ = π΅))) |
34 | 33 | com23 86 |
. . 3
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ))) β ((2nd βπ΄) = (2nd βπ΅) β
(((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄))) β π΄ = π΅))) |
35 | 34 | 3impia 1116 |
. 2
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β§ (2nd βπ΄) = (2nd βπ΅)) β
(((β―β(1st βπ΄)) β β0 β§
(β―β(1st βπ΅)) = (β―β(1st
βπ΄))) β π΄ = π΅)) |
36 | 19, 35 | mpd 15 |
1
β’ ((πΊ β USPGraph β§ (π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β§ (2nd βπ΄) = (2nd βπ΅)) β π΄ = π΅) |