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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
rusgrnumwwlk.l ⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
Assertion rusgrnumwwlkb0 ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( 𝑃 𝐿 0 ) = 1 )

Proof

Step Hyp Ref Expression
1 rusgrnumwwlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 rusgrnumwwlk.l ⊢ 𝐿 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ℕ0 ↦ ( ♯ ‘ { 𝑤 ∈ ( 𝑛 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑣 } ) )
3 simpr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → 𝑃 ∈ 𝑉 )
4 0nn0 ⊢ 0 ∈ ℕ0
5 1 2 rusgrnumwwlklem ⊢ ( ( 𝑃 ∈ 𝑉 ∧ 0 ∈ ℕ0 ) → ( 𝑃 𝐿 0 ) = ( ♯ ‘ { 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
6 3 4 5 sylancl ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( 𝑃 𝐿 0 ) = ( ♯ ‘ { 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) )
7 df-rab ⊢ { 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } = { 𝑤 ∣ ( 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) }
8 7 a1i ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → { 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } = { 𝑤 ∣ ( 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) } )
9 wwlksn0s ⊢ ( 0 WWalksN 𝐺 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 1 }
10 9 a1i ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( 0 WWalksN 𝐺 ) = { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 1 } )
11 10 eleq2d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( 𝑤 ∈ ( 0 WWalksN 𝐺 ) ↔ 𝑤 ∈ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 1 } ) )
12 rabid ⊢ ( 𝑤 ∈ { 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑤 ) = 1 } ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) )
13 11 12 bitrdi ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( 𝑤 ∈ ( 0 WWalksN 𝐺 ) ↔ ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ) )
14 13 anbi1d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( ( 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) )
15 14 abbidv ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → { 𝑤 ∣ ( 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) } = { 𝑤 ∣ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) } )
16 wrdl1s1 ⊢ ( 𝑃 ∈ ( Vtx ‘ 𝐺 ) → ( 𝑣 = ⟨“ 𝑃 ”⟩ ↔ ( 𝑣 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑣 ) = 1 ∧ ( 𝑣 ‘ 0 ) = 𝑃 ) ) )
17 df-3an ⊢ ( ( 𝑣 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑣 ) = 1 ∧ ( 𝑣 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝑣 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑣 ) = 1 ) ∧ ( 𝑣 ‘ 0 ) = 𝑃 ) )
18 16 17 bitr2di ⊢ ( 𝑃 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( 𝑣 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑣 ) = 1 ) ∧ ( 𝑣 ‘ 0 ) = 𝑃 ) ↔ 𝑣 = ⟨“ 𝑃 ”⟩ ) )
19 vex ⊢ 𝑣 ∈ V
20 eleq1w ⊢ ( 𝑤 = 𝑣 → ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ↔ 𝑣 ∈ Word ( Vtx ‘ 𝐺 ) ) )
21 fveqeq2 ⊢ ( 𝑤 = 𝑣 → ( ( ♯ ‘ 𝑤 ) = 1 ↔ ( ♯ ‘ 𝑣 ) = 1 ) )
22 20 21 anbi12d ⊢ ( 𝑤 = 𝑣 → ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ↔ ( 𝑣 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑣 ) = 1 ) ) )
23 fveq1 ⊢ ( 𝑤 = 𝑣 → ( 𝑤 ‘ 0 ) = ( 𝑣 ‘ 0 ) )
24 23 eqeq1d ⊢ ( 𝑤 = 𝑣 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑣 ‘ 0 ) = 𝑃 ) )
25 22 24 anbi12d ⊢ ( 𝑤 = 𝑣 → ( ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝑣 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑣 ) = 1 ) ∧ ( 𝑣 ‘ 0 ) = 𝑃 ) ) )
26 19 25 elab ⊢ ( 𝑣 ∈ { 𝑤 ∣ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) } ↔ ( ( 𝑣 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑣 ) = 1 ) ∧ ( 𝑣 ‘ 0 ) = 𝑃 ) )
27 velsn ⊢ ( 𝑣 ∈ { ⟨“ 𝑃 ”⟩ } ↔ 𝑣 = ⟨“ 𝑃 ”⟩ )
28 18 26 27 3bitr4g ⊢ ( 𝑃 ∈ ( Vtx ‘ 𝐺 ) → ( 𝑣 ∈ { 𝑤 ∣ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) } ↔ 𝑣 ∈ { ⟨“ 𝑃 ”⟩ } ) )
29 28 1 eleq2s ⊢ ( 𝑃 ∈ 𝑉 → ( 𝑣 ∈ { 𝑤 ∣ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) } ↔ 𝑣 ∈ { ⟨“ 𝑃 ”⟩ } ) )
30 29 eqrdv ⊢ ( 𝑃 ∈ 𝑉 → { 𝑤 ∣ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) } = { ⟨“ 𝑃 ”⟩ } )
31 30 adantl ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → { 𝑤 ∣ ( ( 𝑤 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = 1 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) } = { ⟨“ 𝑃 ”⟩ } )
32 8 15 31 3eqtrd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → { 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } = { ⟨“ 𝑃 ”⟩ } )
33 32 fveq2d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ ( 0 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( ♯ ‘ { ⟨“ 𝑃 ”⟩ } ) )
34 s1cl ⊢ ( 𝑃 ∈ 𝑉 → ⟨“ 𝑃 ”⟩ ∈ Word 𝑉 )
35 hashsng ⊢ ( ⟨“ 𝑃 ”⟩ ∈ Word 𝑉 → ( ♯ ‘ { ⟨“ 𝑃 ”⟩ } ) = 1 )
36 34 35 syl ⊢ ( 𝑃 ∈ 𝑉 → ( ♯ ‘ { ⟨“ 𝑃 ”⟩ } ) = 1 )
37 36 adantl ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { ⟨“ 𝑃 ”⟩ } ) = 1 )
38 6 33 37 3eqtrd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ) → ( 𝑃 𝐿 0 ) = 1 )