Metamath Proof Explorer

Theorem dmatALTval

Description: The algebra of N x N diagonal matrices over a ring R . (Contributed by AV, 8-Dec-2019)

Ref Expression
Hypotheses dmatALTval.a 
|- A = ( N Mat R )
dmatALTval.b 
|- B = ( Base ` A )
dmatALTval.0 
|- .0. = ( 0g ` R )
dmatALTval.d 
|- D = ( N DMatALT R )
Assertion dmatALTval 
|- ( ( N e. Fin /\ R e. _V ) -> D = ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )

Proof

Step Hyp Ref Expression
1 dmatALTval.a 
 |-  A = ( N Mat R )
2 dmatALTval.b 
 |-  B = ( Base ` A )
3 dmatALTval.0 
 |-  .0. = ( 0g ` R )
4 dmatALTval.d 
 |-  D = ( N DMatALT R )
5 ovexd 
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) e. _V )
6 id 
 |-  ( a = ( n Mat r ) -> a = ( n Mat r ) )
7 fveq2 
 |-  ( a = ( n Mat r ) -> ( Base ` a ) = ( Base ` ( n Mat r ) ) )
8 7 rabeqdv 
 |-  ( a = ( n Mat r ) -> { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } = { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } )
9 6 8 oveq12d 
 |-  ( a = ( n Mat r ) -> ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) = ( ( n Mat r ) |`s { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )
10 9 adantl 
 |-  ( ( ( n = N /\ r = R ) /\ a = ( n Mat r ) ) -> ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) = ( ( n Mat r ) |`s { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )
11 5 10 csbied 
 |-  ( ( n = N /\ r = R ) -> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) = ( ( n Mat r ) |`s { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )
12 oveq12 
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = ( N Mat R ) )
13 12 1 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = A )
14 13 fveq2d 
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = ( Base ` A ) )
15 14 2 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = B )
16 simpl 
 |-  ( ( n = N /\ r = R ) -> n = N )
17 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
18 17 3 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
19 18 adantl 
 |-  ( ( n = N /\ r = R ) -> ( 0g ` r ) = .0. )
20 19 eqeq2d 
 |-  ( ( n = N /\ r = R ) -> ( ( i m j ) = ( 0g ` r ) <-> ( i m j ) = .0. ) )
21 20 imbi2d 
 |-  ( ( n = N /\ r = R ) -> ( ( i =/= j -> ( i m j ) = ( 0g ` r ) ) <-> ( i =/= j -> ( i m j ) = .0. ) ) )
22 16 21 raleqbidv 
 |-  ( ( n = N /\ r = R ) -> ( A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) <-> A. j e. N ( i =/= j -> ( i m j ) = .0. ) ) )
23 16 22 raleqbidv 
 |-  ( ( n = N /\ r = R ) -> ( A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) <-> A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) ) )
24 15 23 rabeqbidv 
 |-  ( ( n = N /\ r = R ) -> { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
25 13 24 oveq12d 
 |-  ( ( n = N /\ r = R ) -> ( ( n Mat r ) |`s { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) = ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )
26 11 25 eqtrd 
 |-  ( ( n = N /\ r = R ) -> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) = ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )
27 df-dmatalt 
 |-  DMatALT = ( n e. Fin , r e. _V |-> [_ ( n Mat r ) / a ]_ ( a |`s { m e. ( Base ` a ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )
28 ovex 
 |-  ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) e. _V
29 26 27 28 ovmpoa 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( N DMatALT R ) = ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )
30 4 29 syl5eq 
 |-  ( ( N e. Fin /\ R e. _V ) -> D = ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )