frgr2wwlk1

Description: In a friendship graph, there is exactly one walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018) (Revised by AV, 13-May-2021) (Proof shortened by AV, 16-Mar-2022)

		Ref	Expression
	Hypothesis	frgr2wwlkeu.v	$⊢ V = Vtx (G)$
	Assertion	frgr2wwlk1	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \|A (2 WWalksNOn G) B\| = 1$

Proof

Step	Hyp	Ref	Expression
1		frgr2wwlkeu.v	$⊢ V = Vtx (G)$
2	1	frgr2wwlkn0	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to A (2 WWalksNOn G) B \neq \emptyset$
3	1	elwwlks2ons3	$⊢ w \in (A (2 WWalksNOn G) B) \leftrightarrow \exists d \in V (w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B))$
4	1	elwwlks2ons3	$⊢ t \in (A (2 WWalksNOn G) B) \leftrightarrow \exists c \in V (t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B))$
5	3 4	anbi12i	$⊢ (w \in (A (2 WWalksNOn G) B) \land t \in (A (2 WWalksNOn G) B)) \leftrightarrow (\exists d \in V (w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \land \exists c \in V (t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)))$
6	1	frgr2wwlkeu	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \exists! x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B)$
7		s3eq2	$⊢ x = y \to ⟨“ A x B ”⟩ = ⟨“ A y B ”⟩$
8	7	eleq1d	$⊢ x = y \to (⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \leftrightarrow ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B))$
9	8	reu4	$⊢ \exists! x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \leftrightarrow (\exists x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land \forall x \in V \forall y \in V ((⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \to x = y))$
10		s3eq2	$⊢ x = d \to ⟨“ A x B ”⟩ = ⟨“ A d B ”⟩$
11	10	eleq1d	$⊢ x = d \to (⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \leftrightarrow ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B))$
12	11	anbi1d	$⊢ x = d \to ((⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \leftrightarrow (⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)))$
13		equequ1	$⊢ x = d \to (x = y \leftrightarrow d = y)$
14	12 13	imbi12d	$⊢ x = d \to (((⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \to x = y) \leftrightarrow ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = y))$
15		s3eq2	$⊢ y = c \to ⟨“ A y B ”⟩ = ⟨“ A c B ”⟩$
16	15	eleq1d	$⊢ y = c \to (⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B) \leftrightarrow ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B))$
17	16	anbi2d	$⊢ y = c \to ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \leftrightarrow (⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)))$
18		equequ2	$⊢ y = c \to (d = y \leftrightarrow d = c)$
19	17 18	imbi12d	$⊢ y = c \to (((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = y) \leftrightarrow ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c))$
20	14 19	rspc2va	$⊢ ((d \in V \land c \in V) \land \forall x \in V \forall y \in V ((⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \to x = y)) \to ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c)$
21		pm3.35	$⊢ ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \land ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c)) \to d = c$
22		s3eq2	$⊢ c = d \to ⟨“ A c B ”⟩ = ⟨“ A d B ”⟩$
23	22	equcoms	$⊢ d = c \to ⟨“ A c B ”⟩ = ⟨“ A d B ”⟩$
24	23	adantr	$⊢ (d = c \land (t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩)) \to ⟨“ A c B ”⟩ = ⟨“ A d B ”⟩$
25		eqeq12	$⊢ (t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩) \to (t = w \leftrightarrow ⟨“ A c B ”⟩ = ⟨“ A d B ”⟩)$
26	25	adantl	$⊢ (d = c \land (t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩)) \to (t = w \leftrightarrow ⟨“ A c B ”⟩ = ⟨“ A d B ”⟩)$
27	24 26	mpbird	$⊢ (d = c \land (t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩)) \to t = w$
28	27	equcomd	$⊢ (d = c \land (t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩)) \to w = t$
29	28	ex	$⊢ d = c \to ((t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩) \to w = t)$
30	21 29	syl	$⊢ ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \land ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c)) \to ((t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩) \to w = t)$
31	30	ex	$⊢ (⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to (((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c) \to ((t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩) \to w = t))$
32	31	com23	$⊢ (⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to ((t = ⟨“ A c B ”⟩ \land w = ⟨“ A d B ”⟩) \to (((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c) \to w = t))$
33	32	exp4b	$⊢ ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \to (⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B) \to (t = ⟨“ A c B ”⟩ \to (w = ⟨“ A d B ”⟩ \to (((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c) \to w = t))))$
34	33	com13	$⊢ t = ⟨“ A c B ”⟩ \to (⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B) \to (⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \to (w = ⟨“ A d B ”⟩ \to (((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c) \to w = t))))$
35	34	imp	$⊢ (t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to (⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \to (w = ⟨“ A d B ”⟩ \to (((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c) \to w = t)))$
36	35	com13	$⊢ w = ⟨“ A d B ”⟩ \to (⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \to ((t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to (((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c) \to w = t)))$
37	36	imp	$⊢ (w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to ((t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to (((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c) \to w = t))$
38	37	com13	$⊢ ((⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to d = c) \to ((t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to ((w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to w = t))$
39	20 38	syl	$⊢ ((d \in V \land c \in V) \land \forall x \in V \forall y \in V ((⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \to x = y)) \to ((t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to ((w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to w = t))$
40	39	expcom	$⊢ \forall x \in V \forall y \in V ((⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land ⟨“ A y B ”⟩ \in (A (2 WWalksNOn G) B)) \to x = y) \to ((d \in V \land c \in V) \to ((t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to ((w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to w = t)))$
41	9 40	simplbiim	$⊢ \exists! x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \to ((d \in V \land c \in V) \to ((t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to ((w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to w = t)))$
42	41	impl	$⊢ ((\exists! x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land d \in V) \land c \in V) \to ((t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to ((w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to w = t))$
43	42	rexlimdva	$⊢ (\exists! x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land d \in V) \to (\exists c \in V (t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to ((w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to w = t))$
44	43	com23	$⊢ (\exists! x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \land d \in V) \to ((w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to (\exists c \in V (t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to w = t))$
45	44	rexlimdva	$⊢ \exists! x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \to (\exists d \in V (w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \to (\exists c \in V (t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B)) \to w = t))$
46	45	impd	$⊢ \exists! x \in V ⟨“ A x B ”⟩ \in (A (2 WWalksNOn G) B) \to ((\exists d \in V (w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \land \exists c \in V (t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B))) \to w = t)$
47	6 46	syl	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to ((\exists d \in V (w = ⟨“ A d B ”⟩ \land ⟨“ A d B ”⟩ \in (A (2 WWalksNOn G) B)) \land \exists c \in V (t = ⟨“ A c B ”⟩ \land ⟨“ A c B ”⟩ \in (A (2 WWalksNOn G) B))) \to w = t)$
48	5 47	biimtrid	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to ((w \in (A (2 WWalksNOn G) B) \land t \in (A (2 WWalksNOn G) B)) \to w = t)$
49	48	alrimivv	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \forall w \forall t ((w \in (A (2 WWalksNOn G) B) \land t \in (A (2 WWalksNOn G) B)) \to w = t)$
50		eqeuel	$⊢ (A (2 WWalksNOn G) B \neq \emptyset \land \forall w \forall t ((w \in (A (2 WWalksNOn G) B) \land t \in (A (2 WWalksNOn G) B)) \to w = t)) \to \exists! w w \in (A (2 WWalksNOn G) B)$
51	2 49 50	syl2anc	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \exists! w w \in (A (2 WWalksNOn G) B)$
52		ovex	$⊢ A (2 WWalksNOn G) B \in V$
53		euhash1	$⊢ A (2 WWalksNOn G) B \in V \to (\|A (2 WWalksNOn G) B\| = 1 \leftrightarrow \exists! w w \in (A (2 WWalksNOn G) B))$
54	52 53	mp1i	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to (\|A (2 WWalksNOn G) B\| = 1 \leftrightarrow \exists! w w \in (A (2 WWalksNOn G) B))$
55	51 54	mpbird	$⊢ (G \in FriendGraph \land (A \in V \land B \in V) \land A \neq B) \to \|A (2 WWalksNOn G) B\| = 1$

Metamath Proof Explorer

Theorem frgr2wwlk1

Proof