Metamath Proof Explorer

Theorem 3wlkond

Description: A walk of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021) (Revised by AV, 24-Mar-2021)

Ref Expression
Hypotheses 3wlkd.p ⊢P=⟨“ABCD”⟩
3wlkd.f ⊢F=⟨“JKL”⟩
3wlkd.s ⊢φ→A∈V∧B∈V∧C∈V∧D∈V
3wlkd.n ⊢φ→A≠B∧A≠C∧B≠C∧B≠D∧C≠D
3wlkd.e ⊢φ→AB⊆I⁡J∧BC⊆I⁡K∧CD⊆I⁡L
3wlkd.v ⊢V=Vtx⁡G
3wlkd.i ⊢I=iEdg⁡G
Assertion 3wlkond ⊢φ→FAWalksOn⁡GDP

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢P=⟨“ABCD”⟩
2 3wlkd.f ⊢F=⟨“JKL”⟩
3 3wlkd.s ⊢φ→A∈V∧B∈V∧C∈V∧D∈V
4 3wlkd.n ⊢φ→A≠B∧A≠C∧B≠C∧B≠D∧C≠D
5 3wlkd.e ⊢φ→AB⊆I⁡J∧BC⊆I⁡K∧CD⊆I⁡L
6 3wlkd.v ⊢V=Vtx⁡G
7 3wlkd.i ⊢I=iEdg⁡G
8 1 2 3 4 5 6 7 3wlkd ⊢φ→FWalks⁡GP
9 8 wlkonwlk1l ⊢φ→FP⁡0WalksOn⁡GlastS⁡PP
10 1 2 3 3wlkdlem3 ⊢φ→P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D
11 simpll ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→P⁡0=A
12 11 eqcomd ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→A=P⁡0
13 10 12 syl ⊢φ→A=P⁡0
14 1 fveq2i ⊢lastS⁡P=lastS⁡⟨“ABCD”⟩
15 fvex ⊢P⁡3∈V
16 eleq1 ⊢P⁡3=D→P⁡3∈V↔D∈V
17 15 16 mpbii ⊢P⁡3=D→D∈V
18 lsws4 ⊢D∈V→lastS⁡⟨“ABCD”⟩=D
19 17 18 syl ⊢P⁡3=D→lastS⁡⟨“ABCD”⟩=D
20 14 19 eqtr2id ⊢P⁡3=D→D=lastS⁡P
21 20 ad2antll ⊢P⁡0=A∧P⁡1=B∧P⁡2=C∧P⁡3=D→D=lastS⁡P
22 10 21 syl ⊢φ→D=lastS⁡P
23 13 22 oveq12d ⊢φ→AWalksOn⁡GD=P⁡0WalksOn⁡GlastS⁡P
24 23 breqd ⊢φ→FAWalksOn⁡GDP↔FP⁡0WalksOn⁡GlastS⁡PP
25 9 24 mpbird ⊢φ→FAWalksOn⁡GDP