Step |
Hyp |
Ref |
Expression |
1 |
|
mat1rhmval.k |
|- K = ( Base ` R ) |
2 |
|
mat1rhmval.a |
|- A = ( { E } Mat R ) |
3 |
|
mat1rhmval.b |
|- B = ( Base ` A ) |
4 |
|
mat1rhmval.o |
|- O = <. E , E >. |
5 |
|
mat1rhmval.f |
|- F = ( x e. K |-> { <. O , x >. } ) |
6 |
2 1 4
|
mat1dimbas |
|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> { <. O , X >. } e. ( Base ` A ) ) |
7 |
1 2 3 4 5
|
mat1rhmval |
|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( F ` X ) = { <. O , X >. } ) |
8 |
3
|
a1i |
|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> B = ( Base ` A ) ) |
9 |
6 7 8
|
3eltr4d |
|- ( ( R e. Ring /\ E e. V /\ X e. K ) -> ( F ` X ) e. B ) |