Theorem mat1ric

Description: A ring is isomorphic to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 30-Dec-2019)

	Ref	Expression
Hypothesis	mat1ric.a	|- A = ( { E } Mat R )
Assertion	mat1ric	|- ( ( R e. Ring /\ E e. V ) -> R ~=r A )

Proof

Step	Hyp	Ref	Expression
1		mat1ric.a	|- A = ( { E } Mat R )
2		eqid	|- ( Base ` R ) = ( Base ` R )
3		eqid	|- ( Base ` A ) = ( Base ` A )
4		eqid	|- <. E , E >. = <. E , E >.
5		opeq2	|- ( x = y -> <. <. E , E >. , x >. = <. <. E , E >. , y >. )
6	5	sneqd	|- ( x = y -> { <. <. E , E >. , x >. } = { <. <. E , E >. , y >. } )
7	6	cbvmptv	|- ( x e. ( Base ` R ) |-> { <. <. E , E >. , x >. } ) = ( y e. ( Base ` R ) |-> { <. <. E , E >. , y >. } )
8	2 1 3 4 7	mat1rngiso	|- ( ( R e. Ring /\ E e. V ) -> ( x e. ( Base ` R ) |-> { <. <. E , E >. , x >. } ) e. ( R RingIso A ) )
9	8	ne0d	|- ( ( R e. Ring /\ E e. V ) -> ( R RingIso A ) =/= (/) )
10		brric	|- ( R ~=r A <-> ( R RingIso A ) =/= (/) )
11	9 10	sylibr	|- ( ( R e. Ring /\ E e. V ) -> R ~=r A )