Metamath Proof Explorer

Theorem dmatval

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

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

Proof

Step Hyp Ref Expression
1 dmatval.a 
 |-  A = ( N Mat R )
2 dmatval.b 
 |-  B = ( Base ` A )
3 dmatval.0 
 |-  .0. = ( 0g ` R )
4 dmatval.d 
 |-  D = ( N DMat R )
5 df-dmat 
 |-  DMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } )
6 5 a1i 
 |-  ( ( N e. Fin /\ R e. V ) -> DMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat r ) ) | A. i e. n A. j e. n ( i =/= j -> ( i m j ) = ( 0g ` r ) ) } ) )
7 oveq12 
 |-  ( ( n = N /\ r = R ) -> ( n Mat r ) = ( N Mat R ) )
8 7 fveq2d 
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = ( Base ` ( N Mat R ) ) )
9 1 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
10 2 9 eqtri 
 |-  B = ( Base ` ( N Mat R ) )
11 8 10 eqtr4di 
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat r ) ) = B )
12 simpl 
 |-  ( ( n = N /\ r = R ) -> n = N )
13 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
14 13 3 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
15 14 adantl 
 |-  ( ( n = N /\ r = R ) -> ( 0g ` r ) = .0. )
16 15 eqeq2d 
 |-  ( ( n = N /\ r = R ) -> ( ( i m j ) = ( 0g ` r ) <-> ( i m j ) = .0. ) )
17 16 imbi2d 
 |-  ( ( n = N /\ r = R ) -> ( ( i =/= j -> ( i m j ) = ( 0g ` r ) ) <-> ( i =/= j -> ( i m j ) = .0. ) ) )
18 12 17 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. ) ) )
19 12 18 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. ) ) )
20 11 19 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. ) } )
21 20 adantl 
 |-  ( ( ( N e. Fin /\ R e. V ) /\ ( 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. ) } )
22 simpl 
 |-  ( ( N e. Fin /\ R e. V ) -> N e. Fin )
23 elex 
 |-  ( R e. V -> R e. _V )
24 23 adantl 
 |-  ( ( N e. Fin /\ R e. V ) -> R e. _V )
25 2 fvexi 
 |-  B e. _V
26 rabexg 
 |-  ( B e. _V -> { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } e. _V )
27 25 26 mp1i 
 |-  ( ( N e. Fin /\ R e. V ) -> { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } e. _V )
28 6 21 22 24 27 ovmpod 
 |-  ( ( N e. Fin /\ R e. V ) -> ( N DMat R ) = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
29 4 28 syl5eq 
 |-  ( ( N e. Fin /\ R e. V ) -> D = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )