Metamath Proof Explorer


Theorem umgrwwlks2on

Description: A walk of length 2 between two vertices as word in a multigraph. This theorem would also hold for pseudographs, but to prove this the cases A = B and/or B = C must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 12-May-2021)

Ref Expression
Hypotheses s3wwlks2on.v V = Vtx G
usgrwwlks2on.e E = Edg G
Assertion umgrwwlks2on G UMGraph A V B V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C A B E B C E

Proof

Step Hyp Ref Expression
1 s3wwlks2on.v V = Vtx G
2 usgrwwlks2on.e E = Edg G
3 umgrupgr G UMGraph G UPGraph
4 3 adantr G UMGraph A V B V C V G UPGraph
5 simp1 A V B V C V A V
6 5 adantl G UMGraph A V B V C V A V
7 simpr3 G UMGraph A V B V C V C V
8 1 s3wwlks2on G UPGraph A V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C f f Walks G ⟨“ ABC ”⟩ f = 2
9 4 6 7 8 syl3anc G UMGraph A V B V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C f f Walks G ⟨“ ABC ”⟩ f = 2
10 eqid iEdg G = iEdg G
11 1 10 upgr2wlk G UPGraph f Walks G ⟨“ ABC ”⟩ f = 2 f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 iEdg G f 1 = ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2
12 3 11 syl G UMGraph f Walks G ⟨“ ABC ”⟩ f = 2 f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 iEdg G f 1 = ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2
13 12 adantr G UMGraph A V B V C V f Walks G ⟨“ ABC ”⟩ f = 2 f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 iEdg G f 1 = ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2
14 s3fv0 A V ⟨“ ABC ”⟩ 0 = A
15 14 3ad2ant1 A V B V C V ⟨“ ABC ”⟩ 0 = A
16 s3fv1 B V ⟨“ ABC ”⟩ 1 = B
17 16 3ad2ant2 A V B V C V ⟨“ ABC ”⟩ 1 = B
18 15 17 preq12d A V B V C V ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 = A B
19 18 eqeq2d A V B V C V iEdg G f 0 = ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 iEdg G f 0 = A B
20 s3fv2 C V ⟨“ ABC ”⟩ 2 = C
21 20 3ad2ant3 A V B V C V ⟨“ ABC ”⟩ 2 = C
22 17 21 preq12d A V B V C V ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2 = B C
23 22 eqeq2d A V B V C V iEdg G f 1 = ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2 iEdg G f 1 = B C
24 19 23 anbi12d A V B V C V iEdg G f 0 = ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 iEdg G f 1 = ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2 iEdg G f 0 = A B iEdg G f 1 = B C
25 24 adantl G UMGraph A V B V C V iEdg G f 0 = ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 iEdg G f 1 = ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2 iEdg G f 0 = A B iEdg G f 1 = B C
26 25 3anbi3d G UMGraph A V B V C V f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 iEdg G f 1 = ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2 f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C
27 umgruhgr G UMGraph G UHGraph
28 10 uhgrfun G UHGraph Fun iEdg G
29 fdmrn Fun iEdg G iEdg G : dom iEdg G ran iEdg G
30 simpr f : 0 ..^ 2 dom iEdg G iEdg G : dom iEdg G ran iEdg G iEdg G : dom iEdg G ran iEdg G
31 id f : 0 ..^ 2 dom iEdg G f : 0 ..^ 2 dom iEdg G
32 c0ex 0 V
33 32 prid1 0 0 1
34 fzo0to2pr 0 ..^ 2 = 0 1
35 33 34 eleqtrri 0 0 ..^ 2
36 35 a1i f : 0 ..^ 2 dom iEdg G 0 0 ..^ 2
37 31 36 ffvelrnd f : 0 ..^ 2 dom iEdg G f 0 dom iEdg G
38 37 adantr f : 0 ..^ 2 dom iEdg G iEdg G : dom iEdg G ran iEdg G f 0 dom iEdg G
39 30 38 ffvelrnd f : 0 ..^ 2 dom iEdg G iEdg G : dom iEdg G ran iEdg G iEdg G f 0 ran iEdg G
40 1ex 1 V
41 40 prid2 1 0 1
42 41 34 eleqtrri 1 0 ..^ 2
43 42 a1i f : 0 ..^ 2 dom iEdg G 1 0 ..^ 2
44 31 43 ffvelrnd f : 0 ..^ 2 dom iEdg G f 1 dom iEdg G
45 44 adantr f : 0 ..^ 2 dom iEdg G iEdg G : dom iEdg G ran iEdg G f 1 dom iEdg G
46 30 45 ffvelrnd f : 0 ..^ 2 dom iEdg G iEdg G : dom iEdg G ran iEdg G iEdg G f 1 ran iEdg G
47 39 46 jca f : 0 ..^ 2 dom iEdg G iEdg G : dom iEdg G ran iEdg G iEdg G f 0 ran iEdg G iEdg G f 1 ran iEdg G
48 47 ex f : 0 ..^ 2 dom iEdg G iEdg G : dom iEdg G ran iEdg G iEdg G f 0 ran iEdg G iEdg G f 1 ran iEdg G
49 48 3ad2ant1 f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C iEdg G : dom iEdg G ran iEdg G iEdg G f 0 ran iEdg G iEdg G f 1 ran iEdg G
50 49 com12 iEdg G : dom iEdg G ran iEdg G f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C iEdg G f 0 ran iEdg G iEdg G f 1 ran iEdg G
51 29 50 sylbi Fun iEdg G f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C iEdg G f 0 ran iEdg G iEdg G f 1 ran iEdg G
52 27 28 51 3syl G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C iEdg G f 0 ran iEdg G iEdg G f 1 ran iEdg G
53 52 imp G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C iEdg G f 0 ran iEdg G iEdg G f 1 ran iEdg G
54 eqcom iEdg G f 0 = A B A B = iEdg G f 0
55 54 biimpi iEdg G f 0 = A B A B = iEdg G f 0
56 55 adantr iEdg G f 0 = A B iEdg G f 1 = B C A B = iEdg G f 0
57 56 3ad2ant3 f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C A B = iEdg G f 0
58 57 adantl G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C A B = iEdg G f 0
59 edgval Edg G = ran iEdg G
60 2 59 eqtri E = ran iEdg G
61 60 a1i G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C E = ran iEdg G
62 58 61 eleq12d G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C A B E iEdg G f 0 ran iEdg G
63 eqcom iEdg G f 1 = B C B C = iEdg G f 1
64 63 biimpi iEdg G f 1 = B C B C = iEdg G f 1
65 64 adantl iEdg G f 0 = A B iEdg G f 1 = B C B C = iEdg G f 1
66 65 3ad2ant3 f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C B C = iEdg G f 1
67 66 adantl G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C B C = iEdg G f 1
68 67 61 eleq12d G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C B C E iEdg G f 1 ran iEdg G
69 62 68 anbi12d G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C A B E B C E iEdg G f 0 ran iEdg G iEdg G f 1 ran iEdg G
70 53 69 mpbird G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C A B E B C E
71 70 ex G UMGraph f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C A B E B C E
72 71 adantr G UMGraph A V B V C V f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = A B iEdg G f 1 = B C A B E B C E
73 26 72 sylbid G UMGraph A V B V C V f : 0 ..^ 2 dom iEdg G ⟨“ ABC ”⟩ : 0 2 V iEdg G f 0 = ⟨“ ABC ”⟩ 0 ⟨“ ABC ”⟩ 1 iEdg G f 1 = ⟨“ ABC ”⟩ 1 ⟨“ ABC ”⟩ 2 A B E B C E
74 13 73 sylbid G UMGraph A V B V C V f Walks G ⟨“ ABC ”⟩ f = 2 A B E B C E
75 74 exlimdv G UMGraph A V B V C V f f Walks G ⟨“ ABC ”⟩ f = 2 A B E B C E
76 2 umgr2wlk G UMGraph A B E B C E f p f Walks G p f = 2 A = p 0 B = p 1 C = p 2
77 wlklenvp1 f Walks G p p = f + 1
78 oveq1 f = 2 f + 1 = 2 + 1
79 2p1e3 2 + 1 = 3
80 78 79 eqtrdi f = 2 f + 1 = 3
81 80 adantr f = 2 A = p 0 B = p 1 C = p 2 f + 1 = 3
82 77 81 sylan9eq f Walks G p f = 2 A = p 0 B = p 1 C = p 2 p = 3
83 eqcom A = p 0 p 0 = A
84 eqcom B = p 1 p 1 = B
85 eqcom C = p 2 p 2 = C
86 83 84 85 3anbi123i A = p 0 B = p 1 C = p 2 p 0 = A p 1 = B p 2 = C
87 86 biimpi A = p 0 B = p 1 C = p 2 p 0 = A p 1 = B p 2 = C
88 87 adantl f = 2 A = p 0 B = p 1 C = p 2 p 0 = A p 1 = B p 2 = C
89 88 adantl f Walks G p f = 2 A = p 0 B = p 1 C = p 2 p 0 = A p 1 = B p 2 = C
90 82 89 jca f Walks G p f = 2 A = p 0 B = p 1 C = p 2 p = 3 p 0 = A p 1 = B p 2 = C
91 1 wlkpwrd f Walks G p p Word V
92 80 eqeq2d f = 2 p = f + 1 p = 3
93 92 adantl p Word V f = 2 p = f + 1 p = 3
94 simp1 p Word V p = 3 A = p 0 B = p 1 C = p 2 p Word V
95 oveq2 p = 3 0 ..^ p = 0 ..^ 3
96 fzo0to3tp 0 ..^ 3 = 0 1 2
97 95 96 eqtrdi p = 3 0 ..^ p = 0 1 2
98 32 tpid1 0 0 1 2
99 eleq2 0 ..^ p = 0 1 2 0 0 ..^ p 0 0 1 2
100 98 99 mpbiri 0 ..^ p = 0 1 2 0 0 ..^ p
101 wrdsymbcl p Word V 0 0 ..^ p p 0 V
102 100 101 sylan2 p Word V 0 ..^ p = 0 1 2 p 0 V
103 40 tpid2 1 0 1 2
104 eleq2 0 ..^ p = 0 1 2 1 0 ..^ p 1 0 1 2
105 103 104 mpbiri 0 ..^ p = 0 1 2 1 0 ..^ p
106 wrdsymbcl p Word V 1 0 ..^ p p 1 V
107 105 106 sylan2 p Word V 0 ..^ p = 0 1 2 p 1 V
108 2ex 2 V
109 108 tpid3 2 0 1 2
110 eleq2 0 ..^ p = 0 1 2 2 0 ..^ p 2 0 1 2
111 109 110 mpbiri 0 ..^ p = 0 1 2 2 0 ..^ p
112 wrdsymbcl p Word V 2 0 ..^ p p 2 V
113 111 112 sylan2 p Word V 0 ..^ p = 0 1 2 p 2 V
114 102 107 113 3jca p Word V 0 ..^ p = 0 1 2 p 0 V p 1 V p 2 V
115 97 114 sylan2 p Word V p = 3 p 0 V p 1 V p 2 V
116 115 3adant3 p Word V p = 3 A = p 0 B = p 1 C = p 2 p 0 V p 1 V p 2 V
117 eleq1 A = p 0 A V p 0 V
118 117 3ad2ant1 A = p 0 B = p 1 C = p 2 A V p 0 V
119 eleq1 B = p 1 B V p 1 V
120 119 3ad2ant2 A = p 0 B = p 1 C = p 2 B V p 1 V
121 eleq1 C = p 2 C V p 2 V
122 121 3ad2ant3 A = p 0 B = p 1 C = p 2 C V p 2 V
123 118 120 122 3anbi123d A = p 0 B = p 1 C = p 2 A V B V C V p 0 V p 1 V p 2 V
124 123 3ad2ant3 p Word V p = 3 A = p 0 B = p 1 C = p 2 A V B V C V p 0 V p 1 V p 2 V
125 116 124 mpbird p Word V p = 3 A = p 0 B = p 1 C = p 2 A V B V C V
126 94 125 jca p Word V p = 3 A = p 0 B = p 1 C = p 2 p Word V A V B V C V
127 126 3exp p Word V p = 3 A = p 0 B = p 1 C = p 2 p Word V A V B V C V
128 127 adantr p Word V f = 2 p = 3 A = p 0 B = p 1 C = p 2 p Word V A V B V C V
129 93 128 sylbid p Word V f = 2 p = f + 1 A = p 0 B = p 1 C = p 2 p Word V A V B V C V
130 129 impancom p Word V p = f + 1 f = 2 A = p 0 B = p 1 C = p 2 p Word V A V B V C V
131 130 impd p Word V p = f + 1 f = 2 A = p 0 B = p 1 C = p 2 p Word V A V B V C V
132 91 77 131 syl2anc f Walks G p f = 2 A = p 0 B = p 1 C = p 2 p Word V A V B V C V
133 132 imp f Walks G p f = 2 A = p 0 B = p 1 C = p 2 p Word V A V B V C V
134 eqwrds3 p Word V A V B V C V p = ⟨“ ABC ”⟩ p = 3 p 0 = A p 1 = B p 2 = C
135 133 134 syl f Walks G p f = 2 A = p 0 B = p 1 C = p 2 p = ⟨“ ABC ”⟩ p = 3 p 0 = A p 1 = B p 2 = C
136 90 135 mpbird f Walks G p f = 2 A = p 0 B = p 1 C = p 2 p = ⟨“ ABC ”⟩
137 136 breq2d f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G p f Walks G ⟨“ ABC ”⟩
138 137 biimpd f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G p f Walks G ⟨“ ABC ”⟩
139 138 ex f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G p f Walks G ⟨“ ABC ”⟩
140 139 pm2.43a f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G ⟨“ ABC ”⟩
141 140 3impib f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G ⟨“ ABC ”⟩
142 141 adantl A V B V C V f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G ⟨“ ABC ”⟩
143 simpr2 A V B V C V f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f = 2
144 142 143 jca A V B V C V f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G ⟨“ ABC ”⟩ f = 2
145 144 ex A V B V C V f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G ⟨“ ABC ”⟩ f = 2
146 145 exlimdv A V B V C V p f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f Walks G ⟨“ ABC ”⟩ f = 2
147 146 eximdv A V B V C V f p f Walks G p f = 2 A = p 0 B = p 1 C = p 2 f f Walks G ⟨“ ABC ”⟩ f = 2
148 76 147 syl5com G UMGraph A B E B C E A V B V C V f f Walks G ⟨“ ABC ”⟩ f = 2
149 148 3expib G UMGraph A B E B C E A V B V C V f f Walks G ⟨“ ABC ”⟩ f = 2
150 149 com23 G UMGraph A V B V C V A B E B C E f f Walks G ⟨“ ABC ”⟩ f = 2
151 150 imp G UMGraph A V B V C V A B E B C E f f Walks G ⟨“ ABC ”⟩ f = 2
152 75 151 impbid G UMGraph A V B V C V f f Walks G ⟨“ ABC ”⟩ f = 2 A B E B C E
153 9 152 bitrd G UMGraph A V B V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C A B E B C E