Metamath Proof Explorer
Definition df-s4
Description: Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)
|
|
Ref |
Expression |
|
Assertion |
df-s4 |
⊢ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 = ( 〈“ 𝐴 𝐵 𝐶 ”〉 ++ 〈“ 𝐷 ”〉 ) |
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
cA |
⊢ 𝐴 |
1 |
|
cB |
⊢ 𝐵 |
2 |
|
cC |
⊢ 𝐶 |
3 |
|
cD |
⊢ 𝐷 |
4 |
0 1 2 3
|
cs4 |
⊢ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 |
5 |
0 1 2
|
cs3 |
⊢ 〈“ 𝐴 𝐵 𝐶 ”〉 |
6 |
|
cconcat |
⊢ ++ |
7 |
3
|
cs1 |
⊢ 〈“ 𝐷 ”〉 |
8 |
5 7 6
|
co |
⊢ ( 〈“ 𝐴 𝐵 𝐶 ”〉 ++ 〈“ 𝐷 ”〉 ) |
9 |
4 8
|
wceq |
⊢ 〈“ 𝐴 𝐵 𝐶 𝐷 ”〉 = ( 〈“ 𝐴 𝐵 𝐶 ”〉 ++ 〈“ 𝐷 ”〉 ) |