This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( 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 ) ) )