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

Metamath Proof Explorer

Theorem ccatlen

Description: The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by JJ, 1-Jan-2024)

Ref Expression
Assertion ccatlen ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
2 1 fveq2d ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) = ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ) )
3 fvex ⊢ ( 𝑆 ‘ 𝑥 ) ∈ V
4 fvex ⊢ ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ∈ V
5 3 4 ifex ⊢ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ∈ V
6 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) )
7 5 6 fnmpti ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
8 hashfn ⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
9 7 8 mp1i ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ) = ( ♯ ‘ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
10 lencl ⊢ ( 𝑆 ∈ Word 𝐴 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
11 lencl ⊢ ( 𝑇 ∈ Word 𝐵 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
12 nn0addcl ⊢ ( ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℕ0 )
13 10 11 12 syl2an ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℕ0 )
14 hashfzo0 ⊢ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
15 13 14 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
16 2 9 15 3eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )