Metamath Proof Explorer


Theorem s3wwlks2on

Description: A length 3 string which represents a walk of length 2 between two vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021)

Ref Expression
Hypothesis s3wwlks2on.v V = Vtx G
Assertion s3wwlks2on G UPGraph A V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C f f Walks G ⟨“ ABC ”⟩ f = 2

Proof

Step Hyp Ref Expression
1 s3wwlks2on.v V = Vtx G
2 wwlknon ⟨“ ABC ”⟩ A 2 WWalksNOn G C ⟨“ ABC ”⟩ 2 WWalksN G ⟨“ ABC ”⟩ 0 = A ⟨“ ABC ”⟩ 2 = C
3 2 a1i G UPGraph A V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C ⟨“ ABC ”⟩ 2 WWalksN G ⟨“ ABC ”⟩ 0 = A ⟨“ ABC ”⟩ 2 = C
4 3anass ⟨“ ABC ”⟩ 2 WWalksN G ⟨“ ABC ”⟩ 0 = A ⟨“ ABC ”⟩ 2 = C ⟨“ ABC ”⟩ 2 WWalksN G ⟨“ ABC ”⟩ 0 = A ⟨“ ABC ”⟩ 2 = C
5 s3fv0 A V ⟨“ ABC ”⟩ 0 = A
6 s3fv2 C V ⟨“ ABC ”⟩ 2 = C
7 5 6 anim12i A V C V ⟨“ ABC ”⟩ 0 = A ⟨“ ABC ”⟩ 2 = C
8 7 3adant1 G UPGraph A V C V ⟨“ ABC ”⟩ 0 = A ⟨“ ABC ”⟩ 2 = C
9 8 biantrud G UPGraph A V C V ⟨“ ABC ”⟩ 2 WWalksN G ⟨“ ABC ”⟩ 2 WWalksN G ⟨“ ABC ”⟩ 0 = A ⟨“ ABC ”⟩ 2 = C
10 4 9 bitr4id G UPGraph A V C V ⟨“ ABC ”⟩ 2 WWalksN G ⟨“ ABC ”⟩ 0 = A ⟨“ ABC ”⟩ 2 = C ⟨“ ABC ”⟩ 2 WWalksN G
11 wlklnwwlknupgr G UPGraph f f Walks G ⟨“ ABC ”⟩ f = 2 ⟨“ ABC ”⟩ 2 WWalksN G
12 11 bicomd G UPGraph ⟨“ ABC ”⟩ 2 WWalksN G f f Walks G ⟨“ ABC ”⟩ f = 2
13 12 3ad2ant1 G UPGraph A V C V ⟨“ ABC ”⟩ 2 WWalksN G f f Walks G ⟨“ ABC ”⟩ f = 2
14 3 10 13 3bitrd G UPGraph A V C V ⟨“ ABC ”⟩ A 2 WWalksNOn G C f f Walks G ⟨“ ABC ”⟩ f = 2