Metamath Proof Explorer


Theorem numclwwlk1lem2f1

Description: T is a 1-1 function. (Contributed by AV, 26-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 23-Feb-2022) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v V = Vtx G
extwwlkfab.c C = v V , n 2 w v ClWWalksNOn G n | w n 2 = v
extwwlkfab.f F = X ClWWalksNOn G N 2
numclwwlk.t T = u X C N u prefix N 2 u N 1
Assertion numclwwlk1lem2f1 G USGraph X V N 3 T : X C N 1-1 F × G NeighbVtx X

Proof

Step Hyp Ref Expression
1 extwwlkfab.v V = Vtx G
2 extwwlkfab.c C = v V , n 2 w v ClWWalksNOn G n | w n 2 = v
3 extwwlkfab.f F = X ClWWalksNOn G N 2
4 numclwwlk.t T = u X C N u prefix N 2 u N 1
5 1 2 3 4 numclwwlk1lem2f G USGraph X V N 3 T : X C N F × G NeighbVtx X
6 1 2 3 4 numclwwlk1lem2fv p X C N T p = p prefix N 2 p N 1
7 6 ad2antrl G USGraph X V N 3 p X C N a X C N T p = p prefix N 2 p N 1
8 1 2 3 4 numclwwlk1lem2fv a X C N T a = a prefix N 2 a N 1
9 8 ad2antll G USGraph X V N 3 p X C N a X C N T a = a prefix N 2 a N 1
10 7 9 eqeq12d G USGraph X V N 3 p X C N a X C N T p = T a p prefix N 2 p N 1 = a prefix N 2 a N 1
11 ovex p prefix N 2 V
12 fvex p N 1 V
13 11 12 opth p prefix N 2 p N 1 = a prefix N 2 a N 1 p prefix N 2 = a prefix N 2 p N 1 = a N 1
14 uzuzle23 N 3 N 2
15 2 2clwwlkel X V N 2 p X C N p X ClWWalksNOn G N p N 2 = X
16 isclwwlknon p X ClWWalksNOn G N p N ClWWalksN G p 0 = X
17 16 anbi1i p X ClWWalksNOn G N p N 2 = X p N ClWWalksN G p 0 = X p N 2 = X
18 15 17 bitrdi X V N 2 p X C N p N ClWWalksN G p 0 = X p N 2 = X
19 2 2clwwlkel X V N 2 a X C N a X ClWWalksNOn G N a N 2 = X
20 isclwwlknon a X ClWWalksNOn G N a N ClWWalksN G a 0 = X
21 20 anbi1i a X ClWWalksNOn G N a N 2 = X a N ClWWalksN G a 0 = X a N 2 = X
22 19 21 bitrdi X V N 2 a X C N a N ClWWalksN G a 0 = X a N 2 = X
23 18 22 anbi12d X V N 2 p X C N a X C N p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X
24 14 23 sylan2 X V N 3 p X C N a X C N p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X
25 24 3adant1 G USGraph X V N 3 p X C N a X C N p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X
26 1 clwwlknbp p N ClWWalksN G p Word V p = N
27 26 adantr p N ClWWalksN G p 0 = X p Word V p = N
28 27 adantr p N ClWWalksN G p 0 = X p N 2 = X p Word V p = N
29 simpr p N ClWWalksN G p 0 = X p 0 = X
30 29 adantr p N ClWWalksN G p 0 = X p N 2 = X p 0 = X
31 simpr p N ClWWalksN G p 0 = X p N 2 = X p N 2 = X
32 29 eqcomd p N ClWWalksN G p 0 = X X = p 0
33 32 adantr p N ClWWalksN G p 0 = X p N 2 = X X = p 0
34 31 33 eqtrd p N ClWWalksN G p 0 = X p N 2 = X p N 2 = p 0
35 28 30 34 jca32 p N ClWWalksN G p 0 = X p N 2 = X p Word V p = N p 0 = X p N 2 = p 0
36 1 clwwlknbp a N ClWWalksN G a Word V a = N
37 36 adantr a N ClWWalksN G a 0 = X a Word V a = N
38 37 adantr a N ClWWalksN G a 0 = X a N 2 = X a Word V a = N
39 simpr a N ClWWalksN G a 0 = X a 0 = X
40 39 adantr a N ClWWalksN G a 0 = X a N 2 = X a 0 = X
41 simpr a N ClWWalksN G a 0 = X a N 2 = X a N 2 = X
42 39 eqcomd a N ClWWalksN G a 0 = X X = a 0
43 42 adantr a N ClWWalksN G a 0 = X a N 2 = X X = a 0
44 41 43 eqtrd a N ClWWalksN G a 0 = X a N 2 = X a N 2 = a 0
45 38 40 44 jca32 a N ClWWalksN G a 0 = X a N 2 = X a Word V a = N a 0 = X a N 2 = a 0
46 eqtr3 p = N a = N p = a
47 46 expcom a = N p = N p = a
48 47 ad2antlr a Word V a = N a 0 = X a N 2 = a 0 p = N p = a
49 48 com12 p = N a Word V a = N a 0 = X a N 2 = a 0 p = a
50 49 ad2antlr p Word V p = N p 0 = X p N 2 = p 0 a Word V a = N a 0 = X a N 2 = a 0 p = a
51 50 imp p Word V p = N p 0 = X p N 2 = p 0 a Word V a = N a 0 = X a N 2 = a 0 p = a
52 35 45 51 syl2an p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p = a
53 52 3ad2ant2 N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p = a
54 27 simprd p N ClWWalksN G p 0 = X p = N
55 54 adantr p N ClWWalksN G p 0 = X p N 2 = X p = N
56 55 eqcomd p N ClWWalksN G p 0 = X p N 2 = X N = p
57 56 adantr p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X N = p
58 57 oveq1d p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X N 2 = p 2
59 58 oveq2d p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = p prefix p 2
60 58 oveq2d p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X a prefix N 2 = a prefix p 2
61 59 60 eqeq12d p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p prefix p 2 = a prefix p 2
62 61 biimpcd p prefix N 2 = a prefix N 2 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix p 2 = a prefix p 2
63 62 adantr p prefix N 2 = a prefix N 2 p N 1 = a N 1 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix p 2 = a prefix p 2
64 63 impcom p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p prefix p 2 = a prefix p 2
65 55 oveq1d p N ClWWalksN G p 0 = X p N 2 = X p 2 = N 2
66 65 fveq2d p N ClWWalksN G p 0 = X p N 2 = X p p 2 = p N 2
67 66 31 eqtrd p N ClWWalksN G p 0 = X p N 2 = X p p 2 = X
68 67 adantr p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p p 2 = X
69 41 eqcomd a N ClWWalksN G a 0 = X a N 2 = X X = a N 2
70 69 adantl p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X X = a N 2
71 58 fveq2d p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X a N 2 = a p 2
72 70 71 eqtrd p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X X = a p 2
73 68 72 eqtrd p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p p 2 = a p 2
74 73 adantr p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p p 2 = a p 2
75 lsw p Word V lastS p = p p 1
76 fvoveq1 p = N p p 1 = p N 1
77 75 76 sylan9eq p Word V p = N lastS p = p N 1
78 26 77 syl p N ClWWalksN G lastS p = p N 1
79 78 eqcomd p N ClWWalksN G p N 1 = lastS p
80 79 ad3antrrr p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p N 1 = lastS p
81 lsw a Word V lastS a = a a 1
82 81 adantr a Word V a = N lastS a = a a 1
83 oveq1 N = a N 1 = a 1
84 83 eqcoms a = N N 1 = a 1
85 84 fveq2d a = N a N 1 = a a 1
86 85 eqeq2d a = N lastS a = a N 1 lastS a = a a 1
87 86 adantl a Word V a = N lastS a = a N 1 lastS a = a a 1
88 82 87 mpbird a Word V a = N lastS a = a N 1
89 36 88 syl a N ClWWalksN G lastS a = a N 1
90 89 eqcomd a N ClWWalksN G a N 1 = lastS a
91 90 adantr a N ClWWalksN G a 0 = X a N 1 = lastS a
92 91 ad2antrl p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X a N 1 = lastS a
93 80 92 eqeq12d p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p N 1 = a N 1 lastS p = lastS a
94 93 biimpd p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p N 1 = a N 1 lastS p = lastS a
95 94 adantld p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 lastS p = lastS a
96 95 imp p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 lastS p = lastS a
97 64 74 96 3jca p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p prefix p 2 = a prefix p 2 p p 2 = a p 2 lastS p = lastS a
98 97 3adant1 N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p prefix p 2 = a prefix p 2 p p 2 = a p 2 lastS p = lastS a
99 1 clwwlknwrd p N ClWWalksN G p Word V
100 99 ad3antrrr p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p Word V
101 100 3ad2ant2 N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p Word V
102 1 clwwlknwrd a N ClWWalksN G a Word V
103 102 adantr a N ClWWalksN G a 0 = X a Word V
104 103 ad2antrl p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X a Word V
105 104 3ad2ant2 N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 a Word V
106 clwwlknlen p N ClWWalksN G p = N
107 eluz2b1 N 2 N 1 < N
108 breq2 N = p 1 < N 1 < p
109 108 eqcoms p = N 1 < N 1 < p
110 109 biimpcd 1 < N p = N 1 < p
111 107 110 simplbiim N 2 p = N 1 < p
112 14 106 111 syl2imc p N ClWWalksN G N 3 1 < p
113 112 ad3antrrr p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X N 3 1 < p
114 113 impcom N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X 1 < p
115 114 3adant3 N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 1 < p
116 2swrd2eqwrdeq p Word V a Word V 1 < p p = a p = a p prefix p 2 = a prefix p 2 p p 2 = a p 2 lastS p = lastS a
117 101 105 115 116 syl3anc N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p = a p = a p prefix p 2 = a prefix p 2 p p 2 = a p 2 lastS p = lastS a
118 53 98 117 mpbir2and N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p = a
119 118 3exp N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p = a
120 119 3ad2ant3 G USGraph X V N 3 p N ClWWalksN G p 0 = X p N 2 = X a N ClWWalksN G a 0 = X a N 2 = X p prefix N 2 = a prefix N 2 p N 1 = a N 1 p = a
121 25 120 sylbid G USGraph X V N 3 p X C N a X C N p prefix N 2 = a prefix N 2 p N 1 = a N 1 p = a
122 121 imp G USGraph X V N 3 p X C N a X C N p prefix N 2 = a prefix N 2 p N 1 = a N 1 p = a
123 13 122 syl5bi G USGraph X V N 3 p X C N a X C N p prefix N 2 p N 1 = a prefix N 2 a N 1 p = a
124 10 123 sylbid G USGraph X V N 3 p X C N a X C N T p = T a p = a
125 124 ralrimivva G USGraph X V N 3 p X C N a X C N T p = T a p = a
126 dff13 T : X C N 1-1 F × G NeighbVtx X T : X C N F × G NeighbVtx X p X C N a X C N T p = T a p = a
127 5 125 126 sylanbrc G USGraph X V N 3 T : X C N 1-1 F × G NeighbVtx X