Step |
Hyp |
Ref |
Expression |
1 |
|
srapart.a |
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) ) |
2 |
|
srapart.s |
|- ( ph -> S C_ ( Base ` W ) ) |
3 |
|
dsid |
|- dist = Slot ( dist ` ndx ) |
4 |
|
slotsdnscsi |
|- ( ( dist ` ndx ) =/= ( Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) ) |
5 |
4
|
simp1i |
|- ( dist ` ndx ) =/= ( Scalar ` ndx ) |
6 |
5
|
necomi |
|- ( Scalar ` ndx ) =/= ( dist ` ndx ) |
7 |
4
|
simp2i |
|- ( dist ` ndx ) =/= ( .s ` ndx ) |
8 |
7
|
necomi |
|- ( .s ` ndx ) =/= ( dist ` ndx ) |
9 |
4
|
simp3i |
|- ( dist ` ndx ) =/= ( .i ` ndx ) |
10 |
9
|
necomi |
|- ( .i ` ndx ) =/= ( dist ` ndx ) |
11 |
1 2 3 6 8 10
|
sralem |
|- ( ph -> ( dist ` W ) = ( dist ` A ) ) |