2 |
|
eqid |
|- { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } = { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } |
3 |
2
|
ring1 |
|- ( z e. _V -> { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } e. Ring ) |
4 |
|
ne0i |
|- ( { <. ( Base ` ndx ) , { z } >. , <. ( +g ` ndx ) , { <. <. z , z >. , z >. } >. , <. ( .r ` ndx ) , { <. <. z , z >. , z >. } >. } e. Ring -> Ring =/= (/) ) |