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 ..^ ( ♯ ‘ 𝑆 ) ) , ( 𝑆 ‘ 𝑥 ) , ( 𝑇 ‘ ( 𝑥 − ( ♯ ‘ 𝑆 ) ) ) ) ) )