Metamath Proof Explorer

Theorem scmatf1

Description: There is a 1-1 function from a ring to any ring of scalar matrices with positive dimension over this ring. (Contributed by AV, 25-Dec-2019)

Ref Expression
Hypotheses scmatrhmval.k 
|- K = ( Base ` R )
scmatrhmval.a 
|- A = ( N Mat R )
scmatrhmval.o 
|- .1. = ( 1r ` A )
scmatrhmval.t 
|- .* = ( .s ` A )
scmatrhmval.f 
|- F = ( x e. K |-> ( x .* .1. ) )
scmatrhmval.c 
|- C = ( N ScMat R )
Assertion scmatf1 
|- ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-> C )

Proof

Step Hyp Ref Expression
1 scmatrhmval.k 
 |-  K = ( Base ` R )
2 scmatrhmval.a 
 |-  A = ( N Mat R )
3 scmatrhmval.o 
 |-  .1. = ( 1r ` A )
4 scmatrhmval.t 
 |-  .* = ( .s ` A )
5 scmatrhmval.f 
 |-  F = ( x e. K |-> ( x .* .1. ) )
6 scmatrhmval.c 
 |-  C = ( N ScMat R )
7 1 2 3 4 5 6 scmatf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> F : K --> C )
8 7 3adant2 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K --> C )
9 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
10 simpl 
 |-  ( ( y e. K /\ z e. K ) -> y e. K )
11 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ y e. K ) -> ( F ` y ) = ( y .* .1. ) )
12 9 10 11 syl2an 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` y ) = ( y .* .1. ) )
13 simpr 
 |-  ( ( y e. K /\ z e. K ) -> z e. K )
14 1 2 3 4 5 scmatrhmval 
 |-  ( ( R e. Ring /\ z e. K ) -> ( F ` z ) = ( z .* .1. ) )
15 9 13 14 syl2an 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( F ` z ) = ( z .* .1. ) )
16 12 15 eqeq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( F ` y ) = ( F ` z ) <-> ( y .* .1. ) = ( z .* .1. ) ) )
17 16 3adantl2 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( F ` y ) = ( F ` z ) <-> ( y .* .1. ) = ( z .* .1. ) ) )
18 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
19 eqid 
 |-  ( Base ` A ) = ( Base ` A )
20 19 3 ringidcl 
 |-  ( A e. Ring -> .1. e. ( Base ` A ) )
21 18 20 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. e. ( Base ` A ) )
22 21 10 anim12ci 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( y e. K /\ .1. e. ( Base ` A ) ) )
23 1 2 19 4 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ .1. e. ( Base ` A ) ) ) -> ( y .* .1. ) e. ( Base ` A ) )
24 22 23 syldan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( y .* .1. ) e. ( Base ` A ) )
25 21 13 anim12ci 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( z e. K /\ .1. e. ( Base ` A ) ) )
26 1 2 19 4 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( z e. K /\ .1. e. ( Base ` A ) ) ) -> ( z .* .1. ) e. ( Base ` A ) )
27 25 26 syldan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( z .* .1. ) e. ( Base ` A ) )
28 24 27 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y .* .1. ) e. ( Base ` A ) /\ ( z .* .1. ) e. ( Base ` A ) ) )
29 28 3adantl2 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y .* .1. ) e. ( Base ` A ) /\ ( z .* .1. ) e. ( Base ` A ) ) )
30 2 19 eqmat 
 |-  ( ( ( y .* .1. ) e. ( Base ` A ) /\ ( z .* .1. ) e. ( Base ` A ) ) -> ( ( y .* .1. ) = ( z .* .1. ) <-> A. i e. N A. j e. N ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) ) )
31 29 30 syl 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y .* .1. ) = ( z .* .1. ) <-> A. i e. N A. j e. N ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) ) )
32 difsnid 
 |-  ( i e. N -> ( ( N \ { i } ) u. { i } ) = N )
33 32 eqcomd 
 |-  ( i e. N -> N = ( ( N \ { i } ) u. { i } ) )
34 33 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> N = ( ( N \ { i } ) u. { i } ) )
35 34 raleqdv 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( A. j e. N ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) <-> A. j e. ( ( N \ { i } ) u. { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) ) )
36 oveq2 
 |-  ( j = i -> ( i ( y .* .1. ) j ) = ( i ( y .* .1. ) i ) )
37 oveq2 
 |-  ( j = i -> ( i ( z .* .1. ) j ) = ( i ( z .* .1. ) i ) )
38 36 37 eqeq12d 
 |-  ( j = i -> ( ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) <-> ( i ( y .* .1. ) i ) = ( i ( z .* .1. ) i ) ) )
39 38 ralunsn 
 |-  ( i e. N -> ( A. j e. ( ( N \ { i } ) u. { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) <-> ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ ( i ( y .* .1. ) i ) = ( i ( z .* .1. ) i ) ) ) )
40 39 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( A. j e. ( ( N \ { i } ) u. { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) <-> ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ ( i ( y .* .1. ) i ) = ( i ( z .* .1. ) i ) ) ) )
41 10 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ y e. K ) )
42 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. K ) <-> ( ( N e. Fin /\ R e. Ring ) /\ y e. K ) )
43 41 42 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( N e. Fin /\ R e. Ring /\ y e. K ) )
44 id 
 |-  ( i e. N -> i e. N )
45 44 44 jca 
 |-  ( i e. N -> ( i e. N /\ i e. N ) )
46 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
47 2 1 46 3 4 scmatscmide 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ y e. K ) /\ ( i e. N /\ i e. N ) ) -> ( i ( y .* .1. ) i ) = if ( i = i , y , ( 0g ` R ) ) )
48 43 45 47 syl2an 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( i ( y .* .1. ) i ) = if ( i = i , y , ( 0g ` R ) ) )
49 eqid 
 |-  i = i
50 49 iftruei 
 |-  if ( i = i , y , ( 0g ` R ) ) = y
51 48 50 eqtrdi 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( i ( y .* .1. ) i ) = y )
52 13 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ z e. K ) )
53 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ z e. K ) <-> ( ( N e. Fin /\ R e. Ring ) /\ z e. K ) )
54 52 53 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( N e. Fin /\ R e. Ring /\ z e. K ) )
55 2 1 46 3 4 scmatscmide 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ z e. K ) /\ ( i e. N /\ i e. N ) ) -> ( i ( z .* .1. ) i ) = if ( i = i , z , ( 0g ` R ) ) )
56 54 45 55 syl2an 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( i ( z .* .1. ) i ) = if ( i = i , z , ( 0g ` R ) ) )
57 49 iftruei 
 |-  if ( i = i , z , ( 0g ` R ) ) = z
58 56 57 eqtrdi 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( i ( z .* .1. ) i ) = z )
59 51 58 eqeq12d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( ( i ( y .* .1. ) i ) = ( i ( z .* .1. ) i ) <-> y = z ) )
60 59 anbi2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ ( i ( y .* .1. ) i ) = ( i ( z .* .1. ) i ) ) <-> ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ y = z ) ) )
61 35 40 60 3bitrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) /\ i e. N ) -> ( A. j e. N ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) <-> ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ y = z ) ) )
62 61 ralbidva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( A. i e. N A. j e. N ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) <-> A. i e. N ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ y = z ) ) )
63 62 3adantl2 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( A. i e. N A. j e. N ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) <-> A. i e. N ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ y = z ) ) )
64 r19.26 
 |-  ( A. i e. N ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ y = z ) <-> ( A. i e. N A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ A. i e. N y = z ) )
65 rspn0 
 |-  ( N =/= (/) -> ( A. i e. N y = z -> y = z ) )
66 65 3ad2ant2 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> ( A. i e. N y = z -> y = z ) )
67 66 adantr 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( A. i e. N y = z -> y = z ) )
68 67 com12 
 |-  ( A. i e. N y = z -> ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> y = z ) )
69 64 68 simplbiim 
 |-  ( A. i e. N ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ y = z ) -> ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> y = z ) )
70 69 com12 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( A. i e. N ( A. j e. ( N \ { i } ) ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) /\ y = z ) -> y = z ) )
71 63 70 sylbid 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( A. i e. N A. j e. N ( i ( y .* .1. ) j ) = ( i ( z .* .1. ) j ) -> y = z ) )
72 31 71 sylbid 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( y .* .1. ) = ( z .* .1. ) -> y = z ) )
73 17 72 sylbid 
 |-  ( ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) /\ ( y e. K /\ z e. K ) ) -> ( ( F ` y ) = ( F ` z ) -> y = z ) )
74 73 ralrimivva 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> A. y e. K A. z e. K ( ( F ` y ) = ( F ` z ) -> y = z ) )
75 dff13 
 |-  ( F : K -1-1-> C <-> ( F : K --> C /\ A. y e. K A. z e. K ( ( F ` y ) = ( F ` z ) -> y = z ) ) )
76 8 74 75 sylanbrc 
 |-  ( ( N e. Fin /\ N =/= (/) /\ R e. Ring ) -> F : K -1-1-> C )