Metamath Proof Explorer

Theorem clwlkclwwlkf1lem2

Description: Lemma 2 for clwlkclwwlkf1 . (Contributed by AV, 24-May-2022) (Revised by AV, 30-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
clwlkclwwlkf.a ⊢ 𝐴 = ( 1st ‘ 𝑈 )
clwlkclwwlkf.b ⊢ 𝐵 = ( 2nd ‘ 𝑈 )
clwlkclwwlkf.d ⊢ 𝐷 = ( 1st ‘ 𝑊 )
clwlkclwwlkf.e ⊢ 𝐸 = ( 2nd ‘ 𝑊 )
Assertion clwlkclwwlkf1lem2 ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
2 clwlkclwwlkf.a ⊢ 𝐴 = ( 1st ‘ 𝑈 )
3 clwlkclwwlkf.b ⊢ 𝐵 = ( 2nd ‘ 𝑈 )
4 clwlkclwwlkf.d ⊢ 𝐷 = ( 1st ‘ 𝑊 )
5 clwlkclwwlkf.e ⊢ 𝐸 = ( 2nd ‘ 𝑊 )
6 1 2 3 clwlkclwwlkflem ⊢ ( 𝑈 ∈ 𝐶 → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
7 1 4 5 clwlkclwwlkflem ⊢ ( 𝑊 ∈ 𝐶 → ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) )
8 6 7 anim12i ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ) → ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) )
9 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10 9 wlkpwrd ⊢ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
11 10 3ad2ant1 ⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) )
12 9 wlkpwrd ⊢ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 → 𝐸 ∈ Word ( Vtx ‘ 𝐺 ) )
13 12 3ad2ant1 ⊢ ( ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) → 𝐸 ∈ Word ( Vtx ‘ 𝐺 ) )
14 11 13 anim12i ⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) → ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐸 ∈ Word ( Vtx ‘ 𝐺 ) ) )
15 nnnn0 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
17 nnnn0 ⊢ ( ( ♯ ‘ 𝐷 ) ∈ ℕ → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
18 17 3ad2ant3 ⊢ ( ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) → ( ♯ ‘ 𝐷 ) ∈ ℕ0 )
19 16 18 anim12i ⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ0 ) )
20 wlklenvp1 ⊢ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 → ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
21 nnre ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ∈ ℝ )
22 21 lep1d ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + 1 ) )
23 breq2 ⊢ ( ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) + 1 ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ ( ♯ ‘ 𝐴 ) ≤ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
24 22 23 imbitrrid ⊢ ( ( ♯ ‘ 𝐵 ) = ( ( ♯ ‘ 𝐴 ) + 1 ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
25 20 24 syl ⊢ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
26 25 a1d ⊢ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 → ( ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
27 26 3imp ⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )
28 wlklenvp1 ⊢ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 → ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝐷 ) + 1 ) )
29 nnre ⊢ ( ( ♯ ‘ 𝐷 ) ∈ ℕ → ( ♯ ‘ 𝐷 ) ∈ ℝ )
30 29 lep1d ⊢ ( ( ♯ ‘ 𝐷 ) ∈ ℕ → ( ♯ ‘ 𝐷 ) ≤ ( ( ♯ ‘ 𝐷 ) + 1 ) )
31 breq2 ⊢ ( ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝐷 ) + 1 ) → ( ( ♯ ‘ 𝐷 ) ≤ ( ♯ ‘ 𝐸 ) ↔ ( ♯ ‘ 𝐷 ) ≤ ( ( ♯ ‘ 𝐷 ) + 1 ) ) )
32 30 31 imbitrrid ⊢ ( ( ♯ ‘ 𝐸 ) = ( ( ♯ ‘ 𝐷 ) + 1 ) → ( ( ♯ ‘ 𝐷 ) ∈ ℕ → ( ♯ ‘ 𝐷 ) ≤ ( ♯ ‘ 𝐸 ) ) )
33 28 32 syl ⊢ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 → ( ( ♯ ‘ 𝐷 ) ∈ ℕ → ( ♯ ‘ 𝐷 ) ≤ ( ♯ ‘ 𝐸 ) ) )
34 33 a1d ⊢ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 → ( ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) → ( ( ♯ ‘ 𝐷 ) ∈ ℕ → ( ♯ ‘ 𝐷 ) ≤ ( ♯ ‘ 𝐸 ) ) ) )
35 34 3imp ⊢ ( ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) → ( ♯ ‘ 𝐷 ) ≤ ( ♯ ‘ 𝐸 ) )
36 27 35 anim12i ⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐷 ) ≤ ( ♯ ‘ 𝐸 ) ) )
37 14 19 36 3jca ⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) → ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐸 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐷 ) ≤ ( ♯ ‘ 𝐸 ) ) ) )
38 pfxeq ⊢ ( ( ( 𝐵 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝐸 ∈ Word ( Vtx ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ0 ) ∧ ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ∧ ( ♯ ‘ 𝐷 ) ≤ ( ♯ ‘ 𝐸 ) ) ) → ( ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ↔ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) ) )
39 8 37 38 3syl ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ) → ( ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ↔ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) ) )
40 39 biimp3a ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) )