Metamath Proof Explorer

Theorem rusgrnumwwlkb0

Description: Induction base 0 for rusgrnumwwlk . Here, we do not need the regularity of the graph yet. (Contributed by Alexander van der Vekens, 24-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 rusgrnumwwlkb0 ⊢ G ∈ USHGraph ∧ P ∈ V → P L 0 = 1

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 simpr ⊢ G ∈ USHGraph ∧ P ∈ V → P ∈ V
4 0nn0 ⊢ 0 ∈ ℕ 0
5 1 2 rusgrnumwwlklem ⊢ P ∈ V ∧ 0 ∈ ℕ 0 → P L 0 = w ∈ 0 WWalksN G | w ⁡ 0 = P
6 3 4 5 sylancl ⊢ G ∈ USHGraph ∧ P ∈ V → P L 0 = w ∈ 0 WWalksN G | w ⁡ 0 = P
7 df-rab ⊢ w ∈ 0 WWalksN G | w ⁡ 0 = P = w | w ∈ 0 WWalksN G ∧ w ⁡ 0 = P
8 7 a1i ⊢ G ∈ USHGraph ∧ P ∈ V → w ∈ 0 WWalksN G | w ⁡ 0 = P = w | w ∈ 0 WWalksN G ∧ w ⁡ 0 = P
9 wwlksn0s ⊢ 0 WWalksN G = w ∈ Word Vtx ⁡ G | w = 1
10 9 a1i ⊢ G ∈ USHGraph ∧ P ∈ V → 0 WWalksN G = w ∈ Word Vtx ⁡ G | w = 1
11 10 eleq2d ⊢ G ∈ USHGraph ∧ P ∈ V → w ∈ 0 WWalksN G ↔ w ∈ w ∈ Word Vtx ⁡ G | w = 1
12 rabid ⊢ w ∈ w ∈ Word Vtx ⁡ G | w = 1 ↔ w ∈ Word Vtx ⁡ G ∧ w = 1
13 11 12 bitrdi ⊢ G ∈ USHGraph ∧ P ∈ V → w ∈ 0 WWalksN G ↔ w ∈ Word Vtx ⁡ G ∧ w = 1
14 13 anbi1d ⊢ G ∈ USHGraph ∧ P ∈ V → w ∈ 0 WWalksN G ∧ w ⁡ 0 = P ↔ w ∈ Word Vtx ⁡ G ∧ w = 1 ∧ w ⁡ 0 = P
15 14 abbidv ⊢ G ∈ USHGraph ∧ P ∈ V → w | w ∈ 0 WWalksN G ∧ w ⁡ 0 = P = w | w ∈ Word Vtx ⁡ G ∧ w = 1 ∧ w ⁡ 0 = P
16 wrdl1s1 ⊢ P ∈ Vtx ⁡ G → v = ⟨“ P ”⟩ ↔ v ∈ Word Vtx ⁡ G ∧ v = 1 ∧ v ⁡ 0 = P
17 df-3an ⊢ v ∈ Word Vtx ⁡ G ∧ v = 1 ∧ v ⁡ 0 = P ↔ v ∈ Word Vtx ⁡ G ∧ v = 1 ∧ v ⁡ 0 = P
18 16 17 bitr2di ⊢ P ∈ Vtx ⁡ G → v ∈ Word Vtx ⁡ G ∧ v = 1 ∧ v ⁡ 0 = P ↔ v = ⟨“ P ”⟩
19 vex ⊢ v ∈ V
20 eleq1w ⊢ w = v → w ∈ Word Vtx ⁡ G ↔ v ∈ Word Vtx ⁡ G
21 fveqeq2 ⊢ w = v → w = 1 ↔ v = 1
22 20 21 anbi12d ⊢ w = v → w ∈ Word Vtx ⁡ G ∧ w = 1 ↔ v ∈ Word Vtx ⁡ G ∧ v = 1
23 fveq1 ⊢ w = v → w ⁡ 0 = v ⁡ 0
24 23 eqeq1d ⊢ w = v → w ⁡ 0 = P ↔ v ⁡ 0 = P
25 22 24 anbi12d ⊢ w = v → w ∈ Word Vtx ⁡ G ∧ w = 1 ∧ w ⁡ 0 = P ↔ v ∈ Word Vtx ⁡ G ∧ v = 1 ∧ v ⁡ 0 = P
26 19 25 elab ⊢ v ∈ w | w ∈ Word Vtx ⁡ G ∧ w = 1 ∧ w ⁡ 0 = P ↔ v ∈ Word Vtx ⁡ G ∧ v = 1 ∧ v ⁡ 0 = P
27 velsn ⊢ v ∈ ⟨“ P ”⟩ ↔ v = ⟨“ P ”⟩
28 18 26 27 3bitr4g ⊢ P ∈ Vtx ⁡ G → v ∈ w | w ∈ Word Vtx ⁡ G ∧ w = 1 ∧ w ⁡ 0 = P ↔ v ∈ ⟨“ P ”⟩
29 28 1 eleq2s ⊢ P ∈ V → v ∈ w | w ∈ Word Vtx ⁡ G ∧ w = 1 ∧ w ⁡ 0 = P ↔ v ∈ ⟨“ P ”⟩
30 29 eqrdv ⊢ P ∈ V → w | w ∈ Word Vtx ⁡ G ∧ w = 1 ∧ w ⁡ 0 = P = ⟨“ P ”⟩
31 30 adantl ⊢ G ∈ USHGraph ∧ P ∈ V → w | w ∈ Word Vtx ⁡ G ∧ w = 1 ∧ w ⁡ 0 = P = ⟨“ P ”⟩
32 8 15 31 3eqtrd ⊢ G ∈ USHGraph ∧ P ∈ V → w ∈ 0 WWalksN G | w ⁡ 0 = P = ⟨“ P ”⟩
33 32 fveq2d ⊢ G ∈ USHGraph ∧ P ∈ V → w ∈ 0 WWalksN G | w ⁡ 0 = P = ⟨“ P ”⟩
34 s1cl ⊢ P ∈ V → ⟨“ P ”⟩ ∈ Word V
35 hashsng ⊢ ⟨“ P ”⟩ ∈ Word V → ⟨“ P ”⟩ = 1
36 34 35 syl ⊢ P ∈ V → ⟨“ P ”⟩ = 1
37 36 adantl ⊢ G ∈ USHGraph ∧ P ∈ V → ⟨“ P ”⟩ = 1
38 6 33 37 3eqtrd ⊢ G ∈ USHGraph ∧ P ∈ V → P L 0 = 1