ofcccat

Description: Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 5-Oct-2018)

	Ref	Expression
Hypotheses	ofcccat.1	$⊢ φ \to F \in Word S$
	ofcccat.2	$⊢ φ \to G \in Word S$
	ofcccat.3	$⊢ φ \to K \in T$
Assertion	ofcccat	$⊢ φ \to (F ++ G) \circ_{fc} R K = (F \circ_{fc} R K) ++ (G \circ_{fc} R K)$

Proof

Step	Hyp	Ref	Expression
1		ofcccat.1	$⊢ φ \to F \in Word S$
2		ofcccat.2	$⊢ φ \to G \in Word S$
3		ofcccat.3	$⊢ φ \to K \in T$
4		fconst6g	$⊢ K \in T \to ((0 ..^\|F\|) \times \{K\}) : (0 ..^\|F\|) ⟶ T$
5		iswrdi	$⊢ ((0 ..^\|F\|) \times \{K\}) : (0 ..^\|F\|) ⟶ T \to (0 ..^\|F\|) \times \{K\} \in Word T$
6	3 4 5	3syl	$⊢ φ \to (0 ..^\|F\|) \times \{K\} \in Word T$
7		fconst6g	$⊢ K \in T \to ((0 ..^\|G\|) \times \{K\}) : (0 ..^\|G\|) ⟶ T$
8		iswrdi	$⊢ ((0 ..^\|G\|) \times \{K\}) : (0 ..^\|G\|) ⟶ T \to (0 ..^\|G\|) \times \{K\} \in Word T$
9	3 7 8	3syl	$⊢ φ \to (0 ..^\|G\|) \times \{K\} \in Word T$
10		fzofi	$⊢ (0 ..^\|F\|) \in Fin$
11		snfi	$⊢ \{K\} \in Fin$
12		hashxp	$⊢ ((0 ..^\|F\|) \in Fin \land \{K\} \in Fin) \to \|(0 ..^\|F\|) \times \{K\}\| = \|(0 ..^\|F\|)\| \|\{K\}\|$
13	10 11 12	mp2an	$⊢ \|(0 ..^\|F\|) \times \{K\}\| = \|(0 ..^\|F\|)\| \|\{K\}\|$
14		lencl	$⊢ F \in Word S \to \|F\| \in ℕ_{0}$
15		hashfzo0	$⊢ \|F\| \in ℕ_{0} \to \|(0 ..^\|F\|)\| = \|F\|$
16	1 14 15	3syl	$⊢ φ \to \|(0 ..^\|F\|)\| = \|F\|$
17		hashsng	$⊢ K \in T \to \|\{K\}\| = 1$
18	3 17	syl	$⊢ φ \to \|\{K\}\| = 1$
19	16 18	oveq12d	$⊢ φ \to \|(0 ..^\|F\|)\| \|\{K\}\| = \|F\| \cdot 1$
20	1 14	syl	$⊢ φ \to \|F\| \in ℕ_{0}$
21	20	nn0cnd	$⊢ φ \to \|F\| \in ℂ$
22	21	mulridd	$⊢ φ \to \|F\| \cdot 1 = \|F\|$
23	19 22	eqtrd	$⊢ φ \to \|(0 ..^\|F\|)\| \|\{K\}\| = \|F\|$
24	13 23	eqtr2id	$⊢ φ \to \|F\| = \|(0 ..^\|F\|) \times \{K\}\|$
25		fzofi	$⊢ (0 ..^\|G\|) \in Fin$
26		hashxp	$⊢ ((0 ..^\|G\|) \in Fin \land \{K\} \in Fin) \to \|(0 ..^\|G\|) \times \{K\}\| = \|(0 ..^\|G\|)\| \|\{K\}\|$
27	25 11 26	mp2an	$⊢ \|(0 ..^\|G\|) \times \{K\}\| = \|(0 ..^\|G\|)\| \|\{K\}\|$
28		lencl	$⊢ G \in Word S \to \|G\| \in ℕ_{0}$
29		hashfzo0	$⊢ \|G\| \in ℕ_{0} \to \|(0 ..^\|G\|)\| = \|G\|$
30	2 28 29	3syl	$⊢ φ \to \|(0 ..^\|G\|)\| = \|G\|$
31	30 18	oveq12d	$⊢ φ \to \|(0 ..^\|G\|)\| \|\{K\}\| = \|G\| \cdot 1$
32	2 28	syl	$⊢ φ \to \|G\| \in ℕ_{0}$
33	32	nn0cnd	$⊢ φ \to \|G\| \in ℂ$
34	33	mulridd	$⊢ φ \to \|G\| \cdot 1 = \|G\|$
35	31 34	eqtrd	$⊢ φ \to \|(0 ..^\|G\|)\| \|\{K\}\| = \|G\|$
36	27 35	eqtr2id	$⊢ φ \to \|G\| = \|(0 ..^\|G\|) \times \{K\}\|$
37	1 2 6 9 24 36	ofccat	$⊢ φ \to (F ++ G) R_{f} (((0 ..^\|F\|) \times \{K\}) ++ ((0 ..^\|G\|) \times \{K\})) = (F R_{f} ((0 ..^\|F\|) \times \{K\})) ++ (G R_{f} ((0 ..^\|G\|) \times \{K\}))$
38		ccatcl	$⊢ (F \in Word S \land G \in Word S) \to F ++ G \in Word S$
39	1 2 38	syl2anc	$⊢ φ \to F ++ G \in Word S$
40		wrdf	$⊢ F ++ G \in Word S \to (F ++ G) : (0 ..^\|F ++ G\|) ⟶ S$
41	39 40	syl	$⊢ φ \to (F ++ G) : (0 ..^\|F ++ G\|) ⟶ S$
42		ovexd	$⊢ φ \to (0 ..^\|F ++ G\|) \in V$
43	41 42 3	ofcof	$⊢ φ \to (F ++ G) \circ_{fc} R K = (F ++ G) R_{f} ((0 ..^\|F ++ G\|) \times \{K\})$
44		eqid	$⊢ (0 ..^\|F\| + \|G\|) \times \{K\} = (0 ..^\|F\| + \|G\|) \times \{K\}$
45		ccatlen	$⊢ (F \in Word S \land G \in Word S) \to \|F ++ G\| = \|F\| + \|G\|$
46	1 2 45	syl2anc	$⊢ φ \to \|F ++ G\| = \|F\| + \|G\|$
47	46	oveq2d	$⊢ φ \to (0 ..^\|F ++ G\|) = (0 ..^\|F\| + \|G\|)$
48	47	xpeq1d	$⊢ φ \to (0 ..^\|F ++ G\|) \times \{K\} = (0 ..^\|F\| + \|G\|) \times \{K\}$
49		eqid	$⊢ (0 ..^\|F\|) \times \{K\} = (0 ..^\|F\|) \times \{K\}$
50		eqid	$⊢ (0 ..^\|G\|) \times \{K\} = (0 ..^\|G\|) \times \{K\}$
51	49 50 44 3 20 32	ccatmulgnn0dir	$⊢ φ \to ((0 ..^\|F\|) \times \{K\}) ++ ((0 ..^\|G\|) \times \{K\}) = (0 ..^\|F\| + \|G\|) \times \{K\}$
52	44 48 51	3eqtr4a	$⊢ φ \to (0 ..^\|F ++ G\|) \times \{K\} = ((0 ..^\|F\|) \times \{K\}) ++ ((0 ..^\|G\|) \times \{K\})$
53	52	oveq2d	$⊢ φ \to (F ++ G) R_{f} ((0 ..^\|F ++ G\|) \times \{K\}) = (F ++ G) R_{f} (((0 ..^\|F\|) \times \{K\}) ++ ((0 ..^\|G\|) \times \{K\}))$
54	43 53	eqtrd	$⊢ φ \to (F ++ G) \circ_{fc} R K = (F ++ G) R_{f} (((0 ..^\|F\|) \times \{K\}) ++ ((0 ..^\|G\|) \times \{K\}))$
55		wrdf	$⊢ F \in Word S \to F : (0 ..^\|F\|) ⟶ S$
56	1 55	syl	$⊢ φ \to F : (0 ..^\|F\|) ⟶ S$
57		ovexd	$⊢ φ \to (0 ..^\|F\|) \in V$
58	56 57 3	ofcof	$⊢ φ \to F \circ_{fc} R K = F R_{f} ((0 ..^\|F\|) \times \{K\})$
59		wrdf	$⊢ G \in Word S \to G : (0 ..^\|G\|) ⟶ S$
60	2 59	syl	$⊢ φ \to G : (0 ..^\|G\|) ⟶ S$
61		ovexd	$⊢ φ \to (0 ..^\|G\|) \in V$
62	60 61 3	ofcof	$⊢ φ \to G \circ_{fc} R K = G R_{f} ((0 ..^\|G\|) \times \{K\})$
63	58 62	oveq12d	$⊢ φ \to (F \circ_{fc} R K) ++ (G \circ_{fc} R K) = (F R_{f} ((0 ..^\|F\|) \times \{K\})) ++ (G R_{f} ((0 ..^\|G\|) \times \{K\}))$
64	37 54 63	3eqtr4d	$⊢ φ \to (F ++ G) \circ_{fc} R K = (F \circ_{fc} R K) ++ (G \circ_{fc} R K)$

Metamath Proof Explorer

Theorem ofcccat

Proof