Metamath Proof Explorer


Definition df-s7

Description: Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion df-s7
|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cB
 |-  B
2 cC
 |-  C
3 cD
 |-  D
4 cE
 |-  E
5 cF
 |-  F
6 cG
 |-  G
7 0 1 2 3 4 5 6 cs7
 |-  <" A B C D E F G ">
8 0 1 2 3 4 5 cs6
 |-  <" A B C D E F ">
9 cconcat
 |-  ++
10 6 cs1
 |-  <" G ">
11 8 10 9 co
 |-  ( <" A B C D E F "> ++ <" G "> )
12 7 11 wceq
 |-  <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )