Metamath Proof Explorer


Theorem usgr2pth

Description: In a simple graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018) (Revised by AV, 5-Jun-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Hypotheses usgr2pthlem.v V = Vtx G
usgr2pthlem.i I = iEdg G
Assertion usgr2pth G USGraph F Paths G P F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z

Proof

Step Hyp Ref Expression
1 usgr2pthlem.v V = Vtx G
2 usgr2pthlem.i I = iEdg G
3 usgr2pthspth G USGraph F = 2 F Paths G P F SPaths G P
4 usgrupgr G USGraph G UPGraph
5 4 adantr G USGraph F = 2 G UPGraph
6 isspth F SPaths G P F Trails G P Fun P -1
7 6 a1i G UPGraph F SPaths G P F Trails G P Fun P -1
8 1 2 upgrf1istrl G UPGraph F Trails G P F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1
9 8 anbi1d G UPGraph F Trails G P Fun P -1 F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1
10 oveq2 F = 2 0 ..^ F = 0 ..^ 2
11 f1eq2 0 ..^ F = 0 ..^ 2 F : 0 ..^ F 1-1 dom I F : 0 ..^ 2 1-1 dom I
12 10 11 syl F = 2 F : 0 ..^ F 1-1 dom I F : 0 ..^ 2 1-1 dom I
13 12 biimpd F = 2 F : 0 ..^ F 1-1 dom I F : 0 ..^ 2 1-1 dom I
14 13 adantl G USGraph F = 2 F : 0 ..^ F 1-1 dom I F : 0 ..^ 2 1-1 dom I
15 14 com12 F : 0 ..^ F 1-1 dom I G USGraph F = 2 F : 0 ..^ 2 1-1 dom I
16 15 3ad2ant1 F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 G USGraph F = 2 F : 0 ..^ 2 1-1 dom I
17 16 ad2antrl G UPGraph F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1 G USGraph F = 2 F : 0 ..^ 2 1-1 dom I
18 oveq2 F = 2 0 F = 0 2
19 18 feq2d F = 2 P : 0 F V P : 0 2 V
20 df-f1 P : 0 2 1-1 V P : 0 2 V Fun P -1
21 20 simplbi2 P : 0 2 V Fun P -1 P : 0 2 1-1 V
22 21 a1i F = 2 P : 0 2 V Fun P -1 P : 0 2 1-1 V
23 19 22 sylbid F = 2 P : 0 F V Fun P -1 P : 0 2 1-1 V
24 23 adantl G USGraph F = 2 P : 0 F V Fun P -1 P : 0 2 1-1 V
25 24 com3l P : 0 F V Fun P -1 G USGraph F = 2 P : 0 2 1-1 V
26 25 3ad2ant2 F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1 G USGraph F = 2 P : 0 2 1-1 V
27 26 imp F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1 G USGraph F = 2 P : 0 2 1-1 V
28 27 adantl G UPGraph F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1 G USGraph F = 2 P : 0 2 1-1 V
29 1 2 usgr2pthlem F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 G USGraph F = 2 x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
30 29 ad2antrl G UPGraph F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1 G USGraph F = 2 x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
31 17 28 30 3jcad G UPGraph F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1 G USGraph F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
32 31 ex G UPGraph F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1 G USGraph F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
33 9 32 sylbid G UPGraph F Trails G P Fun P -1 G USGraph F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
34 7 33 sylbid G UPGraph F SPaths G P G USGraph F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
35 34 com23 G UPGraph G USGraph F = 2 F SPaths G P F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
36 5 35 mpcom G USGraph F = 2 F SPaths G P F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
37 3 36 sylbid G USGraph F = 2 F Paths G P F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
38 37 ex G USGraph F = 2 F Paths G P F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
39 38 impcomd G USGraph F Paths G P F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z
40 2nn0 2 0
41 f1f F : 0 ..^ 2 1-1 dom I F : 0 ..^ 2 dom I
42 fnfzo0hash 2 0 F : 0 ..^ 2 dom I F = 2
43 40 41 42 sylancr F : 0 ..^ 2 1-1 dom I F = 2
44 oveq2 2 = F 0 ..^ 2 = 0 ..^ F
45 44 eqcoms F = 2 0 ..^ 2 = 0 ..^ F
46 f1eq2 0 ..^ 2 = 0 ..^ F F : 0 ..^ 2 1-1 dom I F : 0 ..^ F 1-1 dom I
47 45 46 syl F = 2 F : 0 ..^ 2 1-1 dom I F : 0 ..^ F 1-1 dom I
48 47 biimpd F = 2 F : 0 ..^ 2 1-1 dom I F : 0 ..^ F 1-1 dom I
49 48 imp F = 2 F : 0 ..^ 2 1-1 dom I F : 0 ..^ F 1-1 dom I
50 49 adantr F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V F : 0 ..^ F 1-1 dom I
51 50 ad2antrr F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F : 0 ..^ F 1-1 dom I
52 f1f P : 0 2 1-1 V P : 0 2 V
53 oveq2 2 = F 0 2 = 0 F
54 53 eqcoms F = 2 0 2 = 0 F
55 54 adantr F = 2 F : 0 ..^ 2 1-1 dom I 0 2 = 0 F
56 55 feq2d F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 V P : 0 F V
57 52 56 syl5ib F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V P : 0 F V
58 57 imp F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V P : 0 F V
59 58 ad2antrr F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph P : 0 F V
60 eqcom P 0 = x x = P 0
61 60 biimpi P 0 = x x = P 0
62 61 3ad2ant1 P 0 = x P 1 = y P 2 = z x = P 0
63 eqcom P 1 = y y = P 1
64 63 biimpi P 1 = y y = P 1
65 64 3ad2ant2 P 0 = x P 1 = y P 2 = z y = P 1
66 62 65 preq12d P 0 = x P 1 = y P 2 = z x y = P 0 P 1
67 66 eqeq2d P 0 = x P 1 = y P 2 = z I F 0 = x y I F 0 = P 0 P 1
68 67 biimpcd I F 0 = x y P 0 = x P 1 = y P 2 = z I F 0 = P 0 P 1
69 68 adantr I F 0 = x y I F 1 = y z P 0 = x P 1 = y P 2 = z I F 0 = P 0 P 1
70 69 impcom P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z I F 0 = P 0 P 1
71 eqcom P 2 = z z = P 2
72 71 biimpi P 2 = z z = P 2
73 72 3ad2ant3 P 0 = x P 1 = y P 2 = z z = P 2
74 65 73 preq12d P 0 = x P 1 = y P 2 = z y z = P 1 P 2
75 74 eqeq2d P 0 = x P 1 = y P 2 = z I F 1 = y z I F 1 = P 1 P 2
76 75 biimpcd I F 1 = y z P 0 = x P 1 = y P 2 = z I F 1 = P 1 P 2
77 76 adantl I F 0 = x y I F 1 = y z P 0 = x P 1 = y P 2 = z I F 1 = P 1 P 2
78 77 impcom P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z I F 1 = P 1 P 2
79 70 78 jca P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z I F 0 = P 0 P 1 I F 1 = P 1 P 2
80 79 rexlimivw z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z I F 0 = P 0 P 1 I F 1 = P 1 P 2
81 80 rexlimivw y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z I F 0 = P 0 P 1 I F 1 = P 1 P 2
82 81 rexlimivw x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z I F 0 = P 0 P 1 I F 1 = P 1 P 2
83 82 a1i13 F = 2 x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph I F 0 = P 0 P 1 I F 1 = P 1 P 2
84 fzo0to2pr 0 ..^ 2 = 0 1
85 10 84 eqtrdi F = 2 0 ..^ F = 0 1
86 85 raleqdv F = 2 i 0 ..^ F I F i = P i P i + 1 i 0 1 I F i = P i P i + 1
87 2wlklem i 0 1 I F i = P i P i + 1 I F 0 = P 0 P 1 I F 1 = P 1 P 2
88 86 87 bitrdi F = 2 i 0 ..^ F I F i = P i P i + 1 I F 0 = P 0 P 1 I F 1 = P 1 P 2
89 88 imbi2d F = 2 G USGraph i 0 ..^ F I F i = P i P i + 1 G USGraph I F 0 = P 0 P 1 I F 1 = P 1 P 2
90 83 89 sylibrd F = 2 x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph i 0 ..^ F I F i = P i P i + 1
91 90 ad2antrr F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph i 0 ..^ F I F i = P i P i + 1
92 91 imp F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph i 0 ..^ F I F i = P i P i + 1
93 92 imp F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph i 0 ..^ F I F i = P i P i + 1
94 51 59 93 3jca F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1
95 20 simprbi P : 0 2 1-1 V Fun P -1
96 95 adantl F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V Fun P -1
97 96 ad2antrr F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph Fun P -1
98 94 97 jca F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1
99 7 9 bitrd G UPGraph F SPaths G P F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1
100 4 99 syl G USGraph F SPaths G P F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1
101 100 adantl F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F SPaths G P F : 0 ..^ F 1-1 dom I P : 0 F V i 0 ..^ F I F i = P i P i + 1 Fun P -1
102 98 101 mpbird F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F SPaths G P
103 simpr F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph G USGraph
104 simp-4l F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F = 2
105 103 104 3 syl2anc F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F Paths G P F SPaths G P
106 102 105 mpbird F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F Paths G P
107 106 104 jca F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F Paths G P F = 2
108 107 ex F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F Paths G P F = 2
109 108 exp41 F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F Paths G P F = 2
110 43 109 mpcom F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F Paths G P F = 2
111 110 3imp F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z G USGraph F Paths G P F = 2
112 111 com12 G USGraph F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z F Paths G P F = 2
113 39 112 impbid G USGraph F Paths G P F = 2 F : 0 ..^ 2 1-1 dom I P : 0 2 1-1 V x V y V x z V x y P 0 = x P 1 = y P 2 = z I F 0 = x y I F 1 = y z