Metamath Proof Explorer

Theorem dmatid

Description: The identity matrix is a diagonal matrix. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatid.a 
|- A = ( N Mat R )
dmatid.b 
|- B = ( Base ` A )
dmatid.0 
|- .0. = ( 0g ` R )
dmatid.d 
|- D = ( N DMat R )
Assertion dmatid 
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. D )

Proof

Step Hyp Ref Expression
1 dmatid.a 
 |-  A = ( N Mat R )
2 dmatid.b 
 |-  B = ( Base ` A )
3 dmatid.0 
 |-  .0. = ( 0g ` R )
4 dmatid.d 
 |-  D = ( N DMat R )
5 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
6 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
7 2 6 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
8 5 7 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 simpl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
11 10 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> N e. Fin )
12 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
13 12 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
14 simpl 
 |-  ( ( i e. N /\ j e. N ) -> i e. N )
15 14 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
16 simpr 
 |-  ( ( i e. N /\ j e. N ) -> j e. N )
17 16 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
18 1 9 3 11 13 15 17 6 mat1ov 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( i ( 1r ` A ) j ) = if ( i = j , ( 1r ` R ) , .0. ) )
19 ifnefalse 
 |-  ( i =/= j -> if ( i = j , ( 1r ` R ) , .0. ) = .0. )
20 18 19 sylan9eq 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i ( 1r ` A ) j ) = .0. )
21 20 ex 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( i =/= j -> ( i ( 1r ` A ) j ) = .0. ) )
22 21 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. i e. N A. j e. N ( i =/= j -> ( i ( 1r ` A ) j ) = .0. ) )
23 1 2 3 4 dmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( 1r ` A ) e. D <-> ( ( 1r ` A ) e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i ( 1r ` A ) j ) = .0. ) ) ) )
24 8 22 23 mpbir2and 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. D )