ccatco

Description: Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015)

		Ref	Expression
	Assertion	ccatco	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to F \circ (S ++ T) = (F \circ S) ++ (F \circ T)$

Proof

Step	Hyp	Ref	Expression
1		lenco	$⊢ (S \in Word A \land F : A ⟶ B) \to \|F \circ S\| = \|S\|$
2	1	3adant2	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to \|F \circ S\| = \|S\|$
3		lenco	$⊢ (T \in Word A \land F : A ⟶ B) \to \|F \circ T\| = \|T\|$
4	3	3adant1	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to \|F \circ T\| = \|T\|$
5	2 4	oveq12d	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to \|F \circ S\| + \|F \circ T\| = \|S\| + \|T\|$
6	5	oveq2d	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to (0 ..^\|F \circ S\| + \|F \circ T\|) = (0 ..^\|S\| + \|T\|)$
7	6	mpteq1d	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to (x \in (0 ..^\|F \circ S\| + \|F \circ T\|) ⟼ if (x \in (0 ..^\|F \circ S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|))) = (x \in (0 ..^\|S\| + \|T\|) ⟼ if (x \in (0 ..^\|F \circ S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|)))$
8	2	oveq2d	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to (0 ..^\|F \circ S\|) = (0 ..^\|S\|)$
9	8	adantr	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to (0 ..^\|F \circ S\|) = (0 ..^\|S\|)$
10	9	eleq2d	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to (x \in (0 ..^\|F \circ S\|) \leftrightarrow x \in (0 ..^\|S\|))$
11	10	ifbid	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to if (x \in (0 ..^\|F \circ S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|)) = if (x \in (0 ..^\|S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|))$
12		wrdf	$⊢ S \in Word A \to S : (0 ..^\|S\|) ⟶ A$
13	12	3ad2ant1	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to S : (0 ..^\|S\|) ⟶ A$
14	13	adantr	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to S : (0 ..^\|S\|) ⟶ A$
15	14	ffnd	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to S Fn (0 ..^\|S\|)$
16		fvco2	$⊢ (S Fn (0 ..^\|S\|) \land x \in (0 ..^\|S\|)) \to (F \circ S) (x) = F (S (x))$
17	15 16	sylan	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land x \in (0 ..^\|S\|)) \to (F \circ S) (x) = F (S (x))$
18		iftrue	$⊢ x \in (0 ..^\|S\|) \to if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|))) = F (S (x))$
19	18	adantl	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land x \in (0 ..^\|S\|)) \to if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|))) = F (S (x))$
20	17 19	eqtr4d	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land x \in (0 ..^\|S\|)) \to (F \circ S) (x) = if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|)))$
21		wrdf	$⊢ T \in Word A \to T : (0 ..^\|T\|) ⟶ A$
22	21	3ad2ant2	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to T : (0 ..^\|T\|) ⟶ A$
23	22	ad2antrr	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to T : (0 ..^\|T\|) ⟶ A$
24	23	ffnd	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to T Fn (0 ..^\|T\|)$
25		lencl	$⊢ S \in Word A \to \|S\| \in ℕ_{0}$
26	25	nn0zd	$⊢ S \in Word A \to \|S\| \in ℤ$
27	26	3ad2ant1	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to \|S\| \in ℤ$
28		fzospliti	$⊢ (x \in (0 ..^\|S\| + \|T\|) \land \|S\| \in ℤ) \to (x \in (0 ..^\|S\|) \lor x \in (\|S\| ..^\|S\| + \|T\|))$
29	28	ancoms	$⊢ (\|S\| \in ℤ \land x \in (0 ..^\|S\| + \|T\|)) \to (x \in (0 ..^\|S\|) \lor x \in (\|S\| ..^\|S\| + \|T\|))$
30	27 29	sylan	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to (x \in (0 ..^\|S\|) \lor x \in (\|S\| ..^\|S\| + \|T\|))$
31	30	orcanai	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to x \in (\|S\| ..^\|S\| + \|T\|)$
32		lencl	$⊢ T \in Word A \to \|T\| \in ℕ_{0}$
33	32	nn0zd	$⊢ T \in Word A \to \|T\| \in ℤ$
34	33	3ad2ant2	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to \|T\| \in ℤ$
35	34	ad2antrr	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to \|T\| \in ℤ$
36		fzosubel3	$⊢ (x \in (\|S\| ..^\|S\| + \|T\|) \land \|T\| \in ℤ) \to x - \|S\| \in (0 ..^\|T\|)$
37	31 35 36	syl2anc	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to x - \|S\| \in (0 ..^\|T\|)$
38		fvco2	$⊢ (T Fn (0 ..^\|T\|) \land x - \|S\| \in (0 ..^\|T\|)) \to (F \circ T) (x - \|S\|) = F (T (x - \|S\|))$
39	24 37 38	syl2anc	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to (F \circ T) (x - \|S\|) = F (T (x - \|S\|))$
40	2	oveq2d	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to x - \|F \circ S\| = x - \|S\|$
41	40	fveq2d	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to (F \circ T) (x - \|F \circ S\|) = (F \circ T) (x - \|S\|)$
42	41	ad2antrr	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to (F \circ T) (x - \|F \circ S\|) = (F \circ T) (x - \|S\|)$
43		iffalse	$⊢ \neg x \in (0 ..^\|S\|) \to if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|))) = F (T (x - \|S\|))$
44	43	adantl	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|))) = F (T (x - \|S\|))$
45	39 42 44	3eqtr4d	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to (F \circ T) (x - \|F \circ S\|) = if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|)))$
46	20 45	ifeqda	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to if (x \in (0 ..^\|S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|)) = if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|)))$
47	11 46	eqtrd	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to if (x \in (0 ..^\|F \circ S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|)) = if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|)))$
48	47	mpteq2dva	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to (x \in (0 ..^\|S\| + \|T\|) ⟼ if (x \in (0 ..^\|F \circ S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|))) = (x \in (0 ..^\|S\| + \|T\|) ⟼ if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|))))$
49	7 48	eqtr2d	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to (x \in (0 ..^\|S\| + \|T\|) ⟼ if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|)))) = (x \in (0 ..^\|F \circ S\| + \|F \circ T\|) ⟼ if (x \in (0 ..^\|F \circ S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|)))$
50	14	ffvelrnda	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land x \in (0 ..^\|S\|)) \to S (x) \in A$
51	23 37	ffvelrnd	$⊢ (((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \land \neg x \in (0 ..^\|S\|)) \to T (x - \|S\|) \in A$
52	50 51	ifclda	$⊢ ((S \in Word A \land T \in Word A \land F : A ⟶ B) \land x \in (0 ..^\|S\| + \|T\|)) \to if (x \in (0 ..^\|S\|), S (x), T (x - \|S\|)) \in A$
53		ccatfval	$⊢ (S \in Word A \land T \in Word A) \to S ++ T = (x \in (0 ..^\|S\| + \|T\|) ⟼ if (x \in (0 ..^\|S\|), S (x), T (x - \|S\|)))$
54	53	3adant3	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to S ++ T = (x \in (0 ..^\|S\| + \|T\|) ⟼ if (x \in (0 ..^\|S\|), S (x), T (x - \|S\|)))$
55		simp3	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to F : A ⟶ B$
56	55	feqmptd	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to F = (y \in A ⟼ F (y))$
57		fveq2	$⊢ y = if (x \in (0 ..^\|S\|), S (x), T (x - \|S\|)) \to F (y) = F (if (x \in (0 ..^\|S\|), S (x), T (x - \|S\|)))$
58		fvif	$⊢ F (if (x \in (0 ..^\|S\|), S (x), T (x - \|S\|))) = if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|)))$
59	57 58	syl6eq	$⊢ y = if (x \in (0 ..^\|S\|), S (x), T (x - \|S\|)) \to F (y) = if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|)))$
60	52 54 56 59	fmptco	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to F \circ (S ++ T) = (x \in (0 ..^\|S\| + \|T\|) ⟼ if (x \in (0 ..^\|S\|), F (S (x)), F (T (x - \|S\|))))$
61		ffun	$⊢ F : A ⟶ B \to Fun F$
62	61	3ad2ant3	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to Fun F$
63		simp1	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to S \in Word A$
64		cofunexg	$⊢ (Fun F \land S \in Word A) \to F \circ S \in V$
65	62 63 64	syl2anc	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to F \circ S \in V$
66		simp2	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to T \in Word A$
67		cofunexg	$⊢ (Fun F \land T \in Word A) \to F \circ T \in V$
68	62 66 67	syl2anc	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to F \circ T \in V$
69		ccatfval	$⊢ (F \circ S \in V \land F \circ T \in V) \to (F \circ S) ++ (F \circ T) = (x \in (0 ..^\|F \circ S\| + \|F \circ T\|) ⟼ if (x \in (0 ..^\|F \circ S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|)))$
70	65 68 69	syl2anc	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to (F \circ S) ++ (F \circ T) = (x \in (0 ..^\|F \circ S\| + \|F \circ T\|) ⟼ if (x \in (0 ..^\|F \circ S\|), (F \circ S) (x), (F \circ T) (x - \|F \circ S\|)))$
71	49 60 70	3eqtr4d	$⊢ (S \in Word A \land T \in Word A \land F : A ⟶ B) \to F \circ (S ++ T) = (F \circ S) ++ (F \circ T)$

Metamath Proof Explorer

Theorem ccatco

Proof