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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion frrusgrord ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 frrusgrord0.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 rusgrrgr ⊢ ( 𝐺 RegUSGraph 𝐾 → 𝐺 RegGraph 𝐾 )
3 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
4 1 3 rgrprop ⊢ ( 𝐺 RegGraph 𝐾 → ( 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
5 2 4 syl ⊢ ( 𝐺 RegUSGraph 𝐾 → ( 𝐾 ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 ) )
6 5 simprd ⊢ ( 𝐺 RegUSGraph 𝐾 → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 )
7 1 frrusgrord0 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 𝐾 → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) )
8 6 7 syl5 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐺 RegUSGraph 𝐾 → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) )
9 8 3expb ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ) → ( 𝐺 RegUSGraph 𝐾 → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) )
10 9 expcom ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ FriendGraph → ( 𝐺 RegUSGraph 𝐾 → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) ) )
11 10 impd ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( 𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾 ) → ( ♯ ‘ 𝑉 ) = ( ( 𝐾 · ( 𝐾 − 1 ) ) + 1 ) ) )