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

Metamath Proof Explorer

Theorem ccatfval

Description: Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion ccatfval ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
2 elex ⊢ ( 𝑇 ∈ 𝑊 → 𝑇 ∈ V )
3 fveq2 ⊢ ( 𝑠 = 𝑆 → ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 𝑆 ) )
4 fveq2 ⊢ ( 𝑡 = 𝑇 → ( ♯ ‘ 𝑡 ) = ( ♯ ‘ 𝑇 ) )
5 3 4 oveqan12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
6 5 oveq2d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
7 3 oveq2d ⊢ ( 𝑠 = 𝑆 → ( 0 ..^ ( ♯ ‘ 𝑠 ) ) = ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
8 7 eleq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ↔ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
9 8 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ↔ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
10 fveq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
11 10 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 ) )
12 simpr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → 𝑡 = 𝑇 )
13 3 oveq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑥 − ( ♯ ‘ 𝑠 ) ) = ( 𝑥 − ( ♯ ‘ 𝑆 ) ) )
14 13 adantr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑥 − ( ♯ ‘ 𝑠 ) ) = ( 𝑥 − ( ♯ ‘ 𝑆 ) ) )
15 12 14 fveq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) = ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) )
16 9 11 15 ifbieq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) = if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) )
17 6 16 mpteq12dv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
18 df-concat ⊢ ++ = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) )
19 ovex ⊢ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ∈ V
20 19 mptex ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) ∈ V
21 17 18 20 ovmpoa ⊢ ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )
22 1 2 21 syl2an ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊 ) → ( 𝑆 ++ 𝑇 ) = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )