Theorem ofccat

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

	Ref	Expression
Hypotheses	ofccat.1	|- ( ph -> E e. Word S )
	ofccat.2	|- ( ph -> F e. Word S )
	ofccat.3	|- ( ph -> G e. Word T )
	ofccat.4	|- ( ph -> H e. Word T )
	ofccat.5	|- ( ph -> ( # ` E ) = ( # ` G ) )
	ofccat.6	|- ( ph -> ( # ` F ) = ( # ` H ) )
Assertion	ofccat	|- ( ph -> ( ( E ++ F ) oF R ( G ++ H ) ) = ( ( E oF R G ) ++ ( F oF R H ) ) )

Proof

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