Metamath Proof Explorer

Theorem clwwlknon2num

Description: In a K-regular graph G , there are K closed walks on vertex X of length 2 . (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 25-Mar-2022)

Ref Expression
Assertion clwwlknon2num ⊢ G RegUSGraph K ∧ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 2 = K

Proof

Step Hyp Ref Expression
1 eqid ⊢ ClWWalksNOn ⁡ G = ClWWalksNOn ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 1 2 3 clwwlknon2x ⊢ X ClWWalksNOn ⁡ G 2 = w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
5 4 a1i ⊢ G RegUSGraph K ∧ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 2 = w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
6 5 fveq2d ⊢ G RegUSGraph K ∧ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 2 = w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
7 3ancomb ⊢ w = 2 ∧ w ⁡ 0 = X ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ↔ w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
8 7 rabbii ⊢ w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 = X ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G = w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
9 8 fveq2i ⊢ w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 = X ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G = w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X
10 2 rusgrnumwrdl2 ⊢ G RegUSGraph K ∧ X ∈ Vtx ⁡ G → w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 = X ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G = K
11 9 10 eqtr3id ⊢ G RegUSGraph K ∧ X ∈ Vtx ⁡ G → w ∈ Word Vtx ⁡ G | w = 2 ∧ w ⁡ 0 w ⁡ 1 ∈ Edg ⁡ G ∧ w ⁡ 0 = X = K
12 6 11 eqtrd ⊢ G RegUSGraph K ∧ X ∈ Vtx ⁡ G → X ClWWalksNOn ⁡ G 2 = K