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 e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 frrusgrord0.v 
 |-  V = ( Vtx ` G )
2 frgrusgr 
 |-  ( G e. FriendGraph -> G e. USGraph )
3 2 anim1i 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( G e. USGraph /\ V e. Fin ) )
4 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
5 3 4 sylibr 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> G e. FinUSGraph )
6 1 fusgreghash2wsp 
 |-  ( ( G e. FinUSGraph /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) ) )
7 5 6 stoic3 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) ) )
8 7 imp 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) )
9 1 frgrhash2wsp 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) )
10 9 eqcomd 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) = ( # ` ( 2 WSPathsN G ) ) )
11 10 eqeq1d 
 |-  ( ( G e. FriendGraph /\ V e. Fin ) -> ( ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) <-> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) ) )
12 11 3adant3 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) <-> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) ) )
13 12 adantr 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) <-> ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) ) )
14 1 frrusgrord0lem 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( K e. CC /\ ( # ` V ) e. CC /\ ( # ` V ) =/= 0 ) )
15 peano2cnm 
 |-  ( ( # ` V ) e. CC -> ( ( # ` V ) - 1 ) e. CC )
16 15 3ad2ant2 
 |-  ( ( K e. CC /\ ( # ` V ) e. CC /\ ( # ` V ) =/= 0 ) -> ( ( # ` V ) - 1 ) e. CC )
17 kcnktkm1cn 
 |-  ( K e. CC -> ( K x. ( K - 1 ) ) e. CC )
18 17 3ad2ant1 
 |-  ( ( K e. CC /\ ( # ` V ) e. CC /\ ( # ` V ) =/= 0 ) -> ( K x. ( K - 1 ) ) e. CC )
19 simp2 
 |-  ( ( K e. CC /\ ( # ` V ) e. CC /\ ( # ` V ) =/= 0 ) -> ( # ` V ) e. CC )
20 simp3 
 |-  ( ( K e. CC /\ ( # ` V ) e. CC /\ ( # ` V ) =/= 0 ) -> ( # ` V ) =/= 0 )
21 16 18 19 20 mulcand 
 |-  ( ( K e. CC /\ ( # ` V ) e. CC /\ ( # ` V ) =/= 0 ) -> ( ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) <-> ( ( # ` V ) - 1 ) = ( K x. ( K - 1 ) ) ) )
22 npcan1 
 |-  ( ( # ` V ) e. CC -> ( ( ( # ` V ) - 1 ) + 1 ) = ( # ` V ) )
23 oveq1 
 |-  ( ( ( # ` V ) - 1 ) = ( K x. ( K - 1 ) ) -> ( ( ( # ` V ) - 1 ) + 1 ) = ( ( K x. ( K - 1 ) ) + 1 ) )
24 22 23 sylan9req 
 |-  ( ( ( # ` V ) e. CC /\ ( ( # ` V ) - 1 ) = ( K x. ( K - 1 ) ) ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) )
25 24 ex 
 |-  ( ( # ` V ) e. CC -> ( ( ( # ` V ) - 1 ) = ( K x. ( K - 1 ) ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )
26 25 3ad2ant2 
 |-  ( ( K e. CC /\ ( # ` V ) e. CC /\ ( # ` V ) =/= 0 ) -> ( ( ( # ` V ) - 1 ) = ( K x. ( K - 1 ) ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )
27 21 26 sylbid 
 |-  ( ( K e. CC /\ ( # ` V ) e. CC /\ ( # ` V ) =/= 0 ) -> ( ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )
28 14 27 syl 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( ( ( # ` V ) x. ( ( # ` V ) - 1 ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )
29 13 28 sylbird 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( ( # ` ( 2 WSPathsN G ) ) = ( ( # ` V ) x. ( K x. ( K - 1 ) ) ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )
30 8 29 mpd 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) )
31 30 ex 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )