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

Metamath Proof Explorer

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 )