Metamath Proof Explorer

Theorem umgr2adedgwlkonALT

Description: Alternate proof for umgr2adedgwlkon , using umgr2adedgwlk , but with a much longer proof! In a multigraph, two adjacent edges form a walk between two (different) vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018) (Revised by AV, 30-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses umgr2adedgwlk.e ⊢ E = Edg ⁡ G
umgr2adedgwlk.i ⊢ I = iEdg ⁡ G
umgr2adedgwlk.f ⊢ F = ⟨“ JK ”⟩
umgr2adedgwlk.p ⊢ P = ⟨“ ABC ”⟩
umgr2adedgwlk.g ⊢ φ → G ∈ UMGraph
umgr2adedgwlk.a ⊢ φ → A B ∈ E ∧ B C ∈ E
umgr2adedgwlk.j ⊢ φ → I ⁡ J = A B
umgr2adedgwlk.k ⊢ φ → I ⁡ K = B C
Assertion umgr2adedgwlkonALT ⊢ φ → F A WalksOn ⁡ G C P

Proof

Step Hyp Ref Expression
1 umgr2adedgwlk.e ⊢ E = Edg ⁡ G
2 umgr2adedgwlk.i ⊢ I = iEdg ⁡ G
3 umgr2adedgwlk.f ⊢ F = ⟨“ JK ”⟩
4 umgr2adedgwlk.p ⊢ P = ⟨“ ABC ”⟩
5 umgr2adedgwlk.g ⊢ φ → G ∈ UMGraph
6 umgr2adedgwlk.a ⊢ φ → A B ∈ E ∧ B C ∈ E
7 umgr2adedgwlk.j ⊢ φ → I ⁡ J = A B
8 umgr2adedgwlk.k ⊢ φ → I ⁡ K = B C
9 1 2 3 4 5 6 7 8 umgr2adedgwlk ⊢ φ → F Walks ⁡ G P ∧ F = 2 ∧ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2
10 simp1 ⊢ F Walks ⁡ G P ∧ F = 2 ∧ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 → F Walks ⁡ G P
11 id ⊢ P ⁡ 0 = A → P ⁡ 0 = A
12 11 eqcoms ⊢ A = P ⁡ 0 → P ⁡ 0 = A
13 12 3ad2ant1 ⊢ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 → P ⁡ 0 = A
14 13 3ad2ant3 ⊢ F Walks ⁡ G P ∧ F = 2 ∧ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 → P ⁡ 0 = A
15 fveq2 ⊢ 2 = F → P ⁡ 2 = P ⁡ F
16 15 eqcoms ⊢ F = 2 → P ⁡ 2 = P ⁡ F
17 16 eqeq1d ⊢ F = 2 → P ⁡ 2 = C ↔ P ⁡ F = C
18 17 biimpcd ⊢ P ⁡ 2 = C → F = 2 → P ⁡ F = C
19 18 eqcoms ⊢ C = P ⁡ 2 → F = 2 → P ⁡ F = C
20 19 3ad2ant3 ⊢ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 → F = 2 → P ⁡ F = C
21 20 com12 ⊢ F = 2 → A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 → P ⁡ F = C
22 21 a1i ⊢ F Walks ⁡ G P → F = 2 → A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 → P ⁡ F = C
23 22 3imp ⊢ F Walks ⁡ G P ∧ F = 2 ∧ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 → P ⁡ F = C
24 10 14 23 3jca ⊢ F Walks ⁡ G P ∧ F = 2 ∧ A = P ⁡ 0 ∧ B = P ⁡ 1 ∧ C = P ⁡ 2 → F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = C
25 9 24 syl ⊢ φ → F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = C
26 3anass ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E ↔ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E
27 5 6 26 sylanbrc ⊢ φ → G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E
28 1 umgr2adedgwlklem ⊢ G ∈ UMGraph ∧ A B ∈ E ∧ B C ∈ E → A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
29 3simpb ⊢ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
30 29 adantl ⊢ A ≠ B ∧ B ≠ C ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
31 27 28 30 3syl ⊢ φ → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
32 3anass ⊢ G ∈ UMGraph ∧ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G ↔ G ∈ UMGraph ∧ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
33 5 31 32 sylanbrc ⊢ φ → G ∈ UMGraph ∧ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
34 s2cli ⊢ ⟨“ JK ”⟩ ∈ Word V
35 3 34 eqeltri ⊢ F ∈ Word V
36 s3cli ⊢ ⟨“ ABC ”⟩ ∈ Word V
37 4 36 eqeltri ⊢ P ∈ Word V
38 35 37 pm3.2i ⊢ F ∈ Word V ∧ P ∈ Word V
39 id ⊢ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
40 39 3adant1 ⊢ G ∈ UMGraph ∧ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
41 40 anim1i ⊢ G ∈ UMGraph ∧ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G ∧ F ∈ Word V ∧ P ∈ Word V → A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G ∧ F ∈ Word V ∧ P ∈ Word V
42 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
43 42 iswlkon ⊢ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G ∧ F ∈ Word V ∧ P ∈ Word V → F A WalksOn ⁡ G C P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = C
44 41 43 syl ⊢ G ∈ UMGraph ∧ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G ∧ F ∈ Word V ∧ P ∈ Word V → F A WalksOn ⁡ G C P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = C
45 33 38 44 sylancl ⊢ φ → F A WalksOn ⁡ G C P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = C
46 25 45 mpbird ⊢ φ → F A WalksOn ⁡ G C P