Step |
Hyp |
Ref |
Expression |
1 |
|
ipspart.a |
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } ) |
2 |
|
eqid |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } |
3 |
2
|
rngstr |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } Struct <. 1 , 3 >. |
4 |
|
5nn |
|- 5 e. NN |
5 |
|
scandx |
|- ( Scalar ` ndx ) = 5 |
6 |
|
5lt6 |
|- 5 < 6 |
7 |
|
6nn |
|- 6 e. NN |
8 |
|
vscandx |
|- ( .s ` ndx ) = 6 |
9 |
|
6lt8 |
|- 6 < 8 |
10 |
|
8nn |
|- 8 e. NN |
11 |
|
ipndx |
|- ( .i ` ndx ) = 8 |
12 |
4 5 6 7 8 9 10 11
|
strle3 |
|- { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } Struct <. 5 , 8 >. |
13 |
|
3lt5 |
|- 3 < 5 |
14 |
3 12 13
|
strleun |
|- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , I >. } ) Struct <. 1 , 8 >. |
15 |
1 14
|
eqbrtri |
|- A Struct <. 1 , 8 >. |