This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( 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 e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> A. i e. ( 0 ... ( # ` A ) ) ( B ` i ) = ( E ` i ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c 
 |-  C = { w e. ( 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 e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) )
7 simprr 
 |-  ( ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) /\ ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) ) -> A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) )
8 1 2 3 clwlkclwwlkflem 
 |-  ( U e. C -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) )
9 1 4 5 clwlkclwwlkflem 
 |-  ( W e. C -> ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) )
10 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` A ) ) <-> ( # ` A ) e. NN )
11 10 biimpri 
 |-  ( ( # ` A ) e. NN -> 0 e. ( 0 ..^ ( # ` A ) ) )
12 11 3ad2ant3 
 |-  ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) -> 0 e. ( 0 ..^ ( # ` A ) ) )
13 12 adantr 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) -> 0 e. ( 0 ..^ ( # ` A ) ) )
14 13 adantr 
 |-  ( ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` A ) = ( # ` D ) ) -> 0 e. ( 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 e. ( 0 ..^ ( # ` A ) ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) -> ( B ` 0 ) = ( E ` 0 ) ) )
19 14 18 syl 
 |-  ( ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` A ) = ( # ` D ) ) -> ( A. i e. ( 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. NN ) -> ( ( 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 ) e. NN ) -> ( ( B ` 0 ) = ( E ` 0 ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` D ) ) ) ) )
29 28 3ad2ant2 
 |-  ( ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) -> ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) -> ( ( B ` 0 ) = ( E ` 0 ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` D ) ) ) ) )
30 29 impcom 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) -> ( ( B ` 0 ) = ( E ` 0 ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` D ) ) ) )
31 30 adantr 
 |-  ( ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` A ) = ( # ` D ) ) -> ( ( B ` 0 ) = ( E ` 0 ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` D ) ) ) )
32 31 imp 
 |-  ( ( ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` 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 ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` A ) = ( # ` D ) ) -> ( E ` ( # ` D ) ) = ( E ` ( # ` A ) ) )
36 35 adantr 
 |-  ( ( ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` A ) = ( # ` D ) ) /\ ( B ` 0 ) = ( E ` 0 ) ) -> ( E ` ( # ` D ) ) = ( E ` ( # ` A ) ) )
37 32 36 eqtrd 
 |-  ( ( ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` A ) = ( # ` D ) ) /\ ( B ` 0 ) = ( E ` 0 ) ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) )
38 37 ex 
 |-  ( ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` A ) = ( # ` D ) ) -> ( ( B ` 0 ) = ( E ` 0 ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) )
39 19 38 syld 
 |-  ( ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) /\ ( # ` A ) = ( # ` D ) ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) )
40 39 ex 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) -> ( ( # ` A ) = ( # ` D ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) ) )
41 8 9 40 syl2an 
 |-  ( ( U e. C /\ W e. C ) -> ( ( # ` A ) = ( # ` D ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) ) )
42 41 impd 
 |-  ( ( U e. C /\ W e. C ) -> ( ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) )
43 42 3adant3 
 |-  ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> ( ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) )
44 43 imp 
 |-  ( ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) /\ ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) ) -> ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) )
45 7 44 jca 
 |-  ( ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) /\ ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) /\ ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) )
46 6 45 mpdan 
 |-  ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) /\ ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) )
47 fvex 
 |-  ( # ` A ) e. _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 ) e. _V -> ( A. i e. ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) ( B ` i ) = ( E ` i ) <-> ( A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) /\ ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) ) )
52 47 51 ax-mp 
 |-  ( A. i e. ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) ( B ` i ) = ( E ` i ) <-> ( A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) /\ ( B ` ( # ` A ) ) = ( E ` ( # ` A ) ) ) )
53 46 52 sylibr 
 |-  ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> A. i e. ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) ( B ` i ) = ( E ` i ) )
54 nnnn0 
 |-  ( ( # ` A ) e. NN -> ( # ` A ) e. NN0 )
55 elnn0uz 
 |-  ( ( # ` A ) e. NN0 <-> ( # ` A ) e. ( ZZ>= ` 0 ) )
56 54 55 sylib 
 |-  ( ( # ` A ) e. NN -> ( # ` A ) e. ( ZZ>= ` 0 ) )
57 56 3ad2ant3 
 |-  ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) -> ( # ` A ) e. ( ZZ>= ` 0 ) )
58 8 57 syl 
 |-  ( U e. C -> ( # ` A ) e. ( ZZ>= ` 0 ) )
59 58 3ad2ant1 
 |-  ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> ( # ` A ) e. ( ZZ>= ` 0 ) )
60 fzisfzounsn 
 |-  ( ( # ` A ) e. ( ZZ>= ` 0 ) -> ( 0 ... ( # ` A ) ) = ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) )
61 59 60 syl 
 |-  ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> ( 0 ... ( # ` A ) ) = ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) )
62 53 61 raleqtrrdv 
 |-  ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> A. i e. ( 0 ... ( # ` A ) ) ( B ` i ) = ( E ` i ) )