Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . . . . . 7
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | | eqid 2731 |
. . . . . . 7
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
3 | | eqid 2731 |
. . . . . . 7
β’
(1st βπ΄) = (1st βπ΄) |
4 | | eqid 2731 |
. . . . . . 7
β’
(2nd βπ΄) = (2nd βπ΄) |
5 | 1, 2, 3, 4 | wlkelwrd 28678 |
. . . . . 6
β’ (π΄ β (WalksβπΊ) β ((1st
βπ΄) β Word dom
(iEdgβπΊ) β§
(2nd βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ))) |
6 | | eqid 2731 |
. . . . . . 7
β’
(1st βπ΅) = (1st βπ΅) |
7 | | eqid 2731 |
. . . . . . 7
β’
(2nd βπ΅) = (2nd βπ΅) |
8 | 1, 2, 6, 7 | wlkelwrd 28678 |
. . . . . 6
β’ (π΅ β (WalksβπΊ) β ((1st
βπ΅) β Word dom
(iEdgβπΊ) β§
(2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ))) |
9 | 5, 8 | anim12i 613 |
. . . . 5
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β (((1st βπ΄) β Word dom
(iEdgβπΊ) β§
(2nd βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) β§ ((1st βπ΅) β Word dom
(iEdgβπΊ) β§
(2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ)))) |
10 | | wlkop 28673 |
. . . . . . 7
β’ (π΄ β (WalksβπΊ) β π΄ = β¨(1st βπ΄), (2nd βπ΄)β©) |
11 | | eleq1 2820 |
. . . . . . . 8
β’ (π΄ = β¨(1st
βπ΄), (2nd
βπ΄)β© β
(π΄ β
(WalksβπΊ) β
β¨(1st βπ΄), (2nd βπ΄)β© β (WalksβπΊ))) |
12 | | df-br 5126 |
. . . . . . . . 9
β’
((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β β¨(1st βπ΄), (2nd βπ΄)β© β
(WalksβπΊ)) |
13 | | wlklenvm1 28667 |
. . . . . . . . 9
β’
((1st βπ΄)(WalksβπΊ)(2nd βπ΄) β (β―β(1st
βπ΄)) =
((β―β(2nd βπ΄)) β 1)) |
14 | 12, 13 | sylbir 234 |
. . . . . . . 8
β’
(β¨(1st βπ΄), (2nd βπ΄)β© β (WalksβπΊ) β
(β―β(1st βπ΄)) = ((β―β(2nd
βπ΄)) β
1)) |
15 | 11, 14 | syl6bi 252 |
. . . . . . 7
β’ (π΄ = β¨(1st
βπ΄), (2nd
βπ΄)β© β
(π΄ β
(WalksβπΊ) β
(β―β(1st βπ΄)) = ((β―β(2nd
βπ΄)) β
1))) |
16 | 10, 15 | mpcom 38 |
. . . . . 6
β’ (π΄ β (WalksβπΊ) β
(β―β(1st βπ΄)) = ((β―β(2nd
βπ΄)) β
1)) |
17 | | wlkop 28673 |
. . . . . . 7
β’ (π΅ β (WalksβπΊ) β π΅ = β¨(1st βπ΅), (2nd βπ΅)β©) |
18 | | eleq1 2820 |
. . . . . . . 8
β’ (π΅ = β¨(1st
βπ΅), (2nd
βπ΅)β© β
(π΅ β
(WalksβπΊ) β
β¨(1st βπ΅), (2nd βπ΅)β© β (WalksβπΊ))) |
19 | | df-br 5126 |
. . . . . . . . 9
β’
((1st βπ΅)(WalksβπΊ)(2nd βπ΅) β β¨(1st βπ΅), (2nd βπ΅)β© β
(WalksβπΊ)) |
20 | | wlklenvm1 28667 |
. . . . . . . . 9
β’
((1st βπ΅)(WalksβπΊ)(2nd βπ΅) β (β―β(1st
βπ΅)) =
((β―β(2nd βπ΅)) β 1)) |
21 | 19, 20 | sylbir 234 |
. . . . . . . 8
β’
(β¨(1st βπ΅), (2nd βπ΅)β© β (WalksβπΊ) β
(β―β(1st βπ΅)) = ((β―β(2nd
βπ΅)) β
1)) |
22 | 18, 21 | syl6bi 252 |
. . . . . . 7
β’ (π΅ = β¨(1st
βπ΅), (2nd
βπ΅)β© β
(π΅ β
(WalksβπΊ) β
(β―β(1st βπ΅)) = ((β―β(2nd
βπ΅)) β
1))) |
23 | 17, 22 | mpcom 38 |
. . . . . 6
β’ (π΅ β (WalksβπΊ) β
(β―β(1st βπ΅)) = ((β―β(2nd
βπ΅)) β
1)) |
24 | 16, 23 | anim12i 613 |
. . . . 5
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β ((β―β(1st
βπ΄)) =
((β―β(2nd βπ΄)) β 1) β§
(β―β(1st βπ΅)) = ((β―β(2nd
βπ΅)) β
1))) |
25 | | eqwrd 14472 |
. . . . . . . 8
β’
(((1st βπ΄) β Word dom (iEdgβπΊ) β§ (1st
βπ΅) β Word dom
(iEdgβπΊ)) β
((1st βπ΄)
= (1st βπ΅)
β ((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0..^(β―β(1st βπ΄)))((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)))) |
26 | 25 | ad2ant2r 745 |
. . . . . . 7
β’
((((1st βπ΄) β Word dom (iEdgβπΊ) β§ (2nd
βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) β§ ((1st βπ΅) β Word dom
(iEdgβπΊ) β§
(2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ))) β ((1st βπ΄) = (1st βπ΅) β
((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0..^(β―β(1st βπ΄)))((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)))) |
27 | 26 | adantr 481 |
. . . . . 6
β’
(((((1st βπ΄) β Word dom (iEdgβπΊ) β§ (2nd
βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) β§ ((1st βπ΅) β Word dom
(iEdgβπΊ) β§
(2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ))) β§ ((β―β(1st
βπ΄)) =
((β―β(2nd βπ΄)) β 1) β§
(β―β(1st βπ΅)) = ((β―β(2nd
βπ΅)) β 1)))
β ((1st βπ΄) = (1st βπ΅) β ((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0..^(β―β(1st
βπ΄)))((1st
βπ΄)βπ₯) = ((1st
βπ΅)βπ₯)))) |
28 | | lencl 14448 |
. . . . . . . . 9
β’
((1st βπ΄) β Word dom (iEdgβπΊ) β
(β―β(1st βπ΄)) β
β0) |
29 | 28 | adantr 481 |
. . . . . . . 8
β’
(((1st βπ΄) β Word dom (iEdgβπΊ) β§ (2nd
βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) β (β―β(1st
βπ΄)) β
β0) |
30 | | simpr 485 |
. . . . . . . 8
β’
(((1st βπ΄) β Word dom (iEdgβπΊ) β§ (2nd
βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) β (2nd βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) |
31 | | simpr 485 |
. . . . . . . 8
β’
(((1st βπ΅) β Word dom (iEdgβπΊ) β§ (2nd
βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ)) β (2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ)) |
32 | | 2ffzeq 13587 |
. . . . . . . 8
β’
(((β―β(1st βπ΄)) β β0 β§
(2nd βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ) β§ (2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ)) β ((2nd βπ΄) = (2nd βπ΅) β
((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0...(β―β(1st βπ΄)))((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)))) |
33 | 29, 30, 31, 32 | syl2an3an 1422 |
. . . . . . 7
β’
((((1st βπ΄) β Word dom (iEdgβπΊ) β§ (2nd
βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) β§ ((1st βπ΅) β Word dom
(iEdgβπΊ) β§
(2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ))) β ((2nd βπ΄) = (2nd βπ΅) β
((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0...(β―β(1st βπ΄)))((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)))) |
34 | 33 | adantr 481 |
. . . . . 6
β’
(((((1st βπ΄) β Word dom (iEdgβπΊ) β§ (2nd
βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) β§ ((1st βπ΅) β Word dom
(iEdgβπΊ) β§
(2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ))) β§ ((β―β(1st
βπ΄)) =
((β―β(2nd βπ΄)) β 1) β§
(β―β(1st βπ΅)) = ((β―β(2nd
βπ΅)) β 1)))
β ((2nd βπ΄) = (2nd βπ΅) β ((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0...(β―β(1st
βπ΄)))((2nd
βπ΄)βπ₯) = ((2nd
βπ΅)βπ₯)))) |
35 | 27, 34 | anbi12d 631 |
. . . . 5
β’
(((((1st βπ΄) β Word dom (iEdgβπΊ) β§ (2nd
βπ΄):(0...(β―β(1st
βπ΄)))βΆ(VtxβπΊ)) β§ ((1st βπ΅) β Word dom
(iEdgβπΊ) β§
(2nd βπ΅):(0...(β―β(1st
βπ΅)))βΆ(VtxβπΊ))) β§ ((β―β(1st
βπ΄)) =
((β―β(2nd βπ΄)) β 1) β§
(β―β(1st βπ΅)) = ((β―β(2nd
βπ΅)) β 1)))
β (((1st βπ΄) = (1st βπ΅) β§ (2nd βπ΄) = (2nd βπ΅)) β
(((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0..^(β―β(1st βπ΄)))((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ ((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0...(β―β(1st
βπ΄)))((2nd
βπ΄)βπ₯) = ((2nd
βπ΅)βπ₯))))) |
36 | 9, 24, 35 | syl2anc 584 |
. . . 4
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β (((1st βπ΄) = (1st βπ΅) β§ (2nd
βπ΄) = (2nd
βπ΅)) β
(((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0..^(β―β(1st βπ΄)))((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ ((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0...(β―β(1st
βπ΄)))((2nd
βπ΄)βπ₯) = ((2nd
βπ΅)βπ₯))))) |
37 | 36 | 3adant3 1132 |
. . 3
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ) β§ π = (β―β(1st
βπ΄))) β
(((1st βπ΄)
= (1st βπ΅)
β§ (2nd βπ΄) = (2nd βπ΅)) β (((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0..^(β―β(1st
βπ΄)))((1st
βπ΄)βπ₯) = ((1st
βπ΅)βπ₯)) β§
((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0...(β―β(1st βπ΄)))((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯))))) |
38 | | eqeq1 2735 |
. . . . . . 7
β’ (π =
(β―β(1st βπ΄)) β (π = (β―β(1st
βπ΅)) β
(β―β(1st βπ΄)) = (β―β(1st
βπ΅)))) |
39 | | oveq2 7385 |
. . . . . . . 8
β’ (π =
(β―β(1st βπ΄)) β (0..^π) = (0..^(β―β(1st
βπ΄)))) |
40 | 39 | raleqdv 3324 |
. . . . . . 7
β’ (π =
(β―β(1st βπ΄)) β (βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯) β βπ₯ β (0..^(β―β(1st
βπ΄)))((1st
βπ΄)βπ₯) = ((1st
βπ΅)βπ₯))) |
41 | 38, 40 | anbi12d 631 |
. . . . . 6
β’ (π =
(β―β(1st βπ΄)) β ((π = (β―β(1st
βπ΅)) β§
βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β ((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0..^(β―β(1st
βπ΄)))((1st
βπ΄)βπ₯) = ((1st
βπ΅)βπ₯)))) |
42 | | oveq2 7385 |
. . . . . . . 8
β’ (π =
(β―β(1st βπ΄)) β (0...π) = (0...(β―β(1st
βπ΄)))) |
43 | 42 | raleqdv 3324 |
. . . . . . 7
β’ (π =
(β―β(1st βπ΄)) β (βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯) β βπ₯ β (0...(β―β(1st
βπ΄)))((2nd
βπ΄)βπ₯) = ((2nd
βπ΅)βπ₯))) |
44 | 38, 43 | anbi12d 631 |
. . . . . 6
β’ (π =
(β―β(1st βπ΄)) β ((π = (β―β(1st
βπ΅)) β§
βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)) β ((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0...(β―β(1st
βπ΄)))((2nd
βπ΄)βπ₯) = ((2nd
βπ΅)βπ₯)))) |
45 | 41, 44 | anbi12d 631 |
. . . . 5
β’ (π =
(β―β(1st βπ΄)) β (((π = (β―β(1st
βπ΅)) β§
βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯))) β (((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0..^(β―β(1st
βπ΄)))((1st
βπ΄)βπ₯) = ((1st
βπ΅)βπ₯)) β§
((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0...(β―β(1st βπ΄)))((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯))))) |
46 | 45 | bibi2d 342 |
. . . 4
β’ (π =
(β―β(1st βπ΄)) β ((((1st βπ΄) = (1st βπ΅) β§ (2nd
βπ΄) = (2nd
βπ΅)) β ((π =
(β―β(1st βπ΅)) β§ βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)))) β (((1st βπ΄) = (1st βπ΅) β§ (2nd
βπ΄) = (2nd
βπ΅)) β
(((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0..^(β―β(1st βπ΄)))((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ ((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0...(β―β(1st
βπ΄)))((2nd
βπ΄)βπ₯) = ((2nd
βπ΅)βπ₯)))))) |
47 | 46 | 3ad2ant3 1135 |
. . 3
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ) β§ π = (β―β(1st
βπ΄))) β
((((1st βπ΄) = (1st βπ΅) β§ (2nd βπ΄) = (2nd βπ΅)) β ((π = (β―β(1st
βπ΅)) β§
βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)))) β (((1st βπ΄) = (1st βπ΅) β§ (2nd
βπ΄) = (2nd
βπ΅)) β
(((β―β(1st βπ΄)) = (β―β(1st
βπ΅)) β§
βπ₯ β
(0..^(β―β(1st βπ΄)))((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ ((β―β(1st
βπ΄)) =
(β―β(1st βπ΅)) β§ βπ₯ β (0...(β―β(1st
βπ΄)))((2nd
βπ΄)βπ₯) = ((2nd
βπ΅)βπ₯)))))) |
48 | 37, 47 | mpbird 256 |
. 2
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ) β§ π = (β―β(1st
βπ΄))) β
(((1st βπ΄)
= (1st βπ΅)
β§ (2nd βπ΄) = (2nd βπ΅)) β ((π = (β―β(1st
βπ΅)) β§
βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯))))) |
49 | | 1st2ndb 7981 |
. . . . 5
β’ (π΄ β (V Γ V) β
π΄ = β¨(1st
βπ΄), (2nd
βπ΄)β©) |
50 | 10, 49 | sylibr 233 |
. . . 4
β’ (π΄ β (WalksβπΊ) β π΄ β (V Γ V)) |
51 | | 1st2ndb 7981 |
. . . . 5
β’ (π΅ β (V Γ V) β
π΅ = β¨(1st
βπ΅), (2nd
βπ΅)β©) |
52 | 17, 51 | sylibr 233 |
. . . 4
β’ (π΅ β (WalksβπΊ) β π΅ β (V Γ V)) |
53 | | xpopth 7982 |
. . . 4
β’ ((π΄ β (V Γ V) β§
π΅ β (V Γ V))
β (((1st βπ΄) = (1st βπ΅) β§ (2nd βπ΄) = (2nd βπ΅)) β π΄ = π΅)) |
54 | 50, 52, 53 | syl2an 596 |
. . 3
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ)) β (((1st βπ΄) = (1st βπ΅) β§ (2nd
βπ΄) = (2nd
βπ΅)) β π΄ = π΅)) |
55 | 54 | 3adant3 1132 |
. 2
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ) β§ π = (β―β(1st
βπ΄))) β
(((1st βπ΄)
= (1st βπ΅)
β§ (2nd βπ΄) = (2nd βπ΅)) β π΄ = π΅)) |
56 | | 3anass 1095 |
. . . 4
β’ ((π =
(β―β(1st βπ΅)) β§ βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯) β§ βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)) β (π = (β―β(1st
βπ΅)) β§
(βπ₯ β
(0..^π)((1st
βπ΄)βπ₯) = ((1st
βπ΅)βπ₯) β§ βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)))) |
57 | | anandi 674 |
. . . 4
β’ ((π =
(β―β(1st βπ΅)) β§ (βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯) β§ βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯))) β ((π = (β―β(1st
βπ΅)) β§
βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)))) |
58 | 56, 57 | bitr2i 275 |
. . 3
β’ (((π =
(β―β(1st βπ΅)) β§ βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯))) β (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯) β§ βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯))) |
59 | 58 | a1i 11 |
. 2
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ) β§ π = (β―β(1st
βπ΄))) β (((π =
(β―β(1st βπ΅)) β§ βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯)) β§ (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯))) β (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯) β§ βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)))) |
60 | 48, 55, 59 | 3bitr3d 308 |
1
β’ ((π΄ β (WalksβπΊ) β§ π΅ β (WalksβπΊ) β§ π = (β―β(1st
βπ΄))) β (π΄ = π΅ β (π = (β―β(1st
βπ΅)) β§
βπ₯ β (0..^π)((1st βπ΄)βπ₯) = ((1st βπ΅)βπ₯) β§ βπ₯ β (0...π)((2nd βπ΄)βπ₯) = ((2nd βπ΅)βπ₯)))) |