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

Proof

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