Step |
Hyp |
Ref |
Expression |
1 |
|
idlsrgbas.1 |
Could not format S = ( IDLsrg ` R ) : No typesetting found for |- S = ( IDLsrg ` R ) with typecode |- |
2 |
|
idlsrgbas.2 |
|
3 |
2
|
fvexi |
|
4 |
|
eqid |
|
5 |
4
|
idlsrgstr |
|
6 |
|
baseid |
|
7 |
|
snsstp1 |
|
8 |
|
ssun1 |
|
9 |
7 8
|
sstri |
|
10 |
5 6 9
|
strfv |
|
11 |
3 10
|
ax-mp |
|
12 |
|
eqid |
|
13 |
|
eqid |
|
14 |
|
eqid |
|
15 |
2 12 13 14
|
idlsrgval |
Could not format ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i ( LSSum ` ( mulGrp ` R ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. I |-> { j e. I | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ I /\ i C_ j ) } >. } ) ) : No typesetting found for |- ( R e. V -> ( IDLsrg ` R ) = ( { <. ( Base ` ndx ) , I >. , <. ( +g ` ndx ) , ( LSSum ` R ) >. , <. ( .r ` ndx ) , ( i e. I , j e. I |-> ( ( RSpan ` R ) ` ( i ( LSSum ` ( mulGrp ` R ) ) j ) ) ) >. } u. { <. ( TopSet ` ndx ) , ran ( i e. I |-> { j e. I | -. i C_ j } ) >. , <. ( le ` ndx ) , { <. i , j >. | ( { i , j } C_ I /\ i C_ j ) } >. } ) ) with typecode |- |
16 |
1 15
|
syl5eq |
|
17 |
16
|
fveq2d |
|
18 |
11 17
|
eqtr4id |
|