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	164 181	raleqtrrdv	|- ( ( ( ( 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 ) )