Metamath Proof Explorer


Theorem cusgrm1rusgr

Description: A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for k e. ZZ , then the assumption V =/= (/) could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Hypothesis cusgrrusgr.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion cusgrm1rusgr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) )

Proof

Step Hyp Ref Expression
1 cusgrrusgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 simpr ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝐺 ∈ ComplUSGraph )
3 1 fusgrvtxfi ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin )
4 3 adantr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → 𝑉 ∈ Fin )
5 4 adantr ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝑉 ∈ Fin )
6 simpr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → 𝑉 ≠ ∅ )
7 6 adantr ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝑉 ≠ ∅ )
8 1 cusgrrusgr ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) )
9 2 5 7 8 syl3anc ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) )
10 9 ex ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ ComplUSGraph → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
11 eqid ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
12 1 11 rusgrprop0 ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → ( 𝐺 ∈ USGraph ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
13 12 simp3d ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
14 1 vdiscusgr ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )
15 14 adantr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )
16 13 15 syl5 ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )
17 10 16 impbid ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) )