Metamath Proof Explorer


Theorem vdiscusgr

Description: In a finite complete simple graph with n vertices every vertex has degree n - 1 . (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 17-Dec-2020)

Ref Expression
Hypothesis hashnbusgrvd.v 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vdiscusgr ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v 𝑉 = ( Vtx ‘ 𝐺 )
2 1 uvtxisvtx ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑛𝑉 )
3 fveqeq2 ( 𝑣 = 𝑛 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
4 3 rspccv ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( 𝑛𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
5 4 adantl ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑛𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
6 5 imp ( ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ∧ 𝑛𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
7 1 usgruvtxvdb ( ( 𝐺 ∈ FinUSGraph ∧ 𝑛𝑉 ) → ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
8 7 adantlr ( ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ∧ 𝑛𝑉 ) → ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑛 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
9 6 8 mpbird ( ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ∧ 𝑛𝑉 ) → 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) )
10 9 ex ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑛𝑉𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ) )
11 2 10 impbid2 ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ↔ 𝑛𝑉 ) )
12 11 eqrdv ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( UnivVtx ‘ 𝐺 ) = 𝑉 )
13 fusgrusgr ( 𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph )
14 1 cusgruvtxb ( 𝐺 ∈ USGraph → ( 𝐺 ∈ ComplUSGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) )
15 13 14 syl ( 𝐺 ∈ FinUSGraph → ( 𝐺 ∈ ComplUSGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) )
16 15 adantr ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝐺 ∈ ComplUSGraph ↔ ( UnivVtx ‘ 𝐺 ) = 𝑉 ) )
17 12 16 mpbird ( ( 𝐺 ∈ FinUSGraph ∧ ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → 𝐺 ∈ ComplUSGraph )
18 17 ex ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )