Metamath Proof Explorer


Theorem clwwlkccatlem

Description: Lemma for clwwlkccat : index j is shifted up by ( #A ) , and the case i = ( ( #A ) - 1 ) is covered by the "bridge" { ( lastSA ) , ( B0 ) } = { ( lastSA ) , ( A0 ) } e. ( EdgG ) . (Contributed by AV, 23-Apr-2022)

Ref Expression
Assertion clwwlkccatlem
|- ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( 0 ..^ ( ( # ` ( A ++ B ) ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )

Proof

Step Hyp Ref Expression
1 simplll
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> A e. Word ( Vtx ` G ) )
2 simplr
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> B e. Word ( Vtx ` G ) )
3 lencl
 |-  ( A e. Word ( Vtx ` G ) -> ( # ` A ) e. NN0 )
4 3 nn0zd
 |-  ( A e. Word ( Vtx ` G ) -> ( # ` A ) e. ZZ )
5 fzossrbm1
 |-  ( ( # ` A ) e. ZZ -> ( 0 ..^ ( ( # ` A ) - 1 ) ) C_ ( 0 ..^ ( # ` A ) ) )
6 4 5 syl
 |-  ( A e. Word ( Vtx ` G ) -> ( 0 ..^ ( ( # ` A ) - 1 ) ) C_ ( 0 ..^ ( # ` A ) ) )
7 6 ad2antrr
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) -> ( 0 ..^ ( ( # ` A ) - 1 ) ) C_ ( 0 ..^ ( # ` A ) ) )
8 7 sselda
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> i e. ( 0 ..^ ( # ` A ) ) )
9 ccatval1
 |-  ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) /\ i e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` i ) = ( A ` i ) )
10 1 2 8 9 syl3anc
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( A ++ B ) ` i ) = ( A ` i ) )
11 4 ad2antrr
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) -> ( # ` A ) e. ZZ )
12 elfzom1elp1fzo
 |-  ( ( ( # ` A ) e. ZZ /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` A ) ) )
13 11 12 sylan
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` A ) ) )
14 ccatval1
 |-  ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) /\ ( i + 1 ) e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ B ) ` ( i + 1 ) ) = ( A ` ( i + 1 ) ) )
15 1 2 13 14 syl3anc
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( ( A ++ B ) ` ( i + 1 ) ) = ( A ` ( i + 1 ) ) )
16 10 15 preq12d
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } = { ( A ` i ) , ( A ` ( i + 1 ) ) } )
17 16 eleq1d
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
18 17 biimprd
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) /\ i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) ) -> ( { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
19 18 ralimdva
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ B e. Word ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
20 19 impancom
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( B e. Word ( Vtx ` G ) -> A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
21 20 3adant3
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> ( B e. Word ( Vtx ` G ) -> A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
22 21 com12
 |-  ( B e. Word ( Vtx ` G ) -> ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
23 22 adantr
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
24 23 3ad2ant1
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) -> ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
25 24 impcom
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) ) -> A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
26 25 3adant3
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
27 simprl
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> A e. Word ( Vtx ` G ) )
28 simpll
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> B e. Word ( Vtx ` G ) )
29 simprr
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> A =/= (/) )
30 ccatval1lsw
 |-  ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) = ( lastS ` A ) )
31 27 28 29 30 syl3anc
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) = ( lastS ` A ) )
32 31 adantr
 |-  ( ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) = ( lastS ` A ) )
33 3 nn0cnd
 |-  ( A e. Word ( Vtx ` G ) -> ( # ` A ) e. CC )
34 npcan1
 |-  ( ( # ` A ) e. CC -> ( ( ( # ` A ) - 1 ) + 1 ) = ( # ` A ) )
35 33 34 syl
 |-  ( A e. Word ( Vtx ` G ) -> ( ( ( # ` A ) - 1 ) + 1 ) = ( # ` A ) )
36 35 ad2antrl
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> ( ( ( # ` A ) - 1 ) + 1 ) = ( # ` A ) )
37 36 fveq2d
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) = ( ( A ++ B ) ` ( # ` A ) ) )
38 simplr
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> B =/= (/) )
39 ccatval21sw
 |-  ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( ( A ++ B ) ` ( # ` A ) ) = ( B ` 0 ) )
40 27 28 38 39 syl3anc
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> ( ( A ++ B ) ` ( # ` A ) ) = ( B ` 0 ) )
41 37 40 eqtrd
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) = ( B ` 0 ) )
42 41 adantr
 |-  ( ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) = ( B ` 0 ) )
43 simpr
 |-  ( ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ` 0 ) = ( B ` 0 ) )
44 42 43 eqtr4d
 |-  ( ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) = ( A ` 0 ) )
45 32 44 preq12d
 |-  ( ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } = { ( lastS ` A ) , ( A ` 0 ) } )
46 45 eleq1d
 |-  ( ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) <-> { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) )
47 46 exbiri
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> ( { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) -> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) ) )
48 47 com23
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) ) -> ( { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) -> ( ( A ` 0 ) = ( B ` 0 ) -> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) ) )
49 48 expimpd
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) ) )
50 49 3ad2ant1
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) -> ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) ) )
51 50 com12
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) ) )
52 51 3adant2
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) ) )
53 52 3imp
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) )
54 ralunb
 |-  ( A. i e. ( ( 0 ..^ ( ( # ` A ) - 1 ) ) u. { ( ( # ` A ) - 1 ) } ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( ( # ` A ) - 1 ) } { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
55 ovex
 |-  ( ( # ` A ) - 1 ) e. _V
56 fveq2
 |-  ( i = ( ( # ` A ) - 1 ) -> ( ( A ++ B ) ` i ) = ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) )
57 fvoveq1
 |-  ( i = ( ( # ` A ) - 1 ) -> ( ( A ++ B ) ` ( i + 1 ) ) = ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) )
58 56 57 preq12d
 |-  ( i = ( ( # ` A ) - 1 ) -> { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } = { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } )
59 58 eleq1d
 |-  ( i = ( ( # ` A ) - 1 ) -> ( { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
60 55 59 ralsn
 |-  ( A. i e. { ( ( # ` A ) - 1 ) } { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) )
61 60 anbi2i
 |-  ( ( A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. { ( ( # ` A ) - 1 ) } { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) <-> ( A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
62 54 61 bitri
 |-  ( A. i e. ( ( 0 ..^ ( ( # ` A ) - 1 ) ) u. { ( ( # ` A ) - 1 ) } ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) , ( ( A ++ B ) ` ( ( ( # ` A ) - 1 ) + 1 ) ) } e. ( Edg ` G ) ) )
63 26 53 62 sylanbrc
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( ( 0 ..^ ( ( # ` A ) - 1 ) ) u. { ( ( # ` A ) - 1 ) } ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
64 0z
 |-  0 e. ZZ
65 lennncl
 |-  ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( # ` A ) e. NN )
66 0p1e1
 |-  ( 0 + 1 ) = 1
67 66 fveq2i
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
68 67 eleq2i
 |-  ( ( # ` A ) e. ( ZZ>= ` ( 0 + 1 ) ) <-> ( # ` A ) e. ( ZZ>= ` 1 ) )
69 elnnuz
 |-  ( ( # ` A ) e. NN <-> ( # ` A ) e. ( ZZ>= ` 1 ) )
70 68 69 bitr4i
 |-  ( ( # ` A ) e. ( ZZ>= ` ( 0 + 1 ) ) <-> ( # ` A ) e. NN )
71 65 70 sylibr
 |-  ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( # ` A ) e. ( ZZ>= ` ( 0 + 1 ) ) )
72 fzosplitsnm1
 |-  ( ( 0 e. ZZ /\ ( # ` A ) e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( 0 ..^ ( # ` A ) ) = ( ( 0 ..^ ( ( # ` A ) - 1 ) ) u. { ( ( # ` A ) - 1 ) } ) )
73 64 71 72 sylancr
 |-  ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( 0 ..^ ( # ` A ) ) = ( ( 0 ..^ ( ( # ` A ) - 1 ) ) u. { ( ( # ` A ) - 1 ) } ) )
74 73 raleqdv
 |-  ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( ( 0 ..^ ( ( # ` A ) - 1 ) ) u. { ( ( # ` A ) - 1 ) } ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
75 74 3ad2ant1
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( ( 0 ..^ ( ( # ` A ) - 1 ) ) u. { ( ( # ` A ) - 1 ) } ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
76 75 3ad2ant1
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A. i e. ( 0 ..^ ( # ` A ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( ( 0 ..^ ( ( # ` A ) - 1 ) ) u. { ( ( # ` A ) - 1 ) } ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
77 63 76 mpbird
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( 0 ..^ ( # ` A ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
78 lencl
 |-  ( B e. Word ( Vtx ` G ) -> ( # ` B ) e. NN0 )
79 78 nn0zd
 |-  ( B e. Word ( Vtx ` G ) -> ( # ` B ) e. ZZ )
80 peano2zm
 |-  ( ( # ` B ) e. ZZ -> ( ( # ` B ) - 1 ) e. ZZ )
81 79 80 syl
 |-  ( B e. Word ( Vtx ` G ) -> ( ( # ` B ) - 1 ) e. ZZ )
82 81 ad2antrl
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` B ) - 1 ) e. ZZ )
83 82 adantr
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( ( # ` B ) - 1 ) e. ZZ )
84 83 anim1ci
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) /\ ( ( # ` B ) - 1 ) e. ZZ ) )
85 fzosubel3
 |-  ( ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) /\ ( ( # ` B ) - 1 ) e. ZZ ) -> ( i - ( # ` A ) ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
86 fveq2
 |-  ( j = ( i - ( # ` A ) ) -> ( B ` j ) = ( B ` ( i - ( # ` A ) ) ) )
87 fvoveq1
 |-  ( j = ( i - ( # ` A ) ) -> ( B ` ( j + 1 ) ) = ( B ` ( ( i - ( # ` A ) ) + 1 ) ) )
88 86 87 preq12d
 |-  ( j = ( i - ( # ` A ) ) -> { ( B ` j ) , ( B ` ( j + 1 ) ) } = { ( B ` ( i - ( # ` A ) ) ) , ( B ` ( ( i - ( # ` A ) ) + 1 ) ) } )
89 88 eleq1d
 |-  ( j = ( i - ( # ` A ) ) -> ( { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) <-> { ( B ` ( i - ( # ` A ) ) ) , ( B ` ( ( i - ( # ` A ) ) + 1 ) ) } e. ( Edg ` G ) ) )
90 89 rspcv
 |-  ( ( i - ( # ` A ) ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) -> ( A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) -> { ( B ` ( i - ( # ` A ) ) ) , ( B ` ( ( i - ( # ` A ) ) + 1 ) ) } e. ( Edg ` G ) ) )
91 84 85 90 3syl
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) -> { ( B ` ( i - ( # ` A ) ) ) , ( B ` ( ( i - ( # ` A ) ) + 1 ) ) } e. ( Edg ` G ) ) )
92 simp-4l
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> A e. Word ( Vtx ` G ) )
93 simprl
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> B e. Word ( Vtx ` G ) )
94 93 ad2antrr
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> B e. Word ( Vtx ` G ) )
95 3 adantr
 |-  ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( # ` A ) e. NN0 )
96 78 adantr
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( # ` B ) e. NN0 )
97 nn0addcl
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( ( # ` A ) + ( # ` B ) ) e. NN0 )
98 97 nn0zd
 |-  ( ( ( # ` A ) e. NN0 /\ ( # ` B ) e. NN0 ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
99 95 96 98 syl2an
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
100 1nn0
 |-  1 e. NN0
101 eluzmn
 |-  ( ( ( ( # ` A ) + ( # ` B ) ) e. ZZ /\ 1 e. NN0 ) -> ( ( # ` A ) + ( # ` B ) ) e. ( ZZ>= ` ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) )
102 99 100 101 sylancl
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` A ) + ( # ` B ) ) e. ( ZZ>= ` ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) )
103 33 ad2antrr
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( # ` A ) e. CC )
104 78 nn0cnd
 |-  ( B e. Word ( Vtx ` G ) -> ( # ` B ) e. CC )
105 104 ad2antrl
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( # ` B ) e. CC )
106 1cnd
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> 1 e. CC )
107 103 105 106 addsubassd
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( ( # ` A ) + ( # ` B ) ) - 1 ) = ( ( # ` A ) + ( ( # ` B ) - 1 ) ) )
108 107 fveq2d
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ZZ>= ` ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) = ( ZZ>= ` ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) )
109 102 108 eleqtrd
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` A ) + ( # ` B ) ) e. ( ZZ>= ` ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) )
110 fzoss2
 |-  ( ( ( # ` A ) + ( # ` B ) ) e. ( ZZ>= ` ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) -> ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) C_ ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
111 109 110 syl
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) C_ ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
112 111 adantr
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) C_ ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
113 112 sselda
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
114 ccatval2
 |-  ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) ` i ) = ( B ` ( i - ( # ` A ) ) ) )
115 92 94 113 114 syl3anc
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( ( A ++ B ) ` i ) = ( B ` ( i - ( # ` A ) ) ) )
116 107 oveq2d
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` A ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) = ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) )
117 116 eleq2d
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( i e. ( ( # ` A ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) <-> i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) )
118 117 adantr
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( i e. ( ( # ` A ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) <-> i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) )
119 eluzmn
 |-  ( ( ( # ` A ) e. ZZ /\ 1 e. NN0 ) -> ( # ` A ) e. ( ZZ>= ` ( ( # ` A ) - 1 ) ) )
120 4 100 119 sylancl
 |-  ( A e. Word ( Vtx ` G ) -> ( # ` A ) e. ( ZZ>= ` ( ( # ` A ) - 1 ) ) )
121 120 ad3antrrr
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( # ` A ) e. ( ZZ>= ` ( ( # ` A ) - 1 ) ) )
122 fzoss1
 |-  ( ( # ` A ) e. ( ZZ>= ` ( ( # ` A ) - 1 ) ) -> ( ( # ` A ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) C_ ( ( ( # ` A ) - 1 ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) )
123 121 122 syl
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( ( # ` A ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) C_ ( ( ( # ` A ) - 1 ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) )
124 123 sseld
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( i e. ( ( # ` A ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) -> i e. ( ( ( # ` A ) - 1 ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) ) )
125 118 124 sylbird
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) -> i e. ( ( ( # ` A ) - 1 ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) ) )
126 125 imp
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> i e. ( ( ( # ` A ) - 1 ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) )
127 4 adantr
 |-  ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( # ` A ) e. ZZ )
128 79 adantr
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( # ` B ) e. ZZ )
129 simpl
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( # ` A ) e. ZZ )
130 zaddcl
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( # ` A ) + ( # ` B ) ) e. ZZ )
131 129 130 jca
 |-  ( ( ( # ` A ) e. ZZ /\ ( # ` B ) e. ZZ ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ ) )
132 127 128 131 syl2an
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ ) )
133 132 adantr
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ ) )
134 elfzoelz
 |-  ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) -> i e. ZZ )
135 1zzd
 |-  ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) -> 1 e. ZZ )
136 134 135 jca
 |-  ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) -> ( i e. ZZ /\ 1 e. ZZ ) )
137 elfzomelpfzo
 |-  ( ( ( ( # ` A ) e. ZZ /\ ( ( # ` A ) + ( # ` B ) ) e. ZZ ) /\ ( i e. ZZ /\ 1 e. ZZ ) ) -> ( i e. ( ( ( # ` A ) - 1 ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) <-> ( i + 1 ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) )
138 133 136 137 syl2an
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( i e. ( ( ( # ` A ) - 1 ) ..^ ( ( ( # ` A ) + ( # ` B ) ) - 1 ) ) <-> ( i + 1 ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) )
139 126 138 mpbid
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( i + 1 ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
140 ccatval2
 |-  ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) /\ ( i + 1 ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) ` ( i + 1 ) ) = ( B ` ( ( i + 1 ) - ( # ` A ) ) ) )
141 92 94 139 140 syl3anc
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( ( A ++ B ) ` ( i + 1 ) ) = ( B ` ( ( i + 1 ) - ( # ` A ) ) ) )
142 134 zcnd
 |-  ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) -> i e. CC )
143 142 adantl
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> i e. CC )
144 1cnd
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> 1 e. CC )
145 103 ad2antrr
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( # ` A ) e. CC )
146 143 144 145 addsubd
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( ( i + 1 ) - ( # ` A ) ) = ( ( i - ( # ` A ) ) + 1 ) )
147 146 fveq2d
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( B ` ( ( i + 1 ) - ( # ` A ) ) ) = ( B ` ( ( i - ( # ` A ) ) + 1 ) ) )
148 141 147 eqtrd
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( ( A ++ B ) ` ( i + 1 ) ) = ( B ` ( ( i - ( # ` A ) ) + 1 ) ) )
149 115 148 preq12d
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } = { ( B ` ( i - ( # ` A ) ) ) , ( B ` ( ( i - ( # ` A ) ) + 1 ) ) } )
150 149 eleq1d
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( B ` ( i - ( # ` A ) ) ) , ( B ` ( ( i - ( # ` A ) ) + 1 ) ) } e. ( Edg ` G ) ) )
151 91 150 sylibrd
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) -> ( A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) -> { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
152 151 impancom
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) ) -> ( i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) -> { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
153 152 ralrimiv
 |-  ( ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
154 153 exp31
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> ( A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
155 154 expcom
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> ( A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) )
156 155 com23
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) )
157 156 com24
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) -> ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) )
158 157 imp
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) ) -> ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
159 158 3adant3
 |-  ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) -> ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
160 159 com12
 |-  ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
161 160 3ad2ant1
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) -> ( ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) -> ( ( A ` 0 ) = ( B ` 0 ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) )
162 161 3imp
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
163 ralunb
 |-  ( A. i e. ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( A. i e. ( 0 ..^ ( # ` A ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) /\ A. i e. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
164 77 162 163 sylanbrc
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )
165 ccatlen
 |-  ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
166 165 oveq1d
 |-  ( ( A e. Word ( Vtx ` G ) /\ B e. Word ( Vtx ` G ) ) -> ( ( # ` ( A ++ B ) ) - 1 ) = ( ( ( # ` A ) + ( # ` B ) ) - 1 ) )
167 166 ad2ant2r
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` ( A ++ B ) ) - 1 ) = ( ( ( # ` A ) + ( # ` B ) ) - 1 ) )
168 167 107 eqtrd
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( ( # ` ( A ++ B ) ) - 1 ) = ( ( # ` A ) + ( ( # ` B ) - 1 ) ) )
169 168 oveq2d
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( 0 ..^ ( ( # ` ( A ++ B ) ) - 1 ) ) = ( 0 ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) )
170 elnn0uz
 |-  ( ( # ` A ) e. NN0 <-> ( # ` A ) e. ( ZZ>= ` 0 ) )
171 3 170 sylib
 |-  ( A e. Word ( Vtx ` G ) -> ( # ` A ) e. ( ZZ>= ` 0 ) )
172 171 adantr
 |-  ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) -> ( # ` A ) e. ( ZZ>= ` 0 ) )
173 lennncl
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( # ` B ) e. NN )
174 nnm1nn0
 |-  ( ( # ` B ) e. NN -> ( ( # ` B ) - 1 ) e. NN0 )
175 173 174 syl
 |-  ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) -> ( ( # ` B ) - 1 ) e. NN0 )
176 fzoun
 |-  ( ( ( # ` A ) e. ( ZZ>= ` 0 ) /\ ( ( # ` B ) - 1 ) e. NN0 ) -> ( 0 ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) = ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) )
177 172 175 176 syl2an
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( 0 ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) = ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) )
178 169 177 eqtrd
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) ) -> ( 0 ..^ ( ( # ` ( A ++ B ) ) - 1 ) ) = ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) )
179 178 3ad2antr1
 |-  ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) ) -> ( 0 ..^ ( ( # ` ( A ++ B ) ) - 1 ) ) = ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) )
180 179 3ad2antl1
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) ) -> ( 0 ..^ ( ( # ` ( A ++ B ) ) - 1 ) ) = ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) )
181 180 3adant3
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( 0 ..^ ( ( # ` ( A ++ B ) ) - 1 ) ) = ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) )
182 181 raleqdv
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A. i e. ( 0 ..^ ( ( # ` ( A ++ B ) ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( ( 0 ..^ ( # ` A ) ) u. ( ( # ` A ) ..^ ( ( # ` A ) + ( ( # ` B ) - 1 ) ) ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
183 164 182 mpbird
 |-  ( ( ( ( A e. Word ( Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` A ) , ( A ` 0 ) } e. ( Edg ` G ) ) /\ ( ( B e. Word ( Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` B ) , ( B ` 0 ) } e. ( Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( 0 ..^ ( ( # ` ( A ++ B ) ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. ( Edg ` G ) )