Metamath Proof Explorer

Theorem frgr2wwlkeqm

Description: If there is a (simple) path of length 2 from one vertex to another vertex and a (simple) path of length 2 from the other vertex back to the first vertex in a friendship graph, then the middle vertex is the same. This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 20-Feb-2018) (Revised by AV, 13-May-2021) (Proof shortened by AV, 7-Jan-2022)

Ref Expression
Assertion frgr2wwlkeqm ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → Q = P

Proof

Step Hyp Ref Expression
1 simp3l ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → P ∈ X
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 2 wwlks2onv ⊢ P ∈ X ∧ ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
4 1 3 sylan ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
5 simp3r ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → Q ∈ Y
6 2 wwlks2onv ⊢ Q ∈ Y ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → B ∈ Vtx ⁡ G ∧ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G
7 5 6 sylan ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → B ∈ Vtx ⁡ G ∧ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G
8 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
9 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
10 8 9 syl ⊢ G ∈ FriendGraph → G ∈ UMGraph
11 10 3ad2ant1 ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → G ∈ UMGraph
12 simpr3 ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → B ∈ Vtx ⁡ G
13 simpl ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → Q ∈ Vtx ⁡ G
14 simpr1 ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G
15 12 13 14 3jca ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → B ∈ Vtx ⁡ G ∧ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G
16 2 wwlks2onsym ⊢ G ∈ UMGraph ∧ B ∈ Vtx ⁡ G ∧ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G → ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A ↔ ⟨“ AQB ”⟩ ∈ A 2 WWalksNOn G B
17 11 15 16 syl2anr ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A ↔ ⟨“ AQB ”⟩ ∈ A 2 WWalksNOn G B
18 simpr1 ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → G ∈ FriendGraph
19 3simpb ⊢ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
20 19 ad2antlr ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G
21 simpr2 ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → A ≠ B
22 2 frgr2wwlkeu ⊢ G ∈ FriendGraph ∧ A ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ A ≠ B → ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B
23 18 20 21 22 syl3anc ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B
24 s3eq2 ⊢ x = Q → ⟨“ AxB ”⟩ = ⟨“ AQB ”⟩
25 24 eleq1d ⊢ x = Q → ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B ↔ ⟨“ AQB ”⟩ ∈ A 2 WWalksNOn G B
26 25 riota2 ⊢ Q ∈ Vtx ⁡ G ∧ ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ AQB ”⟩ ∈ A 2 WWalksNOn G B ↔ ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = Q
27 26 ad4ant14 ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ AQB ”⟩ ∈ A 2 WWalksNOn G B ↔ ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = Q
28 simplr2 ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → P ∈ Vtx ⁡ G
29 s3eq2 ⊢ x = P → ⟨“ AxB ”⟩ = ⟨“ APB ”⟩
30 29 eleq1d ⊢ x = P → ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B ↔ ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B
31 30 riota2 ⊢ P ∈ Vtx ⁡ G ∧ ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B ↔ ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = P
32 28 31 sylan ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B ↔ ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = P
33 eqtr2 ⊢ ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = Q ∧ ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = P → Q = P
34 33 expcom ⊢ ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = P → ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = Q → Q = P
35 32 34 biimtrdi ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = Q → Q = P
36 35 com23 ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B → ι x ∈ Vtx ⁡ G | ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B = Q → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
37 27 36 sylbid ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ∃! x ∈ Vtx ⁡ G ⟨“ AxB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ AQB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
38 23 37 mpdan ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → ⟨“ AQB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
39 17 38 sylbid ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G ∧ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
40 39 expimpd ⊢ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
41 40 ex ⊢ Q ∈ Vtx ⁡ G → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
42 41 com23 ⊢ Q ∈ Vtx ⁡ G → G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
43 42 3ad2ant2 ⊢ B ∈ Vtx ⁡ G ∧ Q ∈ Vtx ⁡ G ∧ A ∈ Vtx ⁡ G → G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
44 7 43 mpcom ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
45 44 ex ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → Q = P
46 45 com24 ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → Q = P
47 46 imp ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → A ∈ Vtx ⁡ G ∧ P ∈ Vtx ⁡ G ∧ B ∈ Vtx ⁡ G → ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → Q = P
48 4 47 mpd ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y ∧ ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B → ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → Q = P
49 48 expimpd ⊢ G ∈ FriendGraph ∧ A ≠ B ∧ P ∈ X ∧ Q ∈ Y → ⟨“ APB ”⟩ ∈ A 2 WWalksNOn G B ∧ ⟨“ BQA ”⟩ ∈ B 2 WWalksNOn G A → Q = P