Metamath Proof Explorer

Theorem mat1f1o

Description: There is a 1-1 function from a ring onto 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 mat1f1o 
|- ( ( R e. Ring /\ E e. V ) -> F : K -1-1-onto-> B )

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 fvexi 
 |-  K e. _V
7 opex 
 |-  <. E , E >. e. _V
8 4 7 eqeltri 
 |-  O e. _V
9 6 8 pm3.2i 
 |-  ( K e. _V /\ O e. _V )
10 vex 
 |-  x e. _V
11 8 10 xpsn 
 |-  ( { O } X. { x } ) = { <. O , x >. }
12 11 eqcomi 
 |-  { <. O , x >. } = ( { O } X. { x } )
13 12 mpteq2i 
 |-  ( x e. K |-> { <. O , x >. } ) = ( x e. K |-> ( { O } X. { x } ) )
14 13 mapsnf1o 
 |-  ( ( K e. _V /\ O e. _V ) -> ( x e. K |-> { <. O , x >. } ) : K -1-1-onto-> ( K ^m { O } ) )
15 9 14 mp1i 
 |-  ( ( R e. Ring /\ E e. V ) -> ( x e. K |-> { <. O , x >. } ) : K -1-1-onto-> ( K ^m { O } ) )
16 5 a1i 
 |-  ( ( R e. Ring /\ E e. V ) -> F = ( x e. K |-> { <. O , x >. } ) )
17 eqidd 
 |-  ( ( R e. Ring /\ E e. V ) -> K = K )
18 4 sneqi 
 |-  { O } = { <. E , E >. }
19 simpr 
 |-  ( ( R e. Ring /\ E e. V ) -> E e. V )
20 xpsng 
 |-  ( ( E e. V /\ E e. V ) -> ( { E } X. { E } ) = { <. E , E >. } )
21 19 20 sylancom 
 |-  ( ( R e. Ring /\ E e. V ) -> ( { E } X. { E } ) = { <. E , E >. } )
22 18 21 eqtr4id 
 |-  ( ( R e. Ring /\ E e. V ) -> { O } = ( { E } X. { E } ) )
23 22 oveq2d 
 |-  ( ( R e. Ring /\ E e. V ) -> ( K ^m { O } ) = ( K ^m ( { E } X. { E } ) ) )
24 snfi 
 |-  { E } e. Fin
25 simpl 
 |-  ( ( R e. Ring /\ E e. V ) -> R e. Ring )
26 2 1 matbas2 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> ( K ^m ( { E } X. { E } ) ) = ( Base ` A ) )
27 24 25 26 sylancr 
 |-  ( ( R e. Ring /\ E e. V ) -> ( K ^m ( { E } X. { E } ) ) = ( Base ` A ) )
28 23 27 eqtrd 
 |-  ( ( R e. Ring /\ E e. V ) -> ( K ^m { O } ) = ( Base ` A ) )
29 3 28 eqtr4id 
 |-  ( ( R e. Ring /\ E e. V ) -> B = ( K ^m { O } ) )
30 16 17 29 f1oeq123d 
 |-  ( ( R e. Ring /\ E e. V ) -> ( F : K -1-1-onto-> B <-> ( x e. K |-> { <. O , x >. } ) : K -1-1-onto-> ( K ^m { O } ) ) )
31 15 30 mpbird 
 |-  ( ( R e. Ring /\ E e. V ) -> F : K -1-1-onto-> B )