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 e. FriendGraph /\ A =/= B /\ ( P e. X /\ Q e. Y ) ) -> ( ( <" A P B "> e. ( A ( 2 WWalksNOn G ) B ) /\ <" B Q A "> e. ( B ( 2 WWalksNOn G ) A ) ) -> Q = P ) )

Proof

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