Metamath Proof Explorer


Theorem uspgrn2crct

Description: In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017) (Revised by AV, 3-Feb-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Assertion uspgrn2crct G USHGraph F Circuits G P F 2

Proof

Step Hyp Ref Expression
1 crctprop F Circuits G P F Trails G P P 0 = P F
2 istrl F Trails G P F Walks G P Fun F -1
3 uspgrupgr G USHGraph G UPGraph
4 eqid Vtx G = Vtx G
5 eqid iEdg G = iEdg G
6 4 5 upgriswlk G UPGraph F Walks G P F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
7 preq2 P 2 = P 0 P 1 P 2 = P 1 P 0
8 prcom P 1 P 0 = P 0 P 1
9 7 8 eqtrdi P 2 = P 0 P 1 P 2 = P 0 P 1
10 9 eqcoms P 0 = P 2 P 1 P 2 = P 0 P 1
11 10 eqeq2d P 0 = P 2 iEdg G F 1 = P 1 P 2 iEdg G F 1 = P 0 P 1
12 11 anbi2d P 0 = P 2 iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 0 P 1
13 12 ad2antrr P 0 = P 2 F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 0 P 1
14 eqtr3 iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 0 P 1 iEdg G F 0 = iEdg G F 1
15 4 5 uspgrf G USHGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2
16 15 adantl Fun F -1 G USHGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2
17 16 adantl F = 2 Fun F -1 G USHGraph iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2
18 17 adantr F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2
19 df-f1 F : 0 ..^ F 1-1 dom iEdg G F : 0 ..^ F dom iEdg G Fun F -1
20 19 simplbi2 F : 0 ..^ F dom iEdg G Fun F -1 F : 0 ..^ F 1-1 dom iEdg G
21 wrdf F Word dom iEdg G F : 0 ..^ F dom iEdg G
22 20 21 syl11 Fun F -1 F Word dom iEdg G F : 0 ..^ F 1-1 dom iEdg G
23 22 adantr Fun F -1 G USHGraph F Word dom iEdg G F : 0 ..^ F 1-1 dom iEdg G
24 23 adantl F = 2 Fun F -1 G USHGraph F Word dom iEdg G F : 0 ..^ F 1-1 dom iEdg G
25 24 imp F = 2 Fun F -1 G USHGraph F Word dom iEdg G F : 0 ..^ F 1-1 dom iEdg G
26 2nn 2
27 lbfzo0 0 0 ..^ 2 2
28 26 27 mpbir 0 0 ..^ 2
29 1nn0 1 0
30 1lt2 1 < 2
31 elfzo0 1 0 ..^ 2 1 0 2 1 < 2
32 29 26 30 31 mpbir3an 1 0 ..^ 2
33 28 32 pm3.2i 0 0 ..^ 2 1 0 ..^ 2
34 oveq2 F = 2 0 ..^ F = 0 ..^ 2
35 34 eleq2d F = 2 0 0 ..^ F 0 0 ..^ 2
36 34 eleq2d F = 2 1 0 ..^ F 1 0 ..^ 2
37 35 36 anbi12d F = 2 0 0 ..^ F 1 0 ..^ F 0 0 ..^ 2 1 0 ..^ 2
38 33 37 mpbiri F = 2 0 0 ..^ F 1 0 ..^ F
39 38 ad2antrr F = 2 Fun F -1 G USHGraph F Word dom iEdg G 0 0 ..^ F 1 0 ..^ F
40 f1cofveqaeq iEdg G : dom iEdg G 1-1 x 𝒫 Vtx G | x 2 F : 0 ..^ F 1-1 dom iEdg G 0 0 ..^ F 1 0 ..^ F iEdg G F 0 = iEdg G F 1 0 = 1
41 18 25 39 40 syl21anc F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = iEdg G F 1 0 = 1
42 0ne1 0 1
43 eqneqall 0 = 1 0 1 P 0 P 2
44 41 42 43 syl6mpi F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = iEdg G F 1 P 0 P 2
45 44 adantll P 0 = P 2 F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = iEdg G F 1 P 0 P 2
46 14 45 syl5 P 0 = P 2 F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 0 P 1 P 0 P 2
47 13 46 sylbid P 0 = P 2 F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 P 0 P 2
48 47 expimpd P 0 = P 2 F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 P 0 P 2
49 48 ex P 0 = P 2 F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 P 0 P 2
50 2a1 P 0 P 2 F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 P 0 P 2
51 49 50 pm2.61ine F = 2 Fun F -1 G USHGraph F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 P 0 P 2
52 fzo0to2pr 0 ..^ 2 = 0 1
53 34 52 eqtrdi F = 2 0 ..^ F = 0 1
54 53 raleqdv F = 2 k 0 ..^ F iEdg G F k = P k P k + 1 k 0 1 iEdg G F k = P k P k + 1
55 2wlklem k 0 1 iEdg G F k = P k P k + 1 iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2
56 54 55 syl6bb F = 2 k 0 ..^ F iEdg G F k = P k P k + 1 iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2
57 56 anbi2d F = 2 F Word dom iEdg G k 0 ..^ F iEdg G F k = P k P k + 1 F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2
58 fveq2 F = 2 P F = P 2
59 58 neeq2d F = 2 P 0 P F P 0 P 2
60 57 59 imbi12d F = 2 F Word dom iEdg G k 0 ..^ F iEdg G F k = P k P k + 1 P 0 P F F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 P 0 P 2
61 60 adantr F = 2 Fun F -1 G USHGraph F Word dom iEdg G k 0 ..^ F iEdg G F k = P k P k + 1 P 0 P F F Word dom iEdg G iEdg G F 0 = P 0 P 1 iEdg G F 1 = P 1 P 2 P 0 P 2
62 51 61 mpbird F = 2 Fun F -1 G USHGraph F Word dom iEdg G k 0 ..^ F iEdg G F k = P k P k + 1 P 0 P F
63 62 ex F = 2 Fun F -1 G USHGraph F Word dom iEdg G k 0 ..^ F iEdg G F k = P k P k + 1 P 0 P F
64 63 com13 F Word dom iEdg G k 0 ..^ F iEdg G F k = P k P k + 1 Fun F -1 G USHGraph F = 2 P 0 P F
65 64 expd F Word dom iEdg G k 0 ..^ F iEdg G F k = P k P k + 1 Fun F -1 G USHGraph F = 2 P 0 P F
66 65 3adant2 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 Fun F -1 G USHGraph F = 2 P 0 P F
67 6 66 syl6bi G UPGraph F Walks G P Fun F -1 G USHGraph F = 2 P 0 P F
68 67 impd G UPGraph F Walks G P Fun F -1 G USHGraph F = 2 P 0 P F
69 68 com23 G UPGraph G USHGraph F Walks G P Fun F -1 F = 2 P 0 P F
70 3 69 mpcom G USHGraph F Walks G P Fun F -1 F = 2 P 0 P F
71 70 com12 F Walks G P Fun F -1 G USHGraph F = 2 P 0 P F
72 2 71 sylbi F Trails G P G USHGraph F = 2 P 0 P F
73 72 imp F Trails G P G USHGraph F = 2 P 0 P F
74 73 necon2d F Trails G P G USHGraph P 0 = P F F 2
75 74 impancom F Trails G P P 0 = P F G USHGraph F 2
76 1 75 syl F Circuits G P G USHGraph F 2
77 76 impcom G USHGraph F Circuits G P F 2