Metamath Proof Explorer

Theorem numclwwlk2lem1lem

Description: Lemma for numclwwlk2lem1 . (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 27-May-2021) (Revised by AV, 15-Mar-2022)

Ref Expression
Assertion numclwwlk2lem1lem 
|- ( ( X e. ( Vtx ` G ) /\ W e. ( N WWalksN G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) -> ( ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" X "> ) ` N ) =/= ( W ` 0 ) ) )

Proof

Step Hyp Ref Expression
1 wwlknbp1 
 |-  ( W e. ( N WWalksN G ) -> ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) )
2 simpl2 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ ( X e. ( Vtx ` G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) -> W e. Word ( Vtx ` G ) )
3 s1cl 
 |-  ( X e. ( Vtx ` G ) -> <" X "> e. Word ( Vtx ` G ) )
4 3 ad2antrl 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ ( X e. ( Vtx ` G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) -> <" X "> e. Word ( Vtx ` G ) )
5 nn0p1gt0 
 |-  ( N e. NN0 -> 0 < ( N + 1 ) )
6 5 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> 0 < ( N + 1 ) )
7 6 adantr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ ( X e. ( Vtx ` G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) -> 0 < ( N + 1 ) )
8 breq2 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) )
9 8 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) )
10 9 adantr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ ( X e. ( Vtx ` G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) )
11 7 10 mpbird 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ ( X e. ( Vtx ` G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) -> 0 < ( # ` W ) )
12 ccatfv0 
 |-  ( ( W e. Word ( Vtx ` G ) /\ <" X "> e. Word ( Vtx ` G ) /\ 0 < ( # ` W ) ) -> ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) )
13 2 4 11 12 syl3anc 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ ( X e. ( Vtx ` G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) -> ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) )
14 oveq1 
 |-  ( ( # ` W ) = ( N + 1 ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
15 14 3ad2ant3 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( # ` W ) - 1 ) = ( ( N + 1 ) - 1 ) )
16 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
17 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
18 16 17 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
19 18 3ad2ant1 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( ( N + 1 ) - 1 ) = N )
20 15 19 eqtr2d 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> N = ( ( # ` W ) - 1 ) )
21 20 adantr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> N = ( ( # ` W ) - 1 ) )
22 21 fveq2d 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> ( ( W ++ <" X "> ) ` N ) = ( ( W ++ <" X "> ) ` ( ( # ` W ) - 1 ) ) )
23 simpl2 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> W e. Word ( Vtx ` G ) )
24 3 adantl 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> <" X "> e. Word ( Vtx ` G ) )
25 6 adantr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> 0 < ( N + 1 ) )
26 9 adantr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> ( 0 < ( # ` W ) <-> 0 < ( N + 1 ) ) )
27 25 26 mpbird 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> 0 < ( # ` W ) )
28 hashneq0 
 |-  ( W e. Word ( Vtx ` G ) -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
29 28 bicomd 
 |-  ( W e. Word ( Vtx ` G ) -> ( W =/= (/) <-> 0 < ( # ` W ) ) )
30 29 3ad2ant2 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( W =/= (/) <-> 0 < ( # ` W ) ) )
31 30 adantr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> ( W =/= (/) <-> 0 < ( # ` W ) ) )
32 27 31 mpbird 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> W =/= (/) )
33 ccatval1lsw 
 |-  ( ( W e. Word ( Vtx ` G ) /\ <" X "> e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( ( W ++ <" X "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
34 23 24 32 33 syl3anc 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> ( ( W ++ <" X "> ) ` ( ( # ` W ) - 1 ) ) = ( lastS ` W ) )
35 22 34 eqtr2d 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> ( lastS ` W ) = ( ( W ++ <" X "> ) ` N ) )
36 35 neeq1d 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> ( ( lastS ` W ) =/= ( W ` 0 ) <-> ( ( W ++ <" X "> ) ` N ) =/= ( W ` 0 ) ) )
37 36 biimpd 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ X e. ( Vtx ` G ) ) -> ( ( lastS ` W ) =/= ( W ` 0 ) -> ( ( W ++ <" X "> ) ` N ) =/= ( W ` 0 ) ) )
38 37 impr 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ ( X e. ( Vtx ` G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) -> ( ( W ++ <" X "> ) ` N ) =/= ( W ` 0 ) )
39 13 38 jca 
 |-  ( ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) /\ ( X e. ( Vtx ` G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) ) -> ( ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" X "> ) ` N ) =/= ( W ` 0 ) ) )
40 39 exp32 
 |-  ( ( N e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( N + 1 ) ) -> ( X e. ( Vtx ` G ) -> ( ( lastS ` W ) =/= ( W ` 0 ) -> ( ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" X "> ) ` N ) =/= ( W ` 0 ) ) ) ) )
41 1 40 syl 
 |-  ( W e. ( N WWalksN G ) -> ( X e. ( Vtx ` G ) -> ( ( lastS ` W ) =/= ( W ` 0 ) -> ( ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" X "> ) ` N ) =/= ( W ` 0 ) ) ) ) )
42 41 3imp21 
 |-  ( ( X e. ( Vtx ` G ) /\ W e. ( N WWalksN G ) /\ ( lastS ` W ) =/= ( W ` 0 ) ) -> ( ( ( W ++ <" X "> ) ` 0 ) = ( W ` 0 ) /\ ( ( W ++ <" X "> ) ` N ) =/= ( W ` 0 ) ) )