Step |
Hyp |
Ref |
Expression |
1 |
|
2str1.g |
|- G = { <. ( Base ` ndx ) , B >. , <. N , .+ >. } |
2 |
|
2str1.b |
|- ( Base ` ndx ) < N |
3 |
|
2str1.n |
|- N e. NN |
4 |
|
eqid |
|- Slot N = Slot N |
5 |
4 3
|
ndxarg |
|- ( Slot N ` ndx ) = N |
6 |
5
|
eqcomi |
|- N = ( Slot N ` ndx ) |
7 |
6
|
opeq1i |
|- <. N , .+ >. = <. ( Slot N ` ndx ) , .+ >. |
8 |
7
|
preq2i |
|- { <. ( Base ` ndx ) , B >. , <. N , .+ >. } = { <. ( Base ` ndx ) , B >. , <. ( Slot N ` ndx ) , .+ >. } |
9 |
1 8
|
eqtri |
|- G = { <. ( Base ` ndx ) , B >. , <. ( Slot N ` ndx ) , .+ >. } |
10 |
|
basendx |
|- ( Base ` ndx ) = 1 |
11 |
10 2
|
eqbrtrri |
|- 1 < N |
12 |
9 4 11 3
|
2strstr |
|- G Struct <. 1 , N >. |
13 |
10
|
opeq1i |
|- <. ( Base ` ndx ) , N >. = <. 1 , N >. |
14 |
12 13
|
breqtrri |
|- G Struct <. ( Base ` ndx ) , N >. |