Metamath Proof Explorer


Definition df-scmat

Description: Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in Connell p. 57: "Ascalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cI_n". (Contributed by AV, 8-Dec-2019)

Ref Expression
Assertion df-scmat
|- ScMat = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cscmat
 |-  ScMat
1 vn
 |-  n
2 cfn
 |-  Fin
3 vr
 |-  r
4 cvv
 |-  _V
5 1 cv
 |-  n
6 cmat
 |-  Mat
7 3 cv
 |-  r
8 5 7 6 co
 |-  ( n Mat r )
9 va
 |-  a
10 vm
 |-  m
11 cbs
 |-  Base
12 9 cv
 |-  a
13 12 11 cfv
 |-  ( Base ` a )
14 vc
 |-  c
15 7 11 cfv
 |-  ( Base ` r )
16 10 cv
 |-  m
17 14 cv
 |-  c
18 cvsca
 |-  .s
19 12 18 cfv
 |-  ( .s ` a )
20 cur
 |-  1r
21 12 20 cfv
 |-  ( 1r ` a )
22 17 21 19 co
 |-  ( c ( .s ` a ) ( 1r ` a ) )
23 16 22 wceq
 |-  m = ( c ( .s ` a ) ( 1r ` a ) )
24 23 14 15 wrex
 |-  E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) )
25 24 10 13 crab
 |-  { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) }
26 9 8 25 csb
 |-  [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) }
27 1 3 2 4 26 cmpo
 |-  ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } )
28 0 27 wceq
 |-  ScMat = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ { m e. ( Base ` a ) | E. c e. ( Base ` r ) m = ( c ( .s ` a ) ( 1r ` a ) ) } )