Metamath Proof Explorer


Theorem numclwwlk1lem2fo

Description: T is an onto function. (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 13-Feb-2022) (Revised by AV, 31-Oct-2022)

Ref Expression
Hypotheses extwwlkfab.v V=VtxG
extwwlkfab.c C=vV,n2wvClWWalksNOnGn|wn2=v
extwwlkfab.f F=XClWWalksNOnGN2
numclwwlk.t T=uXCNuprefixN2uN1
Assertion numclwwlk1lem2fo GUSGraphXVN3T:XCNontoF×GNeighbVtxX

Proof

Step Hyp Ref Expression
1 extwwlkfab.v V=VtxG
2 extwwlkfab.c C=vV,n2wvClWWalksNOnGn|wn2=v
3 extwwlkfab.f F=XClWWalksNOnGN2
4 numclwwlk.t T=uXCNuprefixN2uN1
5 1 2 3 4 numclwwlk1lem2f GUSGraphXVN3T:XCNF×GNeighbVtxX
6 elxp pF×GNeighbVtxXabp=abaFbGNeighbVtxX
7 1 2 3 numclwwlk1lem2foa GUSGraphXVN3aFbGNeighbVtxXa++⟨“X”⟩++⟨“b”⟩XCN
8 7 com12 aFbGNeighbVtxXGUSGraphXVN3a++⟨“X”⟩++⟨“b”⟩XCN
9 8 adantl p=abaFbGNeighbVtxXGUSGraphXVN3a++⟨“X”⟩++⟨“b”⟩XCN
10 9 imp p=abaFbGNeighbVtxXGUSGraphXVN3a++⟨“X”⟩++⟨“b”⟩XCN
11 simpl a++⟨“X”⟩++⟨“b”⟩XCNp=abaFbGNeighbVtxXGUSGraphXVN3a++⟨“X”⟩++⟨“b”⟩XCN
12 fveq2 x=a++⟨“X”⟩++⟨“b”⟩Tx=Ta++⟨“X”⟩++⟨“b”⟩
13 12 eqeq2d x=a++⟨“X”⟩++⟨“b”⟩p=Txp=Ta++⟨“X”⟩++⟨“b”⟩
14 1 2 3 4 numclwwlk1lem2fv a++⟨“X”⟩++⟨“b”⟩XCNTa++⟨“X”⟩++⟨“b”⟩=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
15 14 adantr a++⟨“X”⟩++⟨“b”⟩XCNp=abaFbGNeighbVtxXGUSGraphXVN3Ta++⟨“X”⟩++⟨“b”⟩=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
16 15 eqeq2d a++⟨“X”⟩++⟨“b”⟩XCNp=abaFbGNeighbVtxXGUSGraphXVN3p=Ta++⟨“X”⟩++⟨“b”⟩p=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
17 13 16 sylan9bbr a++⟨“X”⟩++⟨“b”⟩XCNp=abaFbGNeighbVtxXGUSGraphXVN3x=a++⟨“X”⟩++⟨“b”⟩p=Txp=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
18 simprll a++⟨“X”⟩++⟨“b”⟩XCNp=abaFbGNeighbVtxXGUSGraphXVN3p=ab
19 1 nbgrisvtx bGNeighbVtxXbV
20 3 eleq2i aFaXClWWalksNOnGN2
21 uz3m2nn N3N2
22 21 nnne0d N3N20
23 22 3ad2ant3 GUSGraphXVN3N20
24 eqid EdgG=EdgG
25 1 24 clwwlknonel N20aXClWWalksNOnGN2aWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=X
26 23 25 syl GUSGraphXVN3aXClWWalksNOnGN2aWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=X
27 20 26 syl5bb GUSGraphXVN3aFaWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=X
28 df-3an aWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=XaWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=X
29 27 28 bitrdi GUSGraphXVN3aFaWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=X
30 simplll aWordVa=N2XVN3bVaWordV
31 s1cl XV⟨“X”⟩WordV
32 31 adantr XVN3⟨“X”⟩WordV
33 32 adantl aWordVa=N2XVN3⟨“X”⟩WordV
34 33 adantr aWordVa=N2XVN3bV⟨“X”⟩WordV
35 s1cl bV⟨“b”⟩WordV
36 35 adantl aWordVa=N2XVN3bV⟨“b”⟩WordV
37 ccatass aWordV⟨“X”⟩WordV⟨“b”⟩WordVa++⟨“X”⟩++⟨“b”⟩=a++⟨“X”⟩++⟨“b”⟩
38 37 oveq1d aWordV⟨“X”⟩WordV⟨“b”⟩WordVa++⟨“X”⟩++⟨“b”⟩prefixN2=a++⟨“X”⟩++⟨“b”⟩prefixN2
39 30 34 36 38 syl3anc aWordVa=N2XVN3bVa++⟨“X”⟩++⟨“b”⟩prefixN2=a++⟨“X”⟩++⟨“b”⟩prefixN2
40 ccatcl ⟨“X”⟩WordV⟨“b”⟩WordV⟨“X”⟩++⟨“b”⟩WordV
41 33 35 40 syl2an aWordVa=N2XVN3bV⟨“X”⟩++⟨“b”⟩WordV
42 simpr aWordVa=N2a=N2
43 42 eqcomd aWordVa=N2N2=a
44 43 adantr aWordVa=N2XVN3N2=a
45 44 adantr aWordVa=N2XVN3bVN2=a
46 pfxccatid aWordV⟨“X”⟩++⟨“b”⟩WordVN2=aa++⟨“X”⟩++⟨“b”⟩prefixN2=a
47 30 41 45 46 syl3anc aWordVa=N2XVN3bVa++⟨“X”⟩++⟨“b”⟩prefixN2=a
48 39 47 eqtr2d aWordVa=N2XVN3bVa=a++⟨“X”⟩++⟨“b”⟩prefixN2
49 1e2m1 1=21
50 49 a1i N31=21
51 50 oveq2d N3N1=N21
52 eluzelcn N3N
53 2cnd N32
54 1cnd N31
55 52 53 54 subsubd N3N21=N-2+1
56 51 55 eqtrd N3N1=N-2+1
57 56 adantl XVN3N1=N-2+1
58 57 adantl aWordVa=N2XVN3N1=N-2+1
59 58 adantr aWordVa=N2XVN3bVN1=N-2+1
60 59 fveq2d aWordVa=N2XVN3bVa++⟨“X”⟩++⟨“b”⟩N1=a++⟨“X”⟩++⟨“b”⟩N-2+1
61 simpll aWordVa=N2XVN3bVaWordVa=N2
62 simprl aWordVa=N2XVN3XV
63 62 anim1i aWordVa=N2XVN3bVXVbV
64 ccatw2s1p2 aWordVa=N2XVbVa++⟨“X”⟩++⟨“b”⟩N-2+1=b
65 61 63 64 syl2anc aWordVa=N2XVN3bVa++⟨“X”⟩++⟨“b”⟩N-2+1=b
66 60 65 eqtr2d aWordVa=N2XVN3bVb=a++⟨“X”⟩++⟨“b”⟩N1
67 48 66 opeq12d aWordVa=N2XVN3bVab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
68 67 exp31 aWordVa=N2XVN3bVab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
69 68 3ad2antl1 aWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2XVN3bVab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
70 69 adantr aWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=XXVN3bVab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
71 70 com12 XVN3aWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=XbVab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
72 71 3adant1 GUSGraphXVN3aWordVi0..^a1aiai+1EdgGlastSaa0EdgGa=N2a0=XbVab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
73 29 72 sylbid GUSGraphXVN3aFbVab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
74 73 com23 GUSGraphXVN3bVaFab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
75 19 74 syl5 GUSGraphXVN3bGNeighbVtxXaFab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
76 75 com13 aFbGNeighbVtxXGUSGraphXVN3ab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
77 76 imp aFbGNeighbVtxXGUSGraphXVN3ab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
78 77 adantl p=abaFbGNeighbVtxXGUSGraphXVN3ab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
79 78 imp p=abaFbGNeighbVtxXGUSGraphXVN3ab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
80 79 adantl a++⟨“X”⟩++⟨“b”⟩XCNp=abaFbGNeighbVtxXGUSGraphXVN3ab=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
81 18 80 eqtrd a++⟨“X”⟩++⟨“b”⟩XCNp=abaFbGNeighbVtxXGUSGraphXVN3p=a++⟨“X”⟩++⟨“b”⟩prefixN2a++⟨“X”⟩++⟨“b”⟩N1
82 11 17 81 rspcedvd a++⟨“X”⟩++⟨“b”⟩XCNp=abaFbGNeighbVtxXGUSGraphXVN3xXCNp=Tx
83 10 82 mpancom p=abaFbGNeighbVtxXGUSGraphXVN3xXCNp=Tx
84 83 ex p=abaFbGNeighbVtxXGUSGraphXVN3xXCNp=Tx
85 84 exlimivv abp=abaFbGNeighbVtxXGUSGraphXVN3xXCNp=Tx
86 6 85 sylbi pF×GNeighbVtxXGUSGraphXVN3xXCNp=Tx
87 86 impcom GUSGraphXVN3pF×GNeighbVtxXxXCNp=Tx
88 87 ralrimiva GUSGraphXVN3pF×GNeighbVtxXxXCNp=Tx
89 dffo3 T:XCNontoF×GNeighbVtxXT:XCNF×GNeighbVtxXpF×GNeighbVtxXxXCNp=Tx
90 5 88 89 sylanbrc GUSGraphXVN3T:XCNontoF×GNeighbVtxX