Metamath Proof Explorer

Theorem frrusgrord0

Description: If a nonempty finite friendship graph is k-regular, its order is k(k-1)+1. This corresponds to claim 3 in Huneke p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". (Contributed by Alexander van der Vekens, 11-Mar-2018) (Revised by AV, 26-May-2021) (Proof shortened by AV, 12-Jan-2022)

Ref Expression
Hypothesis frrusgrord0.v ⊢ V = Vtx ⁡ G
Assertion frrusgrord0 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V = K ⁢ K − 1 + 1

Proof

Step Hyp Ref Expression
1 frrusgrord0.v ⊢ V = Vtx ⁡ G
2 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
3 2 anim1i ⊢ G ∈ FriendGraph ∧ V ∈ Fin → G ∈ USGraph ∧ V ∈ Fin
4 1 isfusgr ⊢ G ∈ FinUSGraph ↔ G ∈ USGraph ∧ V ∈ Fin
5 3 4 sylibr ⊢ G ∈ FriendGraph ∧ V ∈ Fin → G ∈ FinUSGraph
6 1 fusgreghash2wsp ⊢ G ∈ FinUSGraph ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → 2 WSPathsN G = V ⁢ K ⁢ K − 1
7 5 6 stoic3 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → 2 WSPathsN G = V ⁢ K ⁢ K − 1
8 7 imp ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → 2 WSPathsN G = V ⁢ K ⁢ K − 1
9 1 frgrhash2wsp ⊢ G ∈ FriendGraph ∧ V ∈ Fin → 2 WSPathsN G = V ⁢ V − 1
10 9 eqcomd ⊢ G ∈ FriendGraph ∧ V ∈ Fin → V ⁢ V − 1 = 2 WSPathsN G
11 10 eqeq1d ⊢ G ∈ FriendGraph ∧ V ∈ Fin → V ⁢ V − 1 = V ⁢ K ⁢ K − 1 ↔ 2 WSPathsN G = V ⁢ K ⁢ K − 1
12 11 3adant3 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → V ⁢ V − 1 = V ⁢ K ⁢ K − 1 ↔ 2 WSPathsN G = V ⁢ K ⁢ K − 1
13 12 adantr ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V ⁢ V − 1 = V ⁢ K ⁢ K − 1 ↔ 2 WSPathsN G = V ⁢ K ⁢ K − 1
14 1 frrusgrord0lem ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0
15 peano2cnm ⊢ V ∈ ℂ → V − 1 ∈ ℂ
16 15 3ad2ant2 ⊢ K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0 → V − 1 ∈ ℂ
17 kcnktkm1cn ⊢ K ∈ ℂ → K ⁢ K − 1 ∈ ℂ
18 17 3ad2ant1 ⊢ K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0 → K ⁢ K − 1 ∈ ℂ
19 simp2 ⊢ K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0 → V ∈ ℂ
20 simp3 ⊢ K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0 → V ≠ 0
21 16 18 19 20 mulcand ⊢ K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0 → V ⁢ V − 1 = V ⁢ K ⁢ K − 1 ↔ V − 1 = K ⁢ K − 1
22 npcan1 ⊢ V ∈ ℂ → V - 1 + 1 = V
23 oveq1 ⊢ V − 1 = K ⁢ K − 1 → V - 1 + 1 = K ⁢ K − 1 + 1
24 22 23 sylan9req ⊢ V ∈ ℂ ∧ V − 1 = K ⁢ K − 1 → V = K ⁢ K − 1 + 1
25 24 ex ⊢ V ∈ ℂ → V − 1 = K ⁢ K − 1 → V = K ⁢ K − 1 + 1
26 25 3ad2ant2 ⊢ K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0 → V − 1 = K ⁢ K − 1 → V = K ⁢ K − 1 + 1
27 21 26 sylbid ⊢ K ∈ ℂ ∧ V ∈ ℂ ∧ V ≠ 0 → V ⁢ V − 1 = V ⁢ K ⁢ K − 1 → V = K ⁢ K − 1 + 1
28 14 27 syl ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V ⁢ V − 1 = V ⁢ K ⁢ K − 1 → V = K ⁢ K − 1 + 1
29 13 28 sylbird ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → 2 WSPathsN G = V ⁢ K ⁢ K − 1 → V = K ⁢ K − 1 + 1
30 8 29 mpd ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V = K ⁢ K − 1 + 1
31 30 ex ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V = K ⁢ K − 1 + 1