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≤1st⁡w
clwlkclwwlkf.a ⊢A=1st⁡U
clwlkclwwlkf.b ⊢B=2nd⁡U
clwlkclwwlkf.d ⊢D=1st⁡W
clwlkclwwlkf.e ⊢E=2nd⁡W
Assertion clwlkclwwlkf1lem3 ⊢U∈C∧W∈C∧BprefixA=EprefixD→∀i∈0…AB⁡i=E⁡i

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢C=w∈ClWalks⁡G|1≤1st⁡w
2 clwlkclwwlkf.a ⊢A=1st⁡U
3 clwlkclwwlkf.b ⊢B=2nd⁡U
4 clwlkclwwlkf.d ⊢D=1st⁡W
5 clwlkclwwlkf.e ⊢E=2nd⁡W
6 1 2 3 4 5 clwlkclwwlkf1lem2 ⊢U∈C∧W∈C∧BprefixA=EprefixD→A=D∧∀i∈0..^AB⁡i=E⁡i
7 simprr ⊢U∈C∧W∈C∧BprefixA=EprefixD∧A=D∧∀i∈0..^AB⁡i=E⁡i→∀i∈0..^AB⁡i=E⁡i
8 1 2 3 clwlkclwwlkflem ⊢U∈C→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ
9 1 4 5 clwlkclwwlkflem ⊢W∈C→DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ
10 lbfzo0 ⊢0∈0..^A↔A∈ℕ
11 10 biimpri ⊢A∈ℕ→0∈0..^A
12 11 3ad2ant3 ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ→0∈0..^A
13 12 adantr ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ→0∈0..^A
14 13 adantr ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧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..^AB⁡i=E⁡i→B⁡0=E⁡0
19 14 18 syl ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ∧A=D→∀i∈0..^AB⁡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 ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ→E⁡0=E⁡D→B⁡0=E⁡0→B⁡A=E⁡D
28 27 com12 ⊢E⁡0=E⁡D→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ→B⁡0=E⁡0→B⁡A=E⁡D
29 28 3ad2ant2 ⊢DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ→AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ→B⁡0=E⁡0→B⁡A=E⁡D
30 29 impcom ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ→B⁡0=E⁡0→B⁡A=E⁡D
31 30 adantr ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ∧A=D→B⁡0=E⁡0→B⁡A=E⁡D
32 31 imp ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧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 ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ∧A=D→E⁡D=E⁡A
36 35 adantr ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ∧A=D∧B⁡0=E⁡0→E⁡D=E⁡A
37 32 36 eqtrd ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ∧A=D∧B⁡0=E⁡0→B⁡A=E⁡A
38 37 ex ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ∧A=D→B⁡0=E⁡0→B⁡A=E⁡A
39 19 38 syld ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ∧A=D→∀i∈0..^AB⁡i=E⁡i→B⁡A=E⁡A
40 39 ex ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ∧DWalks⁡GE∧E⁡0=E⁡D∧D∈ℕ→A=D→∀i∈0..^AB⁡i=E⁡i→B⁡A=E⁡A
41 8 9 40 syl2an ⊢U∈C∧W∈C→A=D→∀i∈0..^AB⁡i=E⁡i→B⁡A=E⁡A
42 41 impd ⊢U∈C∧W∈C→A=D∧∀i∈0..^AB⁡i=E⁡i→B⁡A=E⁡A
43 42 3adant3 ⊢U∈C∧W∈C∧BprefixA=EprefixD→A=D∧∀i∈0..^AB⁡i=E⁡i→B⁡A=E⁡A
44 43 imp ⊢U∈C∧W∈C∧BprefixA=EprefixD∧A=D∧∀i∈0..^AB⁡i=E⁡i→B⁡A=E⁡A
45 7 44 jca ⊢U∈C∧W∈C∧BprefixA=EprefixD∧A=D∧∀i∈0..^AB⁡i=E⁡i→∀i∈0..^AB⁡i=E⁡i∧B⁡A=E⁡A
46 6 45 mpdan ⊢U∈C∧W∈C∧BprefixA=EprefixD→∀i∈0..^AB⁡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∪AB⁡i=E⁡i↔∀i∈0..^AB⁡i=E⁡i∧B⁡A=E⁡A
52 47 51 ax-mp ⊢∀i∈0..^A∪AB⁡i=E⁡i↔∀i∈0..^AB⁡i=E⁡i∧B⁡A=E⁡A
53 46 52 sylibr ⊢U∈C∧W∈C∧BprefixA=EprefixD→∀i∈0..^A∪AB⁡i=E⁡i
54 nnnn0 ⊢A∈ℕ→A∈ℕ0
55 elnn0uz ⊢A∈ℕ0↔A∈ℤ≥0
56 54 55 sylib ⊢A∈ℕ→A∈ℤ≥0
57 56 3ad2ant3 ⊢AWalks⁡GB∧B⁡0=B⁡A∧A∈ℕ→A∈ℤ≥0
58 8 57 syl ⊢U∈C→A∈ℤ≥0
59 58 3ad2ant1 ⊢U∈C∧W∈C∧BprefixA=EprefixD→A∈ℤ≥0
60 fzisfzounsn ⊢A∈ℤ≥0→0…A=0..^A∪A
61 59 60 syl ⊢U∈C∧W∈C∧BprefixA=EprefixD→0…A=0..^A∪A
62 61 raleqdv ⊢U∈C∧W∈C∧BprefixA=EprefixD→∀i∈0…AB⁡i=E⁡i↔∀i∈0..^A∪AB⁡i=E⁡i
63 53 62 mpbird ⊢U∈C∧W∈C∧BprefixA=EprefixD→∀i∈0…AB⁡i=E⁡i