Theorem mat1rhm

Description: There is a ring homomorphism 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	mat1rhm	|- ( ( R e. Ring /\ E e. V ) -> F e. ( R RingHom 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		simpl	|- ( ( R e. Ring /\ E e. V ) -> R e. Ring )
7		snfi	|- { E } e. Fin
8	2	matring	|- ( ( { E } e. Fin /\ R e. Ring ) -> A e. Ring )
9	7 6 8	sylancr	|- ( ( R e. Ring /\ E e. V ) -> A e. Ring )
10	1 2 3 4 5	mat1ghm	|- ( ( R e. Ring /\ E e. V ) -> F e. ( R GrpHom A ) )
11		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
12		eqid	|- ( mulGrp ` A ) = ( mulGrp ` A )
13	1 2 3 4 5 11 12	mat1mhm	|- ( ( R e. Ring /\ E e. V ) -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` A ) ) )
14	10 13	jca	|- ( ( R e. Ring /\ E e. V ) -> ( F e. ( R GrpHom A ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` A ) ) ) )
15	11 12	isrhm	|- ( F e. ( R RingHom A ) <-> ( ( R e. Ring /\ A e. Ring ) /\ ( F e. ( R GrpHom A ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` A ) ) ) ) )
16	6 9 14 15	syl21anbrc	|- ( ( R e. Ring /\ E e. V ) -> F e. ( R RingHom A ) )