Metamath Proof Explorer

Theorem rusgr0edg

Description: Special case for graphs without edges: There are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018) (Revised by AV, 7-May-2021)

Ref Expression
Hypotheses rusgrnumwwlk.v ⊢ V = Vtx ⁡ G
rusgrnumwwlk.l ⊢ L = v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v
Assertion rusgr0edg ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → P L N = 0

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v ⊢ V = Vtx ⁡ G
2 rusgrnumwwlk.l ⊢ L = v ∈ V , n ∈ ℕ 0 ⟼ w ∈ n WWalksN G | w ⁡ 0 = v
3 simp2 ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → P ∈ V
4 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
5 4 3ad2ant3 ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → N ∈ ℕ 0
6 1 2 rusgrnumwwlklem ⊢ P ∈ V ∧ N ∈ ℕ 0 → P L N = w ∈ N WWalksN G | w ⁡ 0 = P
7 3 5 6 syl2anc ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → P L N = w ∈ N WWalksN G | w ⁡ 0 = P
8 rusgrusgr ⊢ G RegUSGraph 0 → G ∈ USGraph
9 usgr0edg0rusgr ⊢ G ∈ USGraph → G RegUSGraph 0 ↔ Edg ⁡ G = ∅
10 9 biimpcd ⊢ G RegUSGraph 0 → G ∈ USGraph → Edg ⁡ G = ∅
11 8 10 mpd ⊢ G RegUSGraph 0 → Edg ⁡ G = ∅
12 0enwwlksnge1 ⊢ Edg ⁡ G = ∅ ∧ N ∈ ℕ → N WWalksN G = ∅
13 11 12 sylan ⊢ G RegUSGraph 0 ∧ N ∈ ℕ → N WWalksN G = ∅
14 eleq2 ⊢ N WWalksN G = ∅ → w ∈ N WWalksN G ↔ w ∈ ∅
15 noel ⊢ ¬ w ∈ ∅
16 15 pm2.21i ⊢ w ∈ ∅ → ¬ w ⁡ 0 = P
17 14 16 biimtrdi ⊢ N WWalksN G = ∅ → w ∈ N WWalksN G → ¬ w ⁡ 0 = P
18 13 17 syl ⊢ G RegUSGraph 0 ∧ N ∈ ℕ → w ∈ N WWalksN G → ¬ w ⁡ 0 = P
19 18 3adant2 ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → w ∈ N WWalksN G → ¬ w ⁡ 0 = P
20 19 ralrimiv ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → ∀ w ∈ N WWalksN G ¬ w ⁡ 0 = P
21 rabeq0 ⊢ w ∈ N WWalksN G | w ⁡ 0 = P = ∅ ↔ ∀ w ∈ N WWalksN G ¬ w ⁡ 0 = P
22 20 21 sylibr ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → w ∈ N WWalksN G | w ⁡ 0 = P = ∅
23 22 fveq2d ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → w ∈ N WWalksN G | w ⁡ 0 = P = ∅
24 hash0 ⊢ ∅ = 0
25 23 24 eqtrdi ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → w ∈ N WWalksN G | w ⁡ 0 = P = 0
26 7 25 eqtrd ⊢ G RegUSGraph 0 ∧ P ∈ V ∧ N ∈ ℕ → P L N = 0