Metamath Proof Explorer

Theorem ofcccat

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

Ref Expression
Hypotheses ofcccat.1 ⊢ ( 𝜑 → 𝐹 ∈ Word 𝑆 )
ofcccat.2 ⊢ ( 𝜑 → 𝐺 ∈ Word 𝑆 )
ofcccat.3 ⊢ ( 𝜑 → 𝐾 ∈ 𝑇 )
Assertion ofcccat ( 𝜑 → ( ( 𝐹 ++ 𝐺 ) ∘f/c 𝑅 𝐾 ) = ( ( 𝐹 ∘f/c 𝑅 𝐾 ) ++ ( 𝐺 ∘f/c 𝑅 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 ofcccat.1 ⊢ ( 𝜑 → 𝐹 ∈ Word 𝑆 )
2 ofcccat.2 ⊢ ( 𝜑 → 𝐺 ∈ Word 𝑆 )
3 ofcccat.3 ⊢ ( 𝜑 → 𝐾 ∈ 𝑇 )
4 fconst6g ⊢ ( 𝐾 ∈ 𝑇 → ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑇 )
5 iswrdi ⊢ ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑇 → ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ∈ Word 𝑇 )
6 3 4 5 3syl ⊢ ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ∈ Word 𝑇 )
7 fconst6g ⊢ ( 𝐾 ∈ 𝑇 → ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) : ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ⟶ 𝑇 )
8 iswrdi ⊢ ( ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) : ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ⟶ 𝑇 → ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ∈ Word 𝑇 )
9 3 7 8 3syl ⊢ ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ∈ Word 𝑇 )
10 fzofi ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ Fin
11 snfi ⊢ { 𝐾 } ∈ Fin
12 hashxp ⊢ ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ Fin ∧ { 𝐾 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) · ( ♯ ‘ { 𝐾 } ) ) )
13 10 11 12 mp2an ⊢ ( ♯ ‘ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) · ( ♯ ‘ { 𝐾 } ) )
14 lencl ⊢ ( 𝐹 ∈ Word 𝑆 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
15 hashfzo0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ♯ ‘ 𝐹 ) )
16 1 14 15 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ♯ ‘ 𝐹 ) )
17 hashsng ⊢ ( 𝐾 ∈ 𝑇 → ( ♯ ‘ { 𝐾 } ) = 1 )
18 3 17 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝐾 } ) = 1 )
19 16 18 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) · ( ♯ ‘ { 𝐾 } ) ) = ( ( ♯ ‘ 𝐹 ) · 1 ) )
20 1 14 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
21 20 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℂ )
22 21 mulid1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) · 1 ) = ( ♯ ‘ 𝐹 ) )
23 19 22 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) · ( ♯ ‘ { 𝐾 } ) ) = ( ♯ ‘ 𝐹 ) )
24 13 23 eqtr2id ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ) )
25 fzofi ⊢ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ∈ Fin
26 hashxp ⊢ ( ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ∈ Fin ∧ { 𝐾 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ) · ( ♯ ‘ { 𝐾 } ) ) )
27 25 11 26 mp2an ⊢ ( ♯ ‘ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) = ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ) · ( ♯ ‘ { 𝐾 } ) )
28 lencl ⊢ ( 𝐺 ∈ Word 𝑆 → ( ♯ ‘ 𝐺 ) ∈ ℕ0 )
29 hashfzo0 ⊢ ( ( ♯ ‘ 𝐺 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ) = ( ♯ ‘ 𝐺 ) )
30 2 28 29 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ) = ( ♯ ‘ 𝐺 ) )
31 30 18 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ) · ( ♯ ‘ { 𝐾 } ) ) = ( ( ♯ ‘ 𝐺 ) · 1 ) )
32 2 28 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐺 ) ∈ ℕ0 )
33 32 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐺 ) ∈ ℂ )
34 33 mulid1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐺 ) · 1 ) = ( ♯ ‘ 𝐺 ) )
35 31 34 eqtrd ⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ) · ( ♯ ‘ { 𝐾 } ) ) = ( ♯ ‘ 𝐺 ) )
36 27 35 eqtr2id ⊢ ( 𝜑 → ( ♯ ‘ 𝐺 ) = ( ♯ ‘ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) )
37 1 2 6 9 24 36 ofccat ⊢ ( 𝜑 → ( ( 𝐹 ++ 𝐺 ) ∘f 𝑅 ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ++ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) ) = ( ( 𝐹 ∘f 𝑅 ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ) ++ ( 𝐺 ∘f 𝑅 ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) ) )
38 ccatcl ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝐺 ∈ Word 𝑆 ) → ( 𝐹 ++ 𝐺 ) ∈ Word 𝑆 )
39 1 2 38 syl2anc ⊢ ( 𝜑 → ( 𝐹 ++ 𝐺 ) ∈ Word 𝑆 )
40 wrdf ⊢ ( ( 𝐹 ++ 𝐺 ) ∈ Word 𝑆 → ( 𝐹 ++ 𝐺 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) ) ⟶ 𝑆 )
41 39 40 syl ⊢ ( 𝜑 → ( 𝐹 ++ 𝐺 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) ) ⟶ 𝑆 )
42 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) ) ∈ V )
43 41 42 3 ofcof ⊢ ( 𝜑 → ( ( 𝐹 ++ 𝐺 ) ∘f/c 𝑅 𝐾 ) = ( ( 𝐹 ++ 𝐺 ) ∘f 𝑅 ( ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) ) × { 𝐾 } ) ) )
44 eqid ⊢ ( ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝐺 ) ) ) × { 𝐾 } ) = ( ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝐺 ) ) ) × { 𝐾 } )
45 ccatlen ⊢ ( ( 𝐹 ∈ Word 𝑆 ∧ 𝐺 ∈ Word 𝑆 ) → ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝐺 ) ) )
46 1 2 45 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝐺 ) ) )
47 46 oveq2d ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝐺 ) ) ) )
48 47 xpeq1d ⊢ ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) ) × { 𝐾 } ) = ( ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝐺 ) ) ) × { 𝐾 } ) )
49 eqid ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) = ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } )
50 eqid ⊢ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) = ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } )
51 49 50 44 3 20 32 ccatmulgnn0dir ⊢ ( 𝜑 → ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ++ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝐺 ) ) ) × { 𝐾 } ) )
52 44 48 51 3eqtr4a ⊢ ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) ) × { 𝐾 } ) = ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ++ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) )
53 52 oveq2d ⊢ ( 𝜑 → ( ( 𝐹 ++ 𝐺 ) ∘f 𝑅 ( ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝐺 ) ) ) × { 𝐾 } ) ) = ( ( 𝐹 ++ 𝐺 ) ∘f 𝑅 ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ++ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) ) )
54 43 53 eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ++ 𝐺 ) ∘f/c 𝑅 𝐾 ) = ( ( 𝐹 ++ 𝐺 ) ∘f 𝑅 ( ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ++ ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) ) )
55 wrdf ⊢ ( 𝐹 ∈ Word 𝑆 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 )
56 1 55 syl ⊢ ( 𝜑 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ 𝑆 )
57 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∈ V )
58 56 57 3 ofcof ⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐾 ) = ( 𝐹 ∘f 𝑅 ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ) )
59 wrdf ⊢ ( 𝐺 ∈ Word 𝑆 → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ⟶ 𝑆 )
60 2 59 syl ⊢ ( 𝜑 → 𝐺 : ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ⟶ 𝑆 )
61 ovexd ⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐺 ) ) ∈ V )
62 60 61 3 ofcof ⊢ ( 𝜑 → ( 𝐺 ∘f/c 𝑅 𝐾 ) = ( 𝐺 ∘f 𝑅 ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) )
63 58 62 oveq12d ⊢ ( 𝜑 → ( ( 𝐹 ∘f/c 𝑅 𝐾 ) ++ ( 𝐺 ∘f/c 𝑅 𝐾 ) ) = ( ( 𝐹 ∘f 𝑅 ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) × { 𝐾 } ) ) ++ ( 𝐺 ∘f 𝑅 ( ( 0 ..^ ( ♯ ‘ 𝐺 ) ) × { 𝐾 } ) ) ) )
64 37 54 63 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐹 ++ 𝐺 ) ∘f/c 𝑅 𝐾 ) = ( ( 𝐹 ∘f/c 𝑅 𝐾 ) ++ ( 𝐺 ∘f/c 𝑅 𝐾 ) ) )