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 \in Word Vtx (G) \land A \neq \emptyset) \land \forall i \in (0 ..^\|A\| - 1) \{A (i), A (i + 1)\} \in Edg (G) \land \{lastS (A), A (0)\} \in Edg (G)) \land ((B \in Word Vtx (G) \land B \neq \emptyset) \land \forall j \in (0 ..^\|B\| - 1) \{B (j), B (j + 1)\} \in Edg (G) \land \{lastS (B), B (0)\} \in Edg (G)) \land A (0) = B (0)) \to \forall i \in (0 ..^\|A ++ B\| - 1) \{(A ++ B) (i), (A ++ B) (i + 1)\} \in Edg (G)$

Proof

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

Metamath Proof Explorer

Theorem clwwlkccatlem

Proof