Metamath Proof Explorer

Theorem frrusgrord

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.". Variant of frrusgrord0 , using the definition RegUSGraph ( df-rusgr ). (Contributed by Alexander van der Vekens, 25-Aug-2018) (Revised by AV, 26-May-2021) (Proof shortened by AV, 12-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 frrusgrord0.v ⊢ V = Vtx ⁡ G
2 rusgrrgr ⊢ G RegUSGraph K → G RegGraph K
3 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
4 1 3 rgrprop ⊢ G RegGraph K → K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K
5 2 4 syl ⊢ G RegUSGraph K → K ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K
6 5 simprd ⊢ G RegUSGraph K → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K
7 1 frrusgrord0 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = K → V = K ⁢ K − 1 + 1
8 6 7 syl5 ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G RegUSGraph K → V = K ⁢ K − 1 + 1
9 8 3expb ⊢ G ∈ FriendGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G RegUSGraph K → V = K ⁢ K − 1 + 1
10 9 expcom ⊢ V ∈ Fin ∧ V ≠ ∅ → G ∈ FriendGraph → G RegUSGraph K → V = K ⁢ K − 1 + 1
11 10 impd ⊢ V ∈ Fin ∧ V ≠ ∅ → G ∈ FriendGraph ∧ G RegUSGraph K → V = K ⁢ K − 1 + 1