Metamath Proof Explorer

Theorem clwlkclwwlkf1lem3

Description: Lemma 3 for clwlkclwwlkf1 . (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 30-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c ⊢ C = w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w
clwlkclwwlkf.a ⊢ A = 1 st ⁡ U
clwlkclwwlkf.b ⊢ B = 2 nd ⁡ U
clwlkclwwlkf.d ⊢ D = 1 st ⁡ W
clwlkclwwlkf.e ⊢ E = 2 nd ⁡ W
Assertion clwlkclwwlkf1lem3 ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → ∀ i ∈ 0 … A B ⁡ i = E ⁡ i

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢ C = w ∈ ClWalks ⁡ G | 1 ≤ 1 st ⁡ w
2 clwlkclwwlkf.a ⊢ A = 1 st ⁡ U
3 clwlkclwwlkf.b ⊢ B = 2 nd ⁡ U
4 clwlkclwwlkf.d ⊢ D = 1 st ⁡ W
5 clwlkclwwlkf.e ⊢ E = 2 nd ⁡ W
6 1 2 3 4 5 clwlkclwwlkf1lem2 ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i
7 simprr ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D ∧ A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i
8 1 2 3 clwlkclwwlkflem ⊢ U ∈ C → A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ
9 1 4 5 clwlkclwwlkflem ⊢ W ∈ C → D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ
10 lbfzo0 ⊢ 0 ∈ 0 ..^ A ↔ A ∈ ℕ
11 10 biimpri ⊢ A ∈ ℕ → 0 ∈ 0 ..^ A
12 11 3ad2ant3 ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ → 0 ∈ 0 ..^ A
13 12 adantr ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → 0 ∈ 0 ..^ A
14 13 adantr ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D → 0 ∈ 0 ..^ A
15 fveq2 ⊢ i = 0 → B ⁡ i = B ⁡ 0
16 fveq2 ⊢ i = 0 → E ⁡ i = E ⁡ 0
17 15 16 eqeq12d ⊢ i = 0 → B ⁡ i = E ⁡ i ↔ B ⁡ 0 = E ⁡ 0
18 17 rspcv ⊢ 0 ∈ 0 ..^ A → ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → B ⁡ 0 = E ⁡ 0
19 14 18 syl ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D → ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → B ⁡ 0 = E ⁡ 0
20 simpl ⊢ B ⁡ A = B ⁡ 0 ∧ B ⁡ 0 = E ⁡ 0 ∧ E ⁡ 0 = E ⁡ D → B ⁡ A = B ⁡ 0
21 eqtr ⊢ B ⁡ 0 = E ⁡ 0 ∧ E ⁡ 0 = E ⁡ D → B ⁡ 0 = E ⁡ D
22 21 adantl ⊢ B ⁡ A = B ⁡ 0 ∧ B ⁡ 0 = E ⁡ 0 ∧ E ⁡ 0 = E ⁡ D → B ⁡ 0 = E ⁡ D
23 20 22 eqtrd ⊢ B ⁡ A = B ⁡ 0 ∧ B ⁡ 0 = E ⁡ 0 ∧ E ⁡ 0 = E ⁡ D → B ⁡ A = E ⁡ D
24 23 exp32 ⊢ B ⁡ A = B ⁡ 0 → B ⁡ 0 = E ⁡ 0 → E ⁡ 0 = E ⁡ D → B ⁡ A = E ⁡ D
25 24 com23 ⊢ B ⁡ A = B ⁡ 0 → E ⁡ 0 = E ⁡ D → B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ D
26 25 eqcoms ⊢ B ⁡ 0 = B ⁡ A → E ⁡ 0 = E ⁡ D → B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ D
27 26 3ad2ant2 ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ → E ⁡ 0 = E ⁡ D → B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ D
28 27 com12 ⊢ E ⁡ 0 = E ⁡ D → A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ → B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ D
29 28 3ad2ant2 ⊢ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ → B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ D
30 29 impcom ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ D
31 30 adantr ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D → B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ D
32 31 imp ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D ∧ B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ D
33 fveq2 ⊢ D = A → E ⁡ D = E ⁡ A
34 33 eqcoms ⊢ A = D → E ⁡ D = E ⁡ A
35 34 adantl ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D → E ⁡ D = E ⁡ A
36 35 adantr ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D ∧ B ⁡ 0 = E ⁡ 0 → E ⁡ D = E ⁡ A
37 32 36 eqtrd ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D ∧ B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ A
38 37 ex ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D → B ⁡ 0 = E ⁡ 0 → B ⁡ A = E ⁡ A
39 19 38 syld ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ ∧ A = D → ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → B ⁡ A = E ⁡ A
40 39 ex ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ ∧ D Walks ⁡ G E ∧ E ⁡ 0 = E ⁡ D ∧ D ∈ ℕ → A = D → ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → B ⁡ A = E ⁡ A
41 8 9 40 syl2an ⊢ U ∈ C ∧ W ∈ C → A = D → ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → B ⁡ A = E ⁡ A
42 41 impd ⊢ U ∈ C ∧ W ∈ C → A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → B ⁡ A = E ⁡ A
43 42 3adant3 ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → B ⁡ A = E ⁡ A
44 43 imp ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D ∧ A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → B ⁡ A = E ⁡ A
45 7 44 jca ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D ∧ A = D ∧ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i → ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i ∧ B ⁡ A = E ⁡ A
46 6 45 mpdan ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i ∧ B ⁡ A = E ⁡ A
47 fvex ⊢ A ∈ V
48 fveq2 ⊢ i = A → B ⁡ i = B ⁡ A
49 fveq2 ⊢ i = A → E ⁡ i = E ⁡ A
50 48 49 eqeq12d ⊢ i = A → B ⁡ i = E ⁡ i ↔ B ⁡ A = E ⁡ A
51 50 ralunsn ⊢ A ∈ V → ∀ i ∈ 0 ..^ A ∪ A B ⁡ i = E ⁡ i ↔ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i ∧ B ⁡ A = E ⁡ A
52 47 51 ax-mp ⊢ ∀ i ∈ 0 ..^ A ∪ A B ⁡ i = E ⁡ i ↔ ∀ i ∈ 0 ..^ A B ⁡ i = E ⁡ i ∧ B ⁡ A = E ⁡ A
53 46 52 sylibr ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → ∀ i ∈ 0 ..^ A ∪ A B ⁡ i = E ⁡ i
54 nnnn0 ⊢ A ∈ ℕ → A ∈ ℕ 0
55 elnn0uz ⊢ A ∈ ℕ 0 ↔ A ∈ ℤ ≥ 0
56 54 55 sylib ⊢ A ∈ ℕ → A ∈ ℤ ≥ 0
57 56 3ad2ant3 ⊢ A Walks ⁡ G B ∧ B ⁡ 0 = B ⁡ A ∧ A ∈ ℕ → A ∈ ℤ ≥ 0
58 8 57 syl ⊢ U ∈ C → A ∈ ℤ ≥ 0
59 58 3ad2ant1 ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → A ∈ ℤ ≥ 0
60 fzisfzounsn ⊢ A ∈ ℤ ≥ 0 → 0 … A = 0 ..^ A ∪ A
61 59 60 syl ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → 0 … A = 0 ..^ A ∪ A
62 53 61 raleqtrrdv ⊢ U ∈ C ∧ W ∈ C ∧ B prefix A = E prefix D → ∀ i ∈ 0 … A B ⁡ i = E ⁡ i