ccatass

Description: Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015)

		Ref	Expression
	Assertion	ccatass	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (S ++ T) ++ U = S ++ (T ++ U)$

Proof

Step	Hyp	Ref	Expression
1		ccatcl	$⊢ (S \in Word B \land T \in Word B) \to S ++ T \in Word B$
2		ccatcl	$⊢ (S ++ T \in Word B \land U \in Word B) \to (S ++ T) ++ U \in Word B$
3	1 2	stoic3	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (S ++ T) ++ U \in Word B$
4		wrdfn	$⊢ (S ++ T) ++ U \in Word B \to ((S ++ T) ++ U) Fn (0 ..^\|(S ++ T) ++ U\|)$
5	3 4	syl	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to ((S ++ T) ++ U) Fn (0 ..^\|(S ++ T) ++ U\|)$
6		ccatlen	$⊢ (S ++ T \in Word B \land U \in Word B) \to \|(S ++ T) ++ U\| = \|S ++ T\| + \|U\|$
7	1 6	stoic3	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|(S ++ T) ++ U\| = \|S ++ T\| + \|U\|$
8		ccatlen	$⊢ (S \in Word B \land T \in Word B) \to \|S ++ T\| = \|S\| + \|T\|$
9	8	3adant3	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S ++ T\| = \|S\| + \|T\|$
10	9	oveq1d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S ++ T\| + \|U\| = \|S\| + \|T\| + \|U\|$
11	7 10	eqtrd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|(S ++ T) ++ U\| = \|S\| + \|T\| + \|U\|$
12	11	oveq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (0 ..^\|(S ++ T) ++ U\|) = (0 ..^\|S\| + \|T\| + \|U\|)$
13	12	fneq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (((S ++ T) ++ U) Fn (0 ..^\|(S ++ T) ++ U\|) \leftrightarrow ((S ++ T) ++ U) Fn (0 ..^\|S\| + \|T\| + \|U\|))$
14	5 13	mpbid	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to ((S ++ T) ++ U) Fn (0 ..^\|S\| + \|T\| + \|U\|)$
15		simp1	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to S \in Word B$
16		ccatcl	$⊢ (T \in Word B \land U \in Word B) \to T ++ U \in Word B$
17	16	3adant1	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to T ++ U \in Word B$
18		ccatcl	$⊢ (S \in Word B \land T ++ U \in Word B) \to S ++ (T ++ U) \in Word B$
19	15 17 18	syl2anc	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to S ++ (T ++ U) \in Word B$
20		wrdfn	$⊢ S ++ (T ++ U) \in Word B \to (S ++ (T ++ U)) Fn (0 ..^\|S ++ (T ++ U)\|)$
21	19 20	syl	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (S ++ (T ++ U)) Fn (0 ..^\|S ++ (T ++ U)\|)$
22		ccatlen	$⊢ (T \in Word B \land U \in Word B) \to \|T ++ U\| = \|T\| + \|U\|$
23	22	3adant1	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|T ++ U\| = \|T\| + \|U\|$
24	23	oveq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| + \|T ++ U\| = \|S\| + \|T\| + \|U\|$
25		ccatlen	$⊢ (S \in Word B \land T ++ U \in Word B) \to \|S ++ (T ++ U)\| = \|S\| + \|T ++ U\|$
26	15 17 25	syl2anc	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S ++ (T ++ U)\| = \|S\| + \|T ++ U\|$
27		lencl	$⊢ S \in Word B \to \|S\| \in ℕ_{0}$
28	27	3ad2ant1	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| \in ℕ_{0}$
29	28	nn0cnd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| \in ℂ$
30		lencl	$⊢ T \in Word B \to \|T\| \in ℕ_{0}$
31	30	3ad2ant2	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|T\| \in ℕ_{0}$
32	31	nn0cnd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|T\| \in ℂ$
33		lencl	$⊢ U \in Word B \to \|U\| \in ℕ_{0}$
34	33	3ad2ant3	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|U\| \in ℕ_{0}$
35	34	nn0cnd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|U\| \in ℂ$
36	29 32 35	addassd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| + \|T\| + \|U\| = \|S\| + \|T\| + \|U\|$
37	24 26 36	3eqtr4d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S ++ (T ++ U)\| = \|S\| + \|T\| + \|U\|$
38	37	oveq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (0 ..^\|S ++ (T ++ U)\|) = (0 ..^\|S\| + \|T\| + \|U\|)$
39	38	fneq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to ((S ++ (T ++ U)) Fn (0 ..^\|S ++ (T ++ U)\|) \leftrightarrow (S ++ (T ++ U)) Fn (0 ..^\|S\| + \|T\| + \|U\|))$
40	21 39	mpbid	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (S ++ (T ++ U)) Fn (0 ..^\|S\| + \|T\| + \|U\|)$
41	28	nn0zd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| \in ℤ$
42		fzospliti	$⊢ (x \in (0 ..^\|S\| + \|T\| + \|U\|) \land \|S\| \in ℤ) \to (x \in (0 ..^\|S\|) \lor x \in (\|S\| ..^\|S\| + \|T\| + \|U\|))$
43	42	ex	$⊢ x \in (0 ..^\|S\| + \|T\| + \|U\|) \to (\|S\| \in ℤ \to (x \in (0 ..^\|S\|) \lor x \in (\|S\| ..^\|S\| + \|T\| + \|U\|)))$
44	41 43	mpan9	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\| + \|T\| + \|U\|)) \to (x \in (0 ..^\|S\|) \lor x \in (\|S\| ..^\|S\| + \|T\| + \|U\|))$
45		simp2	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to T \in Word B$
46		id	$⊢ x \in (0 ..^\|S\|) \to x \in (0 ..^\|S\|)$
47		ccatval1	$⊢ (S \in Word B \land T \in Word B \land x \in (0 ..^\|S\|)) \to (S ++ T) (x) = S (x)$
48	15 45 46 47	syl2an3an	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\|)) \to (S ++ T) (x) = S (x)$
49	1	3adant3	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to S ++ T \in Word B$
50	49	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\|)) \to S ++ T \in Word B$
51		simpl3	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\|)) \to U \in Word B$
52	41	uzidd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| \in ℤ_{\geq \|S\|}$
53		uzaddcl	$⊢ (\|S\| \in ℤ_{\geq \|S\|} \land \|T\| \in ℕ_{0}) \to \|S\| + \|T\| \in ℤ_{\geq \|S\|}$
54	52 31 53	syl2anc	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| + \|T\| \in ℤ_{\geq \|S\|}$
55		fzoss2	$⊢ \|S\| + \|T\| \in ℤ_{\geq \|S\|} \to (0 ..^\|S\|) \subseteq (0 ..^\|S\| + \|T\|)$
56	54 55	syl	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (0 ..^\|S\|) \subseteq (0 ..^\|S\| + \|T\|)$
57	9	oveq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (0 ..^\|S ++ T\|) = (0 ..^\|S\| + \|T\|)$
58	56 57	sseqtrrd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (0 ..^\|S\|) \subseteq (0 ..^\|S ++ T\|)$
59	58	sselda	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\|)) \to x \in (0 ..^\|S ++ T\|)$
60		ccatval1	$⊢ (S ++ T \in Word B \land U \in Word B \land x \in (0 ..^\|S ++ T\|)) \to ((S ++ T) ++ U) (x) = (S ++ T) (x)$
61	50 51 59 60	syl3anc	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\|)) \to ((S ++ T) ++ U) (x) = (S ++ T) (x)$
62		ccatval1	$⊢ (S \in Word B \land T ++ U \in Word B \land x \in (0 ..^\|S\|)) \to (S ++ (T ++ U)) (x) = S (x)$
63	15 17 46 62	syl2an3an	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\|)) \to (S ++ (T ++ U)) (x) = S (x)$
64	48 61 63	3eqtr4d	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\|)) \to ((S ++ T) ++ U) (x) = (S ++ (T ++ U)) (x)$
65	31	nn0zd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|T\| \in ℤ$
66	41 65	zaddcld	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| + \|T\| \in ℤ$
67		fzospliti	$⊢ (x \in (\|S\| ..^\|S\| + \|T\| + \|U\|) \land \|S\| + \|T\| \in ℤ) \to (x \in (\|S\| ..^\|S\| + \|T\|) \lor x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|))$
68	67	ex	$⊢ x \in (\|S\| ..^\|S\| + \|T\| + \|U\|) \to (\|S\| + \|T\| \in ℤ \to (x \in (\|S\| ..^\|S\| + \|T\|) \lor x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)))$
69	66 68	mpan9	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\| + \|U\|)) \to (x \in (\|S\| ..^\|S\| + \|T\|) \lor x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|))$
70		id	$⊢ x \in (\|S\| ..^\|S\| + \|T\|) \to x \in (\|S\| ..^\|S\| + \|T\|)$
71		ccatval2	$⊢ (S \in Word B \land T \in Word B \land x \in (\|S\| ..^\|S\| + \|T\|)) \to (S ++ T) (x) = T (x - \|S\|)$
72	15 45 70 71	syl2an3an	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to (S ++ T) (x) = T (x - \|S\|)$
73		simpl2	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to T \in Word B$
74		simpl3	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to U \in Word B$
75		fzosubel3	$⊢ (x \in (\|S\| ..^\|S\| + \|T\|) \land \|T\| \in ℤ) \to x - \|S\| \in (0 ..^\|T\|)$
76	75	ex	$⊢ x \in (\|S\| ..^\|S\| + \|T\|) \to (\|T\| \in ℤ \to x - \|S\| \in (0 ..^\|T\|))$
77	65 76	mpan9	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to x - \|S\| \in (0 ..^\|T\|)$
78		ccatval1	$⊢ (T \in Word B \land U \in Word B \land x - \|S\| \in (0 ..^\|T\|)) \to (T ++ U) (x - \|S\|) = T (x - \|S\|)$
79	73 74 77 78	syl3anc	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to (T ++ U) (x - \|S\|) = T (x - \|S\|)$
80	72 79	eqtr4d	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to (S ++ T) (x) = (T ++ U) (x - \|S\|)$
81	49	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to S ++ T \in Word B$
82		fzoss1	$⊢ \|S\| \in ℤ_{\geq 0} \to (\|S\| ..^\|S\| + \|T\|) \subseteq (0 ..^\|S\| + \|T\|)$
83		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
84	82 83	eleq2s	$⊢ \|S\| \in ℕ_{0} \to (\|S\| ..^\|S\| + \|T\|) \subseteq (0 ..^\|S\| + \|T\|)$
85	28 84	syl	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| ..^\|S\| + \|T\|) \subseteq (0 ..^\|S\| + \|T\|)$
86	85 57	sseqtrrd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| ..^\|S\| + \|T\|) \subseteq (0 ..^\|S ++ T\|)$
87	86	sselda	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to x \in (0 ..^\|S ++ T\|)$
88	81 74 87 60	syl3anc	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to ((S ++ T) ++ U) (x) = (S ++ T) (x)$
89		simpl1	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to S \in Word B$
90	17	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to T ++ U \in Word B$
91	66	uzidd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| + \|T\| \in ℤ_{\geq (\|S\| + \|T\|)}$
92		uzaddcl	$⊢ (\|S\| + \|T\| \in ℤ_{\geq (\|S\| + \|T\|)} \land \|U\| \in ℕ_{0}) \to \|S\| + \|T\| + \|U\| \in ℤ_{\geq (\|S\| + \|T\|)}$
93	91 34 92	syl2anc	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| + \|T\| + \|U\| \in ℤ_{\geq (\|S\| + \|T\|)}$
94		fzoss2	$⊢ \|S\| + \|T\| + \|U\| \in ℤ_{\geq (\|S\| + \|T\|)} \to (\|S\| ..^\|S\| + \|T\|) \subseteq (\|S\| ..^\|S\| + \|T\| + \|U\|)$
95	93 94	syl	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| ..^\|S\| + \|T\|) \subseteq (\|S\| ..^\|S\| + \|T\| + \|U\|)$
96	24 36	eqtr4d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|S\| + \|T ++ U\| = \|S\| + \|T\| + \|U\|$
97	96	oveq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| ..^\|S\| + \|T ++ U\|) = (\|S\| ..^\|S\| + \|T\| + \|U\|)$
98	95 97	sseqtrrd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| ..^\|S\| + \|T\|) \subseteq (\|S\| ..^\|S\| + \|T ++ U\|)$
99	98	sselda	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to x \in (\|S\| ..^\|S\| + \|T ++ U\|)$
100		ccatval2	$⊢ (S \in Word B \land T ++ U \in Word B \land x \in (\|S\| ..^\|S\| + \|T ++ U\|)) \to (S ++ (T ++ U)) (x) = (T ++ U) (x - \|S\|)$
101	89 90 99 100	syl3anc	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to (S ++ (T ++ U)) (x) = (T ++ U) (x - \|S\|)$
102	80 88 101	3eqtr4d	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\|)) \to ((S ++ T) ++ U) (x) = (S ++ (T ++ U)) (x)$
103	9	oveq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to x - \|S ++ T\| = x - (\|S\| + \|T\|)$
104	103	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to x - \|S ++ T\| = x - (\|S\| + \|T\|)$
105		elfzoelz	$⊢ x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|) \to x \in ℤ$
106	105	zcnd	$⊢ x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|) \to x \in ℂ$
107	106	adantl	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to x \in ℂ$
108	29	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to \|S\| \in ℂ$
109	32	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to \|T\| \in ℂ$
110	107 108 109	subsub4d	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to x - \|S\| - \|T\| = x - (\|S\| + \|T\|)$
111	104 110	eqtr4d	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to x - \|S ++ T\| = x - \|S\| - \|T\|$
112	111	fveq2d	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to U (x - \|S ++ T\|) = U (x - \|S\| - \|T\|)$
113		simpl2	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to T \in Word B$
114		simpl3	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to U \in Word B$
115	36	oveq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|) = (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)$
116	115	eleq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|) \leftrightarrow x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|))$
117	116	biimpa	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)$
118	34	nn0zd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|U\| \in ℤ$
119	65 118	zaddcld	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to \|T\| + \|U\| \in ℤ$
120	41 65 119	3jca	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| \in ℤ \land \|T\| \in ℤ \land \|T\| + \|U\| \in ℤ)$
121	120	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to (\|S\| \in ℤ \land \|T\| \in ℤ \land \|T\| + \|U\| \in ℤ)$
122		fzosubel2	$⊢ (x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|) \land (\|S\| \in ℤ \land \|T\| \in ℤ \land \|T\| + \|U\| \in ℤ)) \to x - \|S\| \in (\|T\| ..^\|T\| + \|U\|)$
123	117 121 122	syl2anc	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to x - \|S\| \in (\|T\| ..^\|T\| + \|U\|)$
124		ccatval2	$⊢ (T \in Word B \land U \in Word B \land x - \|S\| \in (\|T\| ..^\|T\| + \|U\|)) \to (T ++ U) (x - \|S\|) = U (x - \|S\| - \|T\|)$
125	113 114 123 124	syl3anc	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to (T ++ U) (x - \|S\|) = U (x - \|S\| - \|T\|)$
126	112 125	eqtr4d	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to U (x - \|S ++ T\|) = (T ++ U) (x - \|S\|)$
127	49	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to S ++ T \in Word B$
128	9 10	oveq12d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S ++ T\| ..^\|S ++ T\| + \|U\|) = (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)$
129	128	eleq2d	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (x \in (\|S ++ T\| ..^\|S ++ T\| + \|U\|) \leftrightarrow x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|))$
130	129	biimpar	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to x \in (\|S ++ T\| ..^\|S ++ T\| + \|U\|)$
131		ccatval2	$⊢ (S ++ T \in Word B \land U \in Word B \land x \in (\|S ++ T\| ..^\|S ++ T\| + \|U\|)) \to ((S ++ T) ++ U) (x) = U (x - \|S ++ T\|)$
132	127 114 130 131	syl3anc	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to ((S ++ T) ++ U) (x) = U (x - \|S ++ T\|)$
133		simpl1	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to S \in Word B$
134	17	adantr	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to T ++ U \in Word B$
135		fzoss1	$⊢ \|S\| + \|T\| \in ℤ_{\geq \|S\|} \to (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|) \subseteq (\|S\| ..^\|S\| + \|T\| + \|U\|)$
136	54 135	syl	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|) \subseteq (\|S\| ..^\|S\| + \|T\| + \|U\|)$
137	136 97	sseqtrrd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|) \subseteq (\|S\| ..^\|S\| + \|T ++ U\|)$
138	137	sselda	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to x \in (\|S\| ..^\|S\| + \|T ++ U\|)$
139	133 134 138 100	syl3anc	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to (S ++ (T ++ U)) (x) = (T ++ U) (x - \|S\|)$
140	126 132 139	3eqtr4d	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|)) \to ((S ++ T) ++ U) (x) = (S ++ (T ++ U)) (x)$
141	102 140	jaodan	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land (x \in (\|S\| ..^\|S\| + \|T\|) \lor x \in (\|S\| + \|T\| ..^\|S\| + \|T\| + \|U\|))) \to ((S ++ T) ++ U) (x) = (S ++ (T ++ U)) (x)$
142	69 141	syldan	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (\|S\| ..^\|S\| + \|T\| + \|U\|)) \to ((S ++ T) ++ U) (x) = (S ++ (T ++ U)) (x)$
143	64 142	jaodan	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land (x \in (0 ..^\|S\|) \lor x \in (\|S\| ..^\|S\| + \|T\| + \|U\|))) \to ((S ++ T) ++ U) (x) = (S ++ (T ++ U)) (x)$
144	44 143	syldan	$⊢ ((S \in Word B \land T \in Word B \land U \in Word B) \land x \in (0 ..^\|S\| + \|T\| + \|U\|)) \to ((S ++ T) ++ U) (x) = (S ++ (T ++ U)) (x)$
145	14 40 144	eqfnfvd	$⊢ (S \in Word B \land T \in Word B \land U \in Word B) \to (S ++ T) ++ U = S ++ (T ++ U)$

Metamath Proof Explorer

Theorem ccatass

Proof