Metamath Proof Explorer

Theorem cusgrrusgr

Description: A complete simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Hypothesis cusgrrusgr.v ⊢ V = Vtx ⁡ G
Assertion cusgrrusgr ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G RegUSGraph V − 1

Proof

Step Hyp Ref Expression
1 cusgrrusgr.v ⊢ V = Vtx ⁡ G
2 cusgrusgr ⊢ G ∈ ComplUSGraph → G ∈ USGraph
3 2 3ad2ant1 ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G ∈ USGraph
4 hashnncl ⊢ V ∈ Fin → V ∈ ℕ ↔ V ≠ ∅
5 nnm1nn0 ⊢ V ∈ ℕ → V − 1 ∈ ℕ 0
6 5 nn0xnn0d ⊢ V ∈ ℕ → V − 1 ∈ ℕ 0 *
7 4 6 biimtrrdi ⊢ V ∈ Fin → V ≠ ∅ → V − 1 ∈ ℕ 0 *
8 7 imp ⊢ V ∈ Fin ∧ V ≠ ∅ → V − 1 ∈ ℕ 0 *
9 8 3adant1 ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → V − 1 ∈ ℕ 0 *
10 cusgrcplgr ⊢ G ∈ ComplUSGraph → G ∈ ComplGraph
11 10 3ad2ant1 ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G ∈ ComplGraph
12 1 nbcplgr ⊢ G ∈ ComplGraph ∧ v ∈ V → G NeighbVtx v = V ∖ v
13 11 12 sylan ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ v ∈ V → G NeighbVtx v = V ∖ v
14 13 ralrimiva ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → ∀ v ∈ V G NeighbVtx v = V ∖ v
15 3 anim1i ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ v ∈ V → G ∈ USGraph ∧ v ∈ V
16 15 adantr ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ v ∈ V ∧ G NeighbVtx v = V ∖ v → G ∈ USGraph ∧ v ∈ V
17 1 hashnbusgrvd ⊢ G ∈ USGraph ∧ v ∈ V → G NeighbVtx v = VtxDeg ⁡ G ⁡ v
18 16 17 syl ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ v ∈ V ∧ G NeighbVtx v = V ∖ v → G NeighbVtx v = VtxDeg ⁡ G ⁡ v
19 fveq2 ⊢ G NeighbVtx v = V ∖ v → G NeighbVtx v = V ∖ v
20 hashdifsn ⊢ V ∈ Fin ∧ v ∈ V → V ∖ v = V − 1
21 20 3ad2antl2 ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ v ∈ V → V ∖ v = V − 1
22 19 21 sylan9eqr ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ v ∈ V ∧ G NeighbVtx v = V ∖ v → G NeighbVtx v = V − 1
23 18 22 eqtr3d ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ v ∈ V ∧ G NeighbVtx v = V ∖ v → VtxDeg ⁡ G ⁡ v = V − 1
24 23 ex ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ ∧ v ∈ V → G NeighbVtx v = V ∖ v → VtxDeg ⁡ G ⁡ v = V − 1
25 24 ralimdva ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → ∀ v ∈ V G NeighbVtx v = V ∖ v → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1
26 14 25 mpd ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1
27 simp1 ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G ∈ ComplUSGraph
28 ovex ⊢ V − 1 ∈ V
29 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
30 1 29 isrusgr0 ⊢ G ∈ ComplUSGraph ∧ V − 1 ∈ V → G RegUSGraph V − 1 ↔ G ∈ USGraph ∧ V − 1 ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1
31 27 28 30 sylancl ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G RegUSGraph V − 1 ↔ G ∈ USGraph ∧ V − 1 ∈ ℕ 0 * ∧ ∀ v ∈ V VtxDeg ⁡ G ⁡ v = V − 1
32 3 9 26 31 mpbir3and ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ V ≠ ∅ → G RegUSGraph V − 1