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 
|- 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 clwlkclwwlkf1lem2 
|- ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> ( ( # ` A ) = ( # ` 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 clwlkclwwlkflem 
 |-  ( U e. C -> ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) )
7 1 4 5 clwlkclwwlkflem 
 |-  ( W e. C -> ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) )
8 6 7 anim12i 
 |-  ( ( U e. C /\ W e. C ) -> ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) )
9 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
10 9 wlkpwrd 
 |-  ( A ( Walks ` G ) B -> B e. Word ( Vtx ` G ) )
11 10 3ad2ant1 
 |-  ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) -> B e. Word ( Vtx ` G ) )
12 9 wlkpwrd 
 |-  ( D ( Walks ` G ) E -> E e. Word ( Vtx ` G ) )
13 12 3ad2ant1 
 |-  ( ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) -> E e. Word ( Vtx ` G ) )
14 11 13 anim12i 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) -> ( B e. Word ( Vtx ` G ) /\ E e. Word ( Vtx ` G ) ) )
15 nnnn0 
 |-  ( ( # ` A ) e. NN -> ( # ` A ) e. NN0 )
16 15 3ad2ant3 
 |-  ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) -> ( # ` A ) e. NN0 )
17 nnnn0 
 |-  ( ( # ` D ) e. NN -> ( # ` D ) e. NN0 )
18 17 3ad2ant3 
 |-  ( ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) -> ( # ` D ) e. NN0 )
19 16 18 anim12i 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) -> ( ( # ` A ) e. NN0 /\ ( # ` D ) e. NN0 ) )
20 wlklenvp1 
 |-  ( A ( Walks ` G ) B -> ( # ` B ) = ( ( # ` A ) + 1 ) )
21 nnre 
 |-  ( ( # ` A ) e. NN -> ( # ` A ) e. RR )
22 21 lep1d 
 |-  ( ( # ` A ) e. NN -> ( # ` A ) <_ ( ( # ` A ) + 1 ) )
23 breq2 
 |-  ( ( # ` B ) = ( ( # ` A ) + 1 ) -> ( ( # ` A ) <_ ( # ` B ) <-> ( # ` A ) <_ ( ( # ` A ) + 1 ) ) )
24 22 23 imbitrrid 
 |-  ( ( # ` B ) = ( ( # ` A ) + 1 ) -> ( ( # ` A ) e. NN -> ( # ` A ) <_ ( # ` B ) ) )
25 20 24 syl 
 |-  ( A ( Walks ` G ) B -> ( ( # ` A ) e. NN -> ( # ` A ) <_ ( # ` B ) ) )
26 25 a1d 
 |-  ( A ( Walks ` G ) B -> ( ( B ` 0 ) = ( B ` ( # ` A ) ) -> ( ( # ` A ) e. NN -> ( # ` A ) <_ ( # ` B ) ) ) )
27 26 3imp 
 |-  ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) -> ( # ` A ) <_ ( # ` B ) )
28 wlklenvp1 
 |-  ( D ( Walks ` G ) E -> ( # ` E ) = ( ( # ` D ) + 1 ) )
29 nnre 
 |-  ( ( # ` D ) e. NN -> ( # ` D ) e. RR )
30 29 lep1d 
 |-  ( ( # ` D ) e. NN -> ( # ` D ) <_ ( ( # ` D ) + 1 ) )
31 breq2 
 |-  ( ( # ` E ) = ( ( # ` D ) + 1 ) -> ( ( # ` D ) <_ ( # ` E ) <-> ( # ` D ) <_ ( ( # ` D ) + 1 ) ) )
32 30 31 imbitrrid 
 |-  ( ( # ` E ) = ( ( # ` D ) + 1 ) -> ( ( # ` D ) e. NN -> ( # ` D ) <_ ( # ` E ) ) )
33 28 32 syl 
 |-  ( D ( Walks ` G ) E -> ( ( # ` D ) e. NN -> ( # ` D ) <_ ( # ` E ) ) )
34 33 a1d 
 |-  ( D ( Walks ` G ) E -> ( ( E ` 0 ) = ( E ` ( # ` D ) ) -> ( ( # ` D ) e. NN -> ( # ` D ) <_ ( # ` E ) ) ) )
35 34 3imp 
 |-  ( ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) -> ( # ` D ) <_ ( # ` E ) )
36 27 35 anim12i 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) -> ( ( # ` A ) <_ ( # ` B ) /\ ( # ` D ) <_ ( # ` E ) ) )
37 14 19 36 3jca 
 |-  ( ( ( A ( Walks ` G ) B /\ ( B ` 0 ) = ( B ` ( # ` A ) ) /\ ( # ` A ) e. NN ) /\ ( D ( Walks ` G ) E /\ ( E ` 0 ) = ( E ` ( # ` D ) ) /\ ( # ` D ) e. NN ) ) -> ( ( B e. Word ( Vtx ` G ) /\ E e. Word ( Vtx ` G ) ) /\ ( ( # ` A ) e. NN0 /\ ( # ` D ) e. NN0 ) /\ ( ( # ` A ) <_ ( # ` B ) /\ ( # ` D ) <_ ( # ` E ) ) ) )
38 pfxeq 
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ E e. Word ( Vtx ` G ) ) /\ ( ( # ` A ) e. NN0 /\ ( # ` D ) e. NN0 ) /\ ( ( # ` A ) <_ ( # ` B ) /\ ( # ` D ) <_ ( # ` E ) ) ) -> ( ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) <-> ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) ) )
39 8 37 38 3syl 
 |-  ( ( U e. C /\ W e. C ) -> ( ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) <-> ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) ) )
40 39 biimp3a 
 |-  ( ( U e. C /\ W e. C /\ ( B prefix ( # ` A ) ) = ( E prefix ( # ` D ) ) ) -> ( ( # ` A ) = ( # ` D ) /\ A. i e. ( 0 ..^ ( # ` A ) ) ( B ` i ) = ( E ` i ) ) )