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 ⊢ ( 𝜑 → 𝐸 ∈ Word 𝑆 )
ofccat.2 ⊢ ( 𝜑 → 𝐹 ∈ Word 𝑆 )
ofccat.3 ⊢ ( 𝜑 → 𝐺 ∈ Word 𝑇 )
ofccat.4 ⊢ ( 𝜑 → 𝐻 ∈ Word 𝑇 )
ofccat.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐺 ) )
ofccat.6 ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐻 ) )
Assertion ofccat ( 𝜑 → ( ( 𝐸 ++ 𝐹 ) ∘f 𝑅 ( 𝐺 ++ 𝐻 ) ) = ( ( 𝐸 ∘f 𝑅 𝐺 ) ++ ( 𝐹 ∘f 𝑅 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 ofccat.1 ⊢ ( 𝜑 → 𝐸 ∈ Word 𝑆 )
2 ofccat.2 ⊢ ( 𝜑 → 𝐹 ∈ Word 𝑆 )
3 ofccat.3 ⊢ ( 𝜑 → 𝐺 ∈ Word 𝑇 )
4 ofccat.4 ⊢ ( 𝜑 → 𝐻 ∈ Word 𝑇 )
5 ofccat.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐺 ) )
6 ofccat.6 ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐻 ) )
7 wrdf ⊢ ( 𝐸 ∈ Word 𝑆 → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ 𝑆 )
8 ffn ⊢ ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ 𝑆 → 𝐸 Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
9 1 7 8 3syl ⊢ ( 𝜑 → 𝐸 Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
10 wrdf ⊢ ( 𝐺 ∈ Word 𝑇 → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ⟶ 𝑇 )
11 ffn ⊢ ( 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ⟶ 𝑇 → 𝐺 Fn ( 0 ..^ ( ♯ ‘ 𝐺 ) ) )
12 3 10 11 3syl ⊢ ( 𝜑 → 𝐺 Fn ( 0 ..^ ( ♯ ‘ 𝐺 ) ) )
13 5 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = ( 0 ..^ ( ♯ ‘ 𝐺 ) ) )
14 13 fneq2d ⊢ ( 𝜑 → ( 𝐺 Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ↔ 𝐺 Fn ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ) )
15 12 14 mpbird ⊢ ( 𝜑 → 𝐺 Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
16 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ∈ V )
17 inidm ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ∩ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐸 ) )
18 9 15 16 16 17 offn ⊢ ( 𝜑 → ( 𝐸 ∘f 𝑅 𝐺 ) Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
19 hashfn ⊢ ( ( 𝐸 ∘f 𝑅 𝐺 ) Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) → ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) )
20 18 19 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) )
21 wrdfin ⊢ ( 𝐸 ∈ Word 𝑆 → 𝐸 ∈ Fin )
22 hashcl ⊢ ( 𝐸 ∈ Fin → ( ♯ ‘ 𝐸 ) ∈ ℕ0 )
23 1 21 22 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) ∈ ℕ0 )
24 hashfzo0 ⊢ ( ( ♯ ‘ 𝐸 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) = ( ♯ ‘ 𝐸 ) )
25 23 24 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) = ( ♯ ‘ 𝐸 ) )
26 20 25 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) = ( ♯ ‘ 𝐸 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) = ( ♯ ‘ 𝐸 ) )
28 27 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
29 28 eleq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) )
30 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → 𝐸 Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
31 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → 𝐺 Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
32 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ∈ V )
33 29 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
34 fnfvof ⊢ ( ( ( 𝐸 Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ∧ 𝐺 Fn ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) ∧ ( ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ∈ V ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) ) → ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) = ( ( 𝐸 ‘ 𝑖 ) 𝑅 ( 𝐺 ‘ 𝑖 ) ) )
35 30 31 32 33 34 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) = ( ( 𝐸 ‘ 𝑖 ) 𝑅 ( 𝐺 ‘ 𝑖 ) ) )
36 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) = ( ♯ ‘ 𝐸 ) )
37 36 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) = ( 𝑖 − ( ♯ ‘ 𝐸 ) ) )
38 37 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) = ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) )
39 wrdf ⊢ ( 𝐹 ∈ Word 𝑆 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 )
40 ffn ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 → 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
41 2 39 40 3syl ⊢ ( 𝜑 → 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
42 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
43 wrdf ⊢ ( 𝐻 ∈ Word 𝑇 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑇 )
44 ffn ⊢ ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ⟶ 𝑇 → 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
45 4 43 44 3syl ⊢ ( 𝜑 → 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
46 6 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ ( ♯ ‘ 𝐻 ) ) )
47 46 fneq2d ⊢ ( 𝜑 → ( 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐻 ) ) ) )
48 45 47 mpbird ⊢ ( 𝜑 → 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
50 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V )
51 simplr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) )
52 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) )
53 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
54 52 53 neleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
55 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ♯ ‘ 𝐸 ) ∈ ℕ0 )
56 55 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ♯ ‘ 𝐸 ) ∈ ℤ )
57 wrdfin ⊢ ( 𝐹 ∈ Word 𝑆 → 𝐹 ∈ Fin )
58 hashcl ⊢ ( 𝐹 ∈ Fin → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
59 2 57 58 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
60 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
61 60 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℤ )
62 fzocatel ⊢ ( ( ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) ∧ ( ( ♯ ‘ 𝐸 ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ∈ ℤ ) ) → ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
63 51 54 56 61 62 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
64 fnfvof ⊢ ( ( ( 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 𝐻 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V ∧ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) → ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) = ( ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) 𝑅 ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) )
65 42 49 50 63 64 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) = ( ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) 𝑅 ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) )
66 38 65 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) ∧ ¬ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) → ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) 𝑅 ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) )
67 29 35 66 ifbieq12d2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) , ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) , ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) ) = if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( ( 𝐸 ‘ 𝑖 ) 𝑅 ( 𝐺 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) 𝑅 ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) )
68 67 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) , ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) , ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( ( 𝐸 ‘ 𝑖 ) 𝑅 ( 𝐺 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) 𝑅 ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) ) )
69 ovex ⊢ ( 𝐸 ∘f 𝑅 𝐺 ) ∈ V
70 ovex ⊢ ( 𝐹 ∘f 𝑅 𝐻 ) ∈ V
71 ccatfval ⊢ ( ( ( 𝐸 ∘f 𝑅 𝐺 ) ∈ V ∧ ( 𝐹 ∘f 𝑅 𝐻 ) ∈ V ) → ( ( 𝐸 ∘f 𝑅 𝐺 ) ++ ( 𝐹 ∘f 𝑅 𝐻 ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) + ( ♯ ‘ ( 𝐹 ∘f 𝑅 𝐻 ) ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) , ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) , ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) ) ) )
72 69 70 71 mp2an ⊢ ( ( 𝐸 ∘f 𝑅 𝐺 ) ++ ( 𝐹 ∘f 𝑅 𝐻 ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) + ( ♯ ‘ ( 𝐹 ∘f 𝑅 𝐻 ) ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) , ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) , ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) ) )
73 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V )
74 inidm ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) )
75 41 48 73 73 74 offn ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐻 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
76 hashfn ⊢ ( ( 𝐹 ∘f 𝑅 𝐻 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ ( 𝐹 ∘f 𝑅 𝐻 ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
77 75 76 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ∘f 𝑅 𝐻 ) ) = ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
78 hashfzo0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ♯ ‘ 𝐹 ) )
79 59 78 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ♯ ‘ 𝐹 ) )
80 77 79 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ∘f 𝑅 𝐻 ) ) = ( ♯ ‘ 𝐹 ) )
81 26 80 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) + ( ♯ ‘ ( 𝐹 ∘f 𝑅 𝐻 ) ) ) = ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) )
82 81 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) + ( ♯ ‘ ( 𝐹 ∘f 𝑅 𝐻 ) ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) )
83 82 mpteq1d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) + ( ♯ ‘ ( 𝐹 ∘f 𝑅 𝐻 ) ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) , ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) , ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) , ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) , ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) ) ) )
84 72 83 eqtrid ⊢ ( 𝜑 → ( ( 𝐸 ∘f 𝑅 𝐺 ) ++ ( 𝐹 ∘f 𝑅 𝐻 ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) , ( ( 𝐸 ∘f 𝑅 𝐺 ) ‘ 𝑖 ) , ( ( 𝐹 ∘f 𝑅 𝐻 ) ‘ ( 𝑖 − ( ♯ ‘ ( 𝐸 ∘f 𝑅 𝐺 ) ) ) ) ) ) )
85 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ∈ V )
86 fvex ⊢ ( 𝐸 ‘ 𝑖 ) ∈ V
87 fvex ⊢ ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ∈ V
88 86 87 ifex ⊢ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ∈ V
89 88 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ∈ V )
90 fvex ⊢ ( 𝐺 ‘ 𝑖 ) ∈ V
91 fvex ⊢ ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ∈ V
92 90 91 ifex ⊢ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ∈ V
93 92 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ∈ V )
94 ccatfval ⊢ ( ( 𝐸 ∈ Word 𝑆 ∧ 𝐹 ∈ Word 𝑆 ) → ( 𝐸 ++ 𝐹 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) )
95 1 2 94 syl2anc ⊢ ( 𝜑 → ( 𝐸 ++ 𝐹 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) )
96 ccatfval ⊢ ( ( 𝐺 ∈ Word 𝑇 ∧ 𝐻 ∈ Word 𝑇 ) → ( 𝐺 ++ 𝐻 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐺 ) + ( ♯ ‘ 𝐻 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ) )
97 3 4 96 syl2anc ⊢ ( 𝜑 → ( 𝐺 ++ 𝐻 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐺 ) + ( ♯ ‘ 𝐻 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ) )
98 5 6 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) = ( ( ♯ ‘ 𝐺 ) + ( ♯ ‘ 𝐻 ) ) )
99 98 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐺 ) + ( ♯ ‘ 𝐻 ) ) ) )
100 99 mpteq1d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐺 ) + ( ♯ ‘ 𝐻 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ) )
101 97 100 eqtr4d ⊢ ( 𝜑 → ( 𝐺 ++ 𝐻 ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ) )
102 85 89 93 95 101 offval2 ⊢ ( 𝜑 → ( ( 𝐸 ++ 𝐹 ) ∘f 𝑅 ( 𝐺 ++ 𝐻 ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ ( if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) 𝑅 if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ) ) )
103 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐺 ) )
104 103 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = ( 0 ..^ ( ♯ ‘ 𝐺 ) ) )
105 104 eleq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ↔ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ) )
106 103 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑖 − ( ♯ ‘ 𝐸 ) ) = ( 𝑖 − ( ♯ ‘ 𝐺 ) ) )
107 106 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) = ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) )
108 105 107 ifbieq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) = if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) )
109 108 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ) → ( if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) 𝑅 if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) = ( if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) 𝑅 if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ) )
110 109 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ ( if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) 𝑅 if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ ( if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) 𝑅 if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐺 ) ) ) ) ) ) )
111 102 110 eqtr4d ⊢ ( 𝜑 → ( ( 𝐸 ++ 𝐹 ) ∘f 𝑅 ( 𝐺 ++ 𝐻 ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ ( if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) 𝑅 if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) ) )
112 ovif12 ⊢ ( if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) 𝑅 if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) = if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( ( 𝐸 ‘ 𝑖 ) 𝑅 ( 𝐺 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) 𝑅 ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) )
113 112 mpteq2i ⊢ ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ ( if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐸 ‘ 𝑖 ) , ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) 𝑅 if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( 𝐺 ‘ 𝑖 ) , ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( ( 𝐸 ‘ 𝑖 ) 𝑅 ( 𝐺 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) 𝑅 ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) )
114 111 113 eqtrdi ⊢ ( 𝜑 → ( ( 𝐸 ++ 𝐹 ) ∘f 𝑅 ( 𝐺 ++ 𝐻 ) ) = ( 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐸 ) + ( ♯ ‘ 𝐹 ) ) ) ↦ if ( 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) , ( ( 𝐸 ‘ 𝑖 ) 𝑅 ( 𝐺 ‘ 𝑖 ) ) , ( ( 𝐹 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) 𝑅 ( 𝐻 ‘ ( 𝑖 − ( ♯ ‘ 𝐸 ) ) ) ) ) ) )
115 68 84 114 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝐸 ++ 𝐹 ) ∘f 𝑅 ( 𝐺 ++ 𝐻 ) ) = ( ( 𝐸 ∘f 𝑅 𝐺 ) ++ ( 𝐹 ∘f 𝑅 𝐻 ) ) )