Theorem mat1rngiso

Description: There is a ring isomorphism from a ring to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019)

	Ref	Expression
Hypotheses	mat1rhmval.k	|- K = ( Base ` R )
	mat1rhmval.a	|- A = ( { E } Mat R )
	mat1rhmval.b	|- B = ( Base ` A )
	mat1rhmval.o	|- O = <. E , E >.
	mat1rhmval.f	|- F = ( x e. K |-> { <. O , x >. } )
Assertion	mat1rngiso	|- ( ( R e. Ring /\ E e. V ) -> F e. ( R RingIso A ) )

Proof

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	1 2 3 4 5	mat1rhm	|- ( ( R e. Ring /\ E e. V ) -> F e. ( R RingHom A ) )
7	1 2 3 4 5	mat1f1o	|- ( ( R e. Ring /\ E e. V ) -> F : K -1-1-onto-> B )
8	1 3	isrim	|- ( F e. ( R RingIso A ) <-> ( F e. ( R RingHom A ) /\ F : K -1-1-onto-> B ) )
9	6 7 8	sylanbrc	|- ( ( R e. Ring /\ E e. V ) -> F e. ( R RingIso A ) )