This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )