Metamath Proof Explorer

Definition df-scmatalt

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-scmatalt 
|- ScMatALT = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cscmatalt 
 |-  ScMatALT
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 9 cv 
 |-  a
11 cress 
 |-  |`s
12 vm 
 |-  m
13 cbs 
 |-  Base
14 10 13 cfv 
 |-  ( Base ` a )
15 vc 
 |-  c
16 7 13 cfv 
 |-  ( Base ` r )
17 vi 
 |-  i
18 vj 
 |-  j
19 17 cv 
 |-  i
20 12 cv 
 |-  m
21 18 cv 
 |-  j
22 19 21 20 co 
 |-  ( i m j )
23 19 21 wceq 
 |-  i = j
24 15 cv 
 |-  c
25 c0g 
 |-  0g
26 7 25 cfv 
 |-  ( 0g ` r )
27 23 24 26 cif 
 |-  if ( i = j , c , ( 0g ` r ) )
28 22 27 wceq 
 |-  ( i m j ) = if ( i = j , c , ( 0g ` r ) )
29 28 18 5 wral 
 |-  A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) )
30 29 17 5 wral 
 |-  A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) )
31 30 15 16 wrex 
 |-  E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) )
32 31 12 14 crab 
 |-  { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) }
33 10 32 11 co 
 |-  ( a |`s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } )
34 9 8 33 csb 
 |-  [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } )
35 1 3 2 4 34 cmpo 
 |-  ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } ) )
36 0 35 wceq 
 |-  ScMatALT = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | E. c e. ( Base ` r ) A. i e. n A. j e. n ( i m j ) = if ( i = j , c , ( 0g ` r ) ) } ) )