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 ) )