Metamath Proof Explorer

Theorem mat1scmat

Description: A 1-dimensional matrix over a ring is always a scalar matrix (and therefore, by scmatdmat , also a diagonal matrix). (Contributed by AV, 21-Dec-2019)

Ref Expression
Hypotheses mat1scmat.a 
|- A = ( N Mat R )
mat1scmat.b 
|- B = ( Base ` A )
Assertion mat1scmat 
|- ( ( N e. V /\ ( # ` N ) = 1 /\ R e. Ring ) -> ( M e. B -> M e. ( N ScMat R ) ) )

Proof

Step Hyp Ref Expression
1 mat1scmat.a 
 |-  A = ( N Mat R )
2 mat1scmat.b 
 |-  B = ( Base ` A )
3 hash1snb 
 |-  ( N e. V -> ( ( # ` N ) = 1 <-> E. e N = { e } ) )
4 simpr 
 |-  ( ( R e. Ring /\ M e. ( Base ` ( { e } Mat R ) ) ) -> M e. ( Base ` ( { e } Mat R ) ) )
5 eqid 
 |-  ( { e } Mat R ) = ( { e } Mat R )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  <. e , e >. = <. e , e >.
8 5 6 7 mat1dimelbas 
 |-  ( ( R e. Ring /\ e e. _V ) -> ( M e. ( Base ` ( { e } Mat R ) ) <-> E. c e. ( Base ` R ) M = { <. <. e , e >. , c >. } ) )
9 8 elvd 
 |-  ( R e. Ring -> ( M e. ( Base ` ( { e } Mat R ) ) <-> E. c e. ( Base ` R ) M = { <. <. e , e >. , c >. } ) )
10 simpr 
 |-  ( ( ( R e. Ring /\ c e. ( Base ` R ) ) /\ M = { <. <. e , e >. , c >. } ) -> M = { <. <. e , e >. , c >. } )
11 vex 
 |-  e e. _V
12 11 a1i 
 |-  ( c e. ( Base ` R ) -> e e. _V )
13 5 6 7 mat1dimid 
 |-  ( ( R e. Ring /\ e e. _V ) -> ( 1r ` ( { e } Mat R ) ) = { <. <. e , e >. , ( 1r ` R ) >. } )
14 12 13 sylan2 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> ( 1r ` ( { e } Mat R ) ) = { <. <. e , e >. , ( 1r ` R ) >. } )
15 14 oveq2d 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) = ( c ( .s ` ( { e } Mat R ) ) { <. <. e , e >. , ( 1r ` R ) >. } ) )
16 simpl 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> R e. Ring )
17 16 11 jctir 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> ( R e. Ring /\ e e. _V ) )
18 simpr 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> c e. ( Base ` R ) )
19 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
20 6 19 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
21 20 adantr 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> ( 1r ` R ) e. ( Base ` R ) )
22 5 6 7 mat1dimscm 
 |-  ( ( ( R e. Ring /\ e e. _V ) /\ ( c e. ( Base ` R ) /\ ( 1r ` R ) e. ( Base ` R ) ) ) -> ( c ( .s ` ( { e } Mat R ) ) { <. <. e , e >. , ( 1r ` R ) >. } ) = { <. <. e , e >. , ( c ( .r ` R ) ( 1r ` R ) ) >. } )
23 17 18 21 22 syl12anc 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> ( c ( .s ` ( { e } Mat R ) ) { <. <. e , e >. , ( 1r ` R ) >. } ) = { <. <. e , e >. , ( c ( .r ` R ) ( 1r ` R ) ) >. } )
24 eqid 
 |-  ( .r ` R ) = ( .r ` R )
25 6 24 19 ringridm 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> ( c ( .r ` R ) ( 1r ` R ) ) = c )
26 25 opeq2d 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> <. <. e , e >. , ( c ( .r ` R ) ( 1r ` R ) ) >. = <. <. e , e >. , c >. )
27 26 sneqd 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> { <. <. e , e >. , ( c ( .r ` R ) ( 1r ` R ) ) >. } = { <. <. e , e >. , c >. } )
28 15 23 27 3eqtrrd 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> { <. <. e , e >. , c >. } = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) )
29 28 adantr 
 |-  ( ( ( R e. Ring /\ c e. ( Base ` R ) ) /\ M = { <. <. e , e >. , c >. } ) -> { <. <. e , e >. , c >. } = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) )
30 10 29 eqtrd 
 |-  ( ( ( R e. Ring /\ c e. ( Base ` R ) ) /\ M = { <. <. e , e >. , c >. } ) -> M = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) )
31 30 ex 
 |-  ( ( R e. Ring /\ c e. ( Base ` R ) ) -> ( M = { <. <. e , e >. , c >. } -> M = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) ) )
32 31 reximdva 
 |-  ( R e. Ring -> ( E. c e. ( Base ` R ) M = { <. <. e , e >. , c >. } -> E. c e. ( Base ` R ) M = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) ) )
33 9 32 sylbid 
 |-  ( R e. Ring -> ( M e. ( Base ` ( { e } Mat R ) ) -> E. c e. ( Base ` R ) M = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) ) )
34 33 imp 
 |-  ( ( R e. Ring /\ M e. ( Base ` ( { e } Mat R ) ) ) -> E. c e. ( Base ` R ) M = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) )
35 snfi 
 |-  { e } e. Fin
36 simpl 
 |-  ( ( R e. Ring /\ M e. ( Base ` ( { e } Mat R ) ) ) -> R e. Ring )
37 eqid 
 |-  ( Base ` ( { e } Mat R ) ) = ( Base ` ( { e } Mat R ) )
38 eqid 
 |-  ( 1r ` ( { e } Mat R ) ) = ( 1r ` ( { e } Mat R ) )
39 eqid 
 |-  ( .s ` ( { e } Mat R ) ) = ( .s ` ( { e } Mat R ) )
40 eqid 
 |-  ( { e } ScMat R ) = ( { e } ScMat R )
41 6 5 37 38 39 40 scmatel 
 |-  ( ( { e } e. Fin /\ R e. Ring ) -> ( M e. ( { e } ScMat R ) <-> ( M e. ( Base ` ( { e } Mat R ) ) /\ E. c e. ( Base ` R ) M = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) ) ) )
42 35 36 41 sylancr 
 |-  ( ( R e. Ring /\ M e. ( Base ` ( { e } Mat R ) ) ) -> ( M e. ( { e } ScMat R ) <-> ( M e. ( Base ` ( { e } Mat R ) ) /\ E. c e. ( Base ` R ) M = ( c ( .s ` ( { e } Mat R ) ) ( 1r ` ( { e } Mat R ) ) ) ) ) )
43 4 34 42 mpbir2and 
 |-  ( ( R e. Ring /\ M e. ( Base ` ( { e } Mat R ) ) ) -> M e. ( { e } ScMat R ) )
44 43 ex 
 |-  ( R e. Ring -> ( M e. ( Base ` ( { e } Mat R ) ) -> M e. ( { e } ScMat R ) ) )
45 1 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
46 2 45 eqtri 
 |-  B = ( Base ` ( N Mat R ) )
47 fvoveq1 
 |-  ( N = { e } -> ( Base ` ( N Mat R ) ) = ( Base ` ( { e } Mat R ) ) )
48 46 47 eqtrid 
 |-  ( N = { e } -> B = ( Base ` ( { e } Mat R ) ) )
49 48 eleq2d 
 |-  ( N = { e } -> ( M e. B <-> M e. ( Base ` ( { e } Mat R ) ) ) )
50 oveq1 
 |-  ( N = { e } -> ( N ScMat R ) = ( { e } ScMat R ) )
51 50 eleq2d 
 |-  ( N = { e } -> ( M e. ( N ScMat R ) <-> M e. ( { e } ScMat R ) ) )
52 49 51 imbi12d 
 |-  ( N = { e } -> ( ( M e. B -> M e. ( N ScMat R ) ) <-> ( M e. ( Base ` ( { e } Mat R ) ) -> M e. ( { e } ScMat R ) ) ) )
53 44 52 imbitrrid 
 |-  ( N = { e } -> ( R e. Ring -> ( M e. B -> M e. ( N ScMat R ) ) ) )
54 53 exlimiv 
 |-  ( E. e N = { e } -> ( R e. Ring -> ( M e. B -> M e. ( N ScMat R ) ) ) )
55 3 54 biimtrdi 
 |-  ( N e. V -> ( ( # ` N ) = 1 -> ( R e. Ring -> ( M e. B -> M e. ( N ScMat R ) ) ) ) )
56 55 3imp 
 |-  ( ( N e. V /\ ( # ` N ) = 1 /\ R e. Ring ) -> ( M e. B -> M e. ( N ScMat R ) ) )