ofccat

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

	Ref	Expression
Hypotheses	ofccat.1	$⊢ φ \to E \in Word S$
	ofccat.2	$⊢ φ \to F \in Word S$
	ofccat.3	$⊢ φ \to G \in Word T$
	ofccat.4	$⊢ φ \to H \in Word T$
	ofccat.5	$⊢ φ \to \|E\| = \|G\|$
	ofccat.6	$⊢ φ \to \|F\| = \|H\|$
Assertion	ofccat	$⊢ φ \to (E ++ F) R_{f} (G ++ H) = (E R_{f} G) ++ (F R_{f} H)$

Proof

Step	Hyp	Ref	Expression
1		ofccat.1	$⊢ φ \to E \in Word S$
2		ofccat.2	$⊢ φ \to F \in Word S$
3		ofccat.3	$⊢ φ \to G \in Word T$
4		ofccat.4	$⊢ φ \to H \in Word T$
5		ofccat.5	$⊢ φ \to \|E\| = \|G\|$
6		ofccat.6	$⊢ φ \to \|F\| = \|H\|$
7		wrdf	$⊢ E \in Word S \to E : (0 ..^\|E\|) ⟶ S$
8		ffn	$⊢ E : (0 ..^\|E\|) ⟶ S \to E Fn (0 ..^\|E\|)$
9	1 7 8	3syl	$⊢ φ \to E Fn (0 ..^\|E\|)$
10		wrdf	$⊢ G \in Word T \to G : (0 ..^\|G\|) ⟶ T$
11		ffn	$⊢ G : (0 ..^\|G\|) ⟶ T \to G Fn (0 ..^\|G\|)$
12	3 10 11	3syl	$⊢ φ \to G Fn (0 ..^\|G\|)$
13	5	oveq2d	$⊢ φ \to (0 ..^\|E\|) = (0 ..^\|G\|)$
14	13	fneq2d	$⊢ φ \to (G Fn (0 ..^\|E\|) \leftrightarrow G Fn (0 ..^\|G\|))$
15	12 14	mpbird	$⊢ φ \to G Fn (0 ..^\|E\|)$
16		ovexd	$⊢ φ \to (0 ..^\|E\|) \in V$
17		inidm	$⊢ (0 ..^\|E\|) \cap (0 ..^\|E\|) = (0 ..^\|E\|)$
18	9 15 16 16 17	offn	$⊢ φ \to (E R_{f} G) Fn (0 ..^\|E\|)$
19		hashfn	$⊢ (E R_{f} G) Fn (0 ..^\|E\|) \to \|E R_{f} G\| = \|(0 ..^\|E\|)\|$
20	18 19	syl	$⊢ φ \to \|E R_{f} G\| = \|(0 ..^\|E\|)\|$
21		wrdfin	$⊢ E \in Word S \to E \in Fin$
22		hashcl	$⊢ E \in Fin \to \|E\| \in ℕ_{0}$
23	1 21 22	3syl	$⊢ φ \to \|E\| \in ℕ_{0}$
24		hashfzo0	$⊢ \|E\| \in ℕ_{0} \to \|(0 ..^\|E\|)\| = \|E\|$
25	23 24	syl	$⊢ φ \to \|(0 ..^\|E\|)\| = \|E\|$
26	20 25	eqtrd	$⊢ φ \to \|E R_{f} G\| = \|E\|$
27	26	adantr	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to \|E R_{f} G\| = \|E\|$
28	27	oveq2d	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to (0 ..^\|E R_{f} G\|) = (0 ..^\|E\|)$
29	28	eleq2d	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to (i \in (0 ..^\|E R_{f} G\|) \leftrightarrow i \in (0 ..^\|E\|))$
30	9	ad2antrr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land i \in (0 ..^\|E R_{f} G\|)) \to E Fn (0 ..^\|E\|)$
31	15	ad2antrr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land i \in (0 ..^\|E R_{f} G\|)) \to G Fn (0 ..^\|E\|)$
32		ovexd	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land i \in (0 ..^\|E R_{f} G\|)) \to (0 ..^\|E\|) \in V$
33	29	biimpa	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land i \in (0 ..^\|E R_{f} G\|)) \to i \in (0 ..^\|E\|)$
34		fnfvof	$⊢ ((E Fn (0 ..^\|E\|) \land G Fn (0 ..^\|E\|)) \land ((0 ..^\|E\|) \in V \land i \in (0 ..^\|E\|))) \to (E R_{f} G) (i) = E (i) R G (i)$
35	30 31 32 33 34	syl22anc	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land i \in (0 ..^\|E R_{f} G\|)) \to (E R_{f} G) (i) = E (i) R G (i)$
36	26	ad2antrr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to \|E R_{f} G\| = \|E\|$
37	36	oveq2d	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to i - \|E R_{f} G\| = i - \|E\|$
38	37	fveq2d	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to (F R_{f} H) (i - \|E R_{f} G\|) = (F R_{f} H) (i - \|E\|)$
39		wrdf	$⊢ F \in Word S \to F : (0 ..^\|F\|) ⟶ S$
40		ffn	$⊢ F : (0 ..^\|F\|) ⟶ S \to F Fn (0 ..^\|F\|)$
41	2 39 40	3syl	$⊢ φ \to F Fn (0 ..^\|F\|)$
42	41	ad2antrr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to F Fn (0 ..^\|F\|)$
43		wrdf	$⊢ H \in Word T \to H : (0 ..^\|H\|) ⟶ T$
44		ffn	$⊢ H : (0 ..^\|H\|) ⟶ T \to H Fn (0 ..^\|H\|)$
45	4 43 44	3syl	$⊢ φ \to H Fn (0 ..^\|H\|)$
46	6	oveq2d	$⊢ φ \to (0 ..^\|F\|) = (0 ..^\|H\|)$
47	46	fneq2d	$⊢ φ \to (H Fn (0 ..^\|F\|) \leftrightarrow H Fn (0 ..^\|H\|))$
48	45 47	mpbird	$⊢ φ \to H Fn (0 ..^\|F\|)$
49	48	ad2antrr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to H Fn (0 ..^\|F\|)$
50		ovexd	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to (0 ..^\|F\|) \in V$
51		simplr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to i \in (0 ..^\|E\| + \|F\|)$
52		simpr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to \neg i \in (0 ..^\|E R_{f} G\|)$
53	28	adantr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to (0 ..^\|E R_{f} G\|) = (0 ..^\|E\|)$
54	52 53	neleqtrd	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to \neg i \in (0 ..^\|E\|)$
55	23	ad2antrr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to \|E\| \in ℕ_{0}$
56	55	nn0zd	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to \|E\| \in ℤ$
57		wrdfin	$⊢ F \in Word S \to F \in Fin$
58		hashcl	$⊢ F \in Fin \to \|F\| \in ℕ_{0}$
59	2 57 58	3syl	$⊢ φ \to \|F\| \in ℕ_{0}$
60	59	ad2antrr	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to \|F\| \in ℕ_{0}$
61	60	nn0zd	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to \|F\| \in ℤ$
62		fzocatel	$⊢ ((i \in (0 ..^\|E\| + \|F\|) \land \neg i \in (0 ..^\|E\|)) \land (\|E\| \in ℤ \land \|F\| \in ℤ)) \to i - \|E\| \in (0 ..^\|F\|)$
63	51 54 56 61 62	syl22anc	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to i - \|E\| \in (0 ..^\|F\|)$
64		fnfvof	$⊢ ((F Fn (0 ..^\|F\|) \land H Fn (0 ..^\|F\|)) \land ((0 ..^\|F\|) \in V \land i - \|E\| \in (0 ..^\|F\|))) \to (F R_{f} H) (i - \|E\|) = F (i - \|E\|) R H (i - \|E\|)$
65	42 49 50 63 64	syl22anc	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to (F R_{f} H) (i - \|E\|) = F (i - \|E\|) R H (i - \|E\|)$
66	38 65	eqtrd	$⊢ ((φ \land i \in (0 ..^\|E\| + \|F\|)) \land \neg i \in (0 ..^\|E R_{f} G\|)) \to (F R_{f} H) (i - \|E R_{f} G\|) = F (i - \|E\|) R H (i - \|E\|)$
67	29 35 66	ifbieq12d2	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to if (i \in (0 ..^\|E R_{f} G\|), (E R_{f} G) (i), (F R_{f} H) (i - \|E R_{f} G\|)) = if (i \in (0 ..^\|E\|), E (i) R G (i), F (i - \|E\|) R H (i - \|E\|))$
68	67	mpteq2dva	$⊢ φ \to (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E R_{f} G\|), (E R_{f} G) (i), (F R_{f} H) (i - \|E R_{f} G\|))) = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i) R G (i), F (i - \|E\|) R H (i - \|E\|)))$
69		ovex	$⊢ E R_{f} G \in V$
70		ovex	$⊢ F R_{f} H \in V$
71		ccatfval	$⊢ (E R_{f} G \in V \land F R_{f} H \in V) \to (E R_{f} G) ++ (F R_{f} H) = (i \in (0 ..^\|E R_{f} G\| + \|F R_{f} H\|) ⟼ if (i \in (0 ..^\|E R_{f} G\|), (E R_{f} G) (i), (F R_{f} H) (i - \|E R_{f} G\|)))$
72	69 70 71	mp2an	$⊢ (E R_{f} G) ++ (F R_{f} H) = (i \in (0 ..^\|E R_{f} G\| + \|F R_{f} H\|) ⟼ if (i \in (0 ..^\|E R_{f} G\|), (E R_{f} G) (i), (F R_{f} H) (i - \|E R_{f} G\|)))$
73		ovexd	$⊢ φ \to (0 ..^\|F\|) \in V$
74		inidm	$⊢ (0 ..^\|F\|) \cap (0 ..^\|F\|) = (0 ..^\|F\|)$
75	41 48 73 73 74	offn	$⊢ φ \to (F R_{f} H) Fn (0 ..^\|F\|)$
76		hashfn	$⊢ (F R_{f} H) Fn (0 ..^\|F\|) \to \|F R_{f} H\| = \|(0 ..^\|F\|)\|$
77	75 76	syl	$⊢ φ \to \|F R_{f} H\| = \|(0 ..^\|F\|)\|$
78		hashfzo0	$⊢ \|F\| \in ℕ_{0} \to \|(0 ..^\|F\|)\| = \|F\|$
79	59 78	syl	$⊢ φ \to \|(0 ..^\|F\|)\| = \|F\|$
80	77 79	eqtrd	$⊢ φ \to \|F R_{f} H\| = \|F\|$
81	26 80	oveq12d	$⊢ φ \to \|E R_{f} G\| + \|F R_{f} H\| = \|E\| + \|F\|$
82	81	oveq2d	$⊢ φ \to (0 ..^\|E R_{f} G\| + \|F R_{f} H\|) = (0 ..^\|E\| + \|F\|)$
83	82	mpteq1d	$⊢ φ \to (i \in (0 ..^\|E R_{f} G\| + \|F R_{f} H\|) ⟼ if (i \in (0 ..^\|E R_{f} G\|), (E R_{f} G) (i), (F R_{f} H) (i - \|E R_{f} G\|))) = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E R_{f} G\|), (E R_{f} G) (i), (F R_{f} H) (i - \|E R_{f} G\|)))$
84	72 83	syl5eq	$⊢ φ \to (E R_{f} G) ++ (F R_{f} H) = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E R_{f} G\|), (E R_{f} G) (i), (F R_{f} H) (i - \|E R_{f} G\|)))$
85		ovexd	$⊢ φ \to (0 ..^\|E\| + \|F\|) \in V$
86		fvex	$⊢ E (i) \in V$
87		fvex	$⊢ F (i - \|E\|) \in V$
88	86 87	ifex	$⊢ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) \in V$
89	88	a1i	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) \in V$
90		fvex	$⊢ G (i) \in V$
91		fvex	$⊢ H (i - \|G\|) \in V$
92	90 91	ifex	$⊢ if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|)) \in V$
93	92	a1i	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|)) \in V$
94		ccatfval	$⊢ (E \in Word S \land F \in Word S) \to E ++ F = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)))$
95	1 2 94	syl2anc	$⊢ φ \to E ++ F = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)))$
96		ccatfval	$⊢ (G \in Word T \land H \in Word T) \to G ++ H = (i \in (0 ..^\|G\| + \|H\|) ⟼ if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|)))$
97	3 4 96	syl2anc	$⊢ φ \to G ++ H = (i \in (0 ..^\|G\| + \|H\|) ⟼ if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|)))$
98	5 6	oveq12d	$⊢ φ \to \|E\| + \|F\| = \|G\| + \|H\|$
99	98	oveq2d	$⊢ φ \to (0 ..^\|E\| + \|F\|) = (0 ..^\|G\| + \|H\|)$
100	99	mpteq1d	$⊢ φ \to (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|))) = (i \in (0 ..^\|G\| + \|H\|) ⟼ if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|)))$
101	97 100	eqtr4d	$⊢ φ \to G ++ H = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|)))$
102	85 89 93 95 101	offval2	$⊢ φ \to (E ++ F) R_{f} (G ++ H) = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) R if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|)))$
103	5	adantr	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to \|E\| = \|G\|$
104	103	oveq2d	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to (0 ..^\|E\|) = (0 ..^\|G\|)$
105	104	eleq2d	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to (i \in (0 ..^\|E\|) \leftrightarrow i \in (0 ..^\|G\|))$
106	103	oveq2d	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to i - \|E\| = i - \|G\|$
107	106	fveq2d	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to H (i - \|E\|) = H (i - \|G\|)$
108	105 107	ifbieq2d	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to if (i \in (0 ..^\|E\|), G (i), H (i - \|E\|)) = if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|))$
109	108	oveq2d	$⊢ (φ \land i \in (0 ..^\|E\| + \|F\|)) \to if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) R if (i \in (0 ..^\|E\|), G (i), H (i - \|E\|)) = if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) R if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|))$
110	109	mpteq2dva	$⊢ φ \to (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) R if (i \in (0 ..^\|E\|), G (i), H (i - \|E\|))) = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) R if (i \in (0 ..^\|G\|), G (i), H (i - \|G\|)))$
111	102 110	eqtr4d	$⊢ φ \to (E ++ F) R_{f} (G ++ H) = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) R if (i \in (0 ..^\|E\|), G (i), H (i - \|E\|)))$
112		ovif12	$⊢ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) R if (i \in (0 ..^\|E\|), G (i), H (i - \|E\|)) = if (i \in (0 ..^\|E\|), E (i) R G (i), F (i - \|E\|) R H (i - \|E\|))$
113	112	mpteq2i	$⊢ (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i), F (i - \|E\|)) R if (i \in (0 ..^\|E\|), G (i), H (i - \|E\|))) = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i) R G (i), F (i - \|E\|) R H (i - \|E\|)))$
114	111 113	eqtrdi	$⊢ φ \to (E ++ F) R_{f} (G ++ H) = (i \in (0 ..^\|E\| + \|F\|) ⟼ if (i \in (0 ..^\|E\|), E (i) R G (i), F (i - \|E\|) R H (i - \|E\|)))$
115	68 84 114	3eqtr4rd	$⊢ φ \to (E ++ F) R_{f} (G ++ H) = (E R_{f} G) ++ (F R_{f} H)$

Metamath Proof Explorer

Theorem ofccat

Proof