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 \in FriendGraph \land A \neq B \land (P \in X \land Q \in Y)) \to ((⟨“ A P B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ B Q A ”⟩ \in (B (2 WWalksNOn G) A)) \to Q = P)$

Proof

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

Metamath Proof Explorer

Theorem frgr2wwlkeqm

Proof