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 \in Fin \land V \neq \emptyset) \to ((G \in FriendGraph \land G RegUSGraph K) \to \|V\| = K (K - 1) + 1)$

Proof

Step	Hyp	Ref	Expression
1		frrusgrord0.v	$⊢ V = Vtx (G)$
2		rusgrrgr	$⊢ G RegUSGraph K \to G RegGraph K$
3		eqid	$⊢ VtxDeg (G) = VtxDeg (G)$
4	1 3	rgrprop	$⊢ G RegGraph K \to (K \in ℕ_{0}^{*} \land \forall v \in V VtxDeg (G) (v) = K)$
5	2 4	syl	$⊢ G RegUSGraph K \to (K \in ℕ_{0}^{*} \land \forall v \in V VtxDeg (G) (v) = K)$
6	5	simprd	$⊢ G RegUSGraph K \to \forall v \in V VtxDeg (G) (v) = K$
7	1	frrusgrord0	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to (\forall v \in V VtxDeg (G) (v) = K \to \|V\| = K (K - 1) + 1)$
8	6 7	syl5	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to (G RegUSGraph K \to \|V\| = K (K - 1) + 1)$
9	8	3expb	$⊢ (G \in FriendGraph \land (V \in Fin \land V \neq \emptyset)) \to (G RegUSGraph K \to \|V\| = K (K - 1) + 1)$
10	9	expcom	$⊢ (V \in Fin \land V \neq \emptyset) \to (G \in FriendGraph \to (G RegUSGraph K \to \|V\| = K (K - 1) + 1))$
11	10	impd	$⊢ (V \in Fin \land V \neq \emptyset) \to ((G \in FriendGraph \land G RegUSGraph K) \to \|V\| = K (K - 1) + 1)$

Metamath Proof Explorer

Theorem frrusgrord

Proof