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

Metamath Proof Explorer

Theorem ccatvalfn

Description: The concatenation of two words is a function over the half-open integer range having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018)

Ref Expression
Assertion ccatvalfn ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐴 ++ 𝐵 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 ccatfval ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐴 ++ 𝐵 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) )
2 fvex ⊢ ( 𝐴 ‘ 𝑥 ) ∈ V
3 fvex ⊢ ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ∈ V
4 2 3 ifex ⊢ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ∈ V
5 eqid ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) )
6 4 5 fnmpti ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) Fn ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
7 fneq1 ⊢ ( ( 𝐴 ++ 𝐵 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) Fn ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) )
8 6 7 mpbiri ⊢ ( ( 𝐴 ++ 𝐵 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) , ( 𝐴 ‘ 𝑥 ) , ( 𝐵 ‘ ( 𝑥 − ( ♯ ‘ 𝐴 ) ) ) ) ) → ( 𝐴 ++ 𝐵 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
9 1 8 syl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐴 ++ 𝐵 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )