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 ) ) )