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 ∖ x y ∉ G NeighbVtx x → 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 ∉ G NeighbVtx x → G NeighbVtx x ∈ V
4 eqid ⊢ Edg ⁡ G = Edg ⁡ G
5 eqid ⊢ G NeighbVtx x = G NeighbVtx x
6 eqid ⊢ G NeighbVtx y = G NeighbVtx y
7 simpl ⊢ x ∈ V ∧ y ∈ V ∖ x → x ∈ V
8 7 ad2antlr ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x ∧ y ∉ G NeighbVtx x → 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 ∉ G NeighbVtx x → 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 ∉ G NeighbVtx x → x ≠ y
20 simpr ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x ∧ y ∉ G NeighbVtx x → y ∉ G NeighbVtx x
21 simpl ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x → G ∈ FriendGraph
22 21 adantr ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x ∧ y ∉ G NeighbVtx x → G ∈ FriendGraph
23 eqid ⊢ a ∈ G NeighbVtx x ⟼ ι b ∈ G NeighbVtx y | a b ∈ Edg ⁡ G = a ∈ G NeighbVtx x ⟼ ι b ∈ G NeighbVtx y | a b ∈ Edg ⁡ G
24 1 4 5 6 8 11 19 20 22 23 frgrncvvdeqlem10 ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x ∧ y ∉ G NeighbVtx x → a ∈ G NeighbVtx x ⟼ ι b ∈ G NeighbVtx y | a b ∈ Edg ⁡ G : G NeighbVtx x ⟶ 1-1 onto G NeighbVtx y
25 3 24 hasheqf1od ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x ∧ y ∉ G NeighbVtx x → G NeighbVtx x = G NeighbVtx y
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 ∉ G NeighbVtx x → G ∈ USGraph ∧ x ∈ V
29 1 hashnbusgrvd ⊢ G ∈ USGraph ∧ x ∈ V → G NeighbVtx x = VtxDeg ⁡ G ⁡ x
30 28 29 syl ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x ∧ y ∉ G NeighbVtx x → G NeighbVtx x = 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 ∉ G NeighbVtx x → G ∈ USGraph ∧ y ∈ V
33 1 hashnbusgrvd ⊢ G ∈ USGraph ∧ y ∈ V → G NeighbVtx y = VtxDeg ⁡ G ⁡ y
34 32 33 syl ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x ∧ y ∉ G NeighbVtx x → G NeighbVtx y = VtxDeg ⁡ G ⁡ y
35 25 30 34 3eqtr3d ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x ∧ y ∉ G NeighbVtx x → 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 ∉ G NeighbVtx x → D ⁡ x = D ⁡ y
39 38 ex ⊢ G ∈ FriendGraph ∧ x ∈ V ∧ y ∈ V ∖ x → y ∉ G NeighbVtx x → D ⁡ x = D ⁡ y
40 39 ralrimivva ⊢ G ∈ FriendGraph → ∀ x ∈ V ∀ y ∈ V ∖ x y ∉ G NeighbVtx x → D ⁡ x = D ⁡ y