Metamath Proof Explorer

Theorem frgrncvvdeq

Description: In a friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to claim 1 in Huneke p. 1: "If x,y are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 10-May-2021)

Ref Expression
Hypotheses frgrncvvdeq.v ⊢V=Vtx⁡G
frgrncvvdeq.d ⊢D=VtxDeg⁡G
Assertion frgrncvvdeq ⊢G∈FriendGraph→∀x∈V∀y∈V∖xy∉GNeighbVtxx→D⁡x=D⁡y

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v ⊢V=Vtx⁡G
2 frgrncvvdeq.d ⊢D=VtxDeg⁡G
3 ovexd ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→GNeighbVtxx∈V
4 eqid ⊢Edg⁡G=Edg⁡G
5 eqid ⊢GNeighbVtxx=GNeighbVtxx
6 eqid ⊢GNeighbVtxy=GNeighbVtxy
7 simpl ⊢x∈V∧y∈V∖x→x∈V
8 7 ad2antlr ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→x∈V
9 eldifi ⊢y∈V∖x→y∈V
10 9 adantl ⊢x∈V∧y∈V∖x→y∈V
11 10 ad2antlr ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→y∈V
12 eldif ⊢y∈V∖x↔y∈V∧¬y∈x
13 velsn ⊢y∈x↔y=x
14 13 biimpri ⊢y=x→y∈x
15 14 equcoms ⊢x=y→y∈x
16 15 necon3bi ⊢¬y∈x→x≠y
17 12 16 simplbiim ⊢y∈V∖x→x≠y
18 17 adantl ⊢x∈V∧y∈V∖x→x≠y
19 18 ad2antlr ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→x≠y
20 simpr ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→y∉GNeighbVtxx
21 simpl ⊢G∈FriendGraph∧x∈V∧y∈V∖x→G∈FriendGraph
22 21 adantr ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→G∈FriendGraph
23 eqid ⊢a∈GNeighbVtxx⟼ιb∈GNeighbVtxy|ab∈Edg⁡G=a∈GNeighbVtxx⟼ιb∈GNeighbVtxy|ab∈Edg⁡G
24 1 4 5 6 8 11 19 20 22 23 frgrncvvdeqlem10 ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→a∈GNeighbVtxx⟼ιb∈GNeighbVtxy|ab∈Edg⁡G:GNeighbVtxx⟶1-1 ontoGNeighbVtxy
25 3 24 hasheqf1od ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→GNeighbVtxx=GNeighbVtxy
26 frgrusgr ⊢G∈FriendGraph→G∈USGraph
27 26 7 anim12i ⊢G∈FriendGraph∧x∈V∧y∈V∖x→G∈USGraph∧x∈V
28 27 adantr ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→G∈USGraph∧x∈V
29 1 hashnbusgrvd ⊢G∈USGraph∧x∈V→GNeighbVtxx=VtxDeg⁡G⁡x
30 28 29 syl ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→GNeighbVtxx=VtxDeg⁡G⁡x
31 26 10 anim12i ⊢G∈FriendGraph∧x∈V∧y∈V∖x→G∈USGraph∧y∈V
32 31 adantr ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→G∈USGraph∧y∈V
33 1 hashnbusgrvd ⊢G∈USGraph∧y∈V→GNeighbVtxy=VtxDeg⁡G⁡y
34 32 33 syl ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→GNeighbVtxy=VtxDeg⁡G⁡y
35 25 30 34 3eqtr3d ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→VtxDeg⁡G⁡x=VtxDeg⁡G⁡y
36 2 fveq1i ⊢D⁡x=VtxDeg⁡G⁡x
37 2 fveq1i ⊢D⁡y=VtxDeg⁡G⁡y
38 35 36 37 3eqtr4g ⊢G∈FriendGraph∧x∈V∧y∈V∖x∧y∉GNeighbVtxx→D⁡x=D⁡y
39 38 ex ⊢G∈FriendGraph∧x∈V∧y∈V∖x→y∉GNeighbVtxx→D⁡x=D⁡y
40 39 ralrimivva ⊢G∈FriendGraph→∀x∈V∀y∈V∖xy∉GNeighbVtxx→D⁡x=D⁡y