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 ⊢V=Vtx⁡G
Assertion vdiscusgr ⊢G∈FinUSGraph→∀v∈VVtxDeg⁡G⁡v=V−1→G∈ComplUSGraph

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v ⊢V=Vtx⁡G
2 1 uvtxisvtx ⊢n∈UnivVtx⁡G→n∈V
3 fveqeq2 ⊢v=n→VtxDeg⁡G⁡v=V−1↔VtxDeg⁡G⁡n=V−1
4 3 rspccv ⊢∀v∈VVtxDeg⁡G⁡v=V−1→n∈V→VtxDeg⁡G⁡n=V−1
5 4 adantl ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1→n∈V→VtxDeg⁡G⁡n=V−1
6 5 imp ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1∧n∈V→VtxDeg⁡G⁡n=V−1
7 1 usgruvtxvdb ⊢G∈FinUSGraph∧n∈V→n∈UnivVtx⁡G↔VtxDeg⁡G⁡n=V−1
8 7 adantlr ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1∧n∈V→n∈UnivVtx⁡G↔VtxDeg⁡G⁡n=V−1
9 6 8 mpbird ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1∧n∈V→n∈UnivVtx⁡G
10 9 ex ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1→n∈V→n∈UnivVtx⁡G
11 2 10 impbid2 ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1→n∈UnivVtx⁡G↔n∈V
12 11 eqrdv ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1→UnivVtx⁡G=V
13 fusgrusgr ⊢G∈FinUSGraph→G∈USGraph
14 1 cusgruvtxb ⊢G∈USGraph→G∈ComplUSGraph↔UnivVtx⁡G=V
15 13 14 syl ⊢G∈FinUSGraph→G∈ComplUSGraph↔UnivVtx⁡G=V
16 15 adantr ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1→G∈ComplUSGraph↔UnivVtx⁡G=V
17 12 16 mpbird ⊢G∈FinUSGraph∧∀v∈VVtxDeg⁡G⁡v=V−1→G∈ComplUSGraph
18 17 ex ⊢G∈FinUSGraph→∀v∈VVtxDeg⁡G⁡v=V−1→G∈ComplUSGraph