Metamath Proof Explorer


Theorem elwwlks2ons3

Description: For each walk of length 2 between two vertices, there is a third vertex in the middle of the walk. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlks2onv.v V = Vtx G
Assertion elwwlks2ons3 W A 2 WWalksNOn G C b V W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C

Proof

Step Hyp Ref Expression
1 wwlks2onv.v V = Vtx G
2 id W A 2 WWalksNOn G C W A 2 WWalksNOn G C
3 1 elwwlks2ons3im W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V
4 anass W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V
5 2 3 4 sylanbrc W A 2 WWalksNOn G C W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V
6 simpr W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V W 1 V
7 s3eq2 b = W 1 ⟨“ AbC ”⟩ = ⟨“ A W 1 C ”⟩
8 eqeq2 ⟨“ AbC ”⟩ = ⟨“ A W 1 C ”⟩ W = ⟨“ AbC ”⟩ W = ⟨“ A W 1 C ”⟩
9 eleq1 ⟨“ AbC ”⟩ = ⟨“ A W 1 C ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C ⟨“ A W 1 C ”⟩ A 2 WWalksNOn G C
10 8 9 anbi12d ⟨“ AbC ”⟩ = ⟨“ A W 1 C ”⟩ W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ ⟨“ A W 1 C ”⟩ A 2 WWalksNOn G C
11 7 10 syl b = W 1 W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ ⟨“ A W 1 C ”⟩ A 2 WWalksNOn G C
12 11 adantl W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V b = W 1 W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ ⟨“ A W 1 C ”⟩ A 2 WWalksNOn G C
13 simpr W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W = ⟨“ A W 1 C ”⟩
14 eleq1 W = ⟨“ A W 1 C ”⟩ W A 2 WWalksNOn G C ⟨“ A W 1 C ”⟩ A 2 WWalksNOn G C
15 14 biimpac W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ ⟨“ A W 1 C ”⟩ A 2 WWalksNOn G C
16 13 15 jca W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W = ⟨“ A W 1 C ”⟩ ⟨“ A W 1 C ”⟩ A 2 WWalksNOn G C
17 16 adantr W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V W = ⟨“ A W 1 C ”⟩ ⟨“ A W 1 C ”⟩ A 2 WWalksNOn G C
18 6 12 17 rspcedvd W A 2 WWalksNOn G C W = ⟨“ A W 1 C ”⟩ W 1 V b V W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C
19 5 18 syl W A 2 WWalksNOn G C b V W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C
20 eleq1 ⟨“ AbC ”⟩ = W ⟨“ AbC ”⟩ A 2 WWalksNOn G C W A 2 WWalksNOn G C
21 20 eqcoms W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C W A 2 WWalksNOn G C
22 21 biimpa W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C W A 2 WWalksNOn G C
23 22 rexlimivw b V W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C W A 2 WWalksNOn G C
24 19 23 impbii W A 2 WWalksNOn G C b V W = ⟨“ AbC ”⟩ ⟨“ AbC ”⟩ A 2 WWalksNOn G C