Metamath Proof Explorer

Theorem dmatelnd

Description: An extradiagonal entry of a diagonal matrix is equal to zero. (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 dmatelnd 
|- ( ( ( N e. Fin /\ R e. Ring /\ X e. D ) /\ ( I e. N /\ J e. N /\ I =/= J ) ) -> ( I X J ) = .0. )

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 2 3 4 dmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. D <-> ( X e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i X j ) = .0. ) ) ) )
6 neeq1 
 |-  ( i = I -> ( i =/= j <-> I =/= j ) )
7 oveq1 
 |-  ( i = I -> ( i X j ) = ( I X j ) )
8 7 eqeq1d 
 |-  ( i = I -> ( ( i X j ) = .0. <-> ( I X j ) = .0. ) )
9 6 8 imbi12d 
 |-  ( i = I -> ( ( i =/= j -> ( i X j ) = .0. ) <-> ( I =/= j -> ( I X j ) = .0. ) ) )
10 neeq2 
 |-  ( j = J -> ( I =/= j <-> I =/= J ) )
11 oveq2 
 |-  ( j = J -> ( I X j ) = ( I X J ) )
12 11 eqeq1d 
 |-  ( j = J -> ( ( I X j ) = .0. <-> ( I X J ) = .0. ) )
13 10 12 imbi12d 
 |-  ( j = J -> ( ( I =/= j -> ( I X j ) = .0. ) <-> ( I =/= J -> ( I X J ) = .0. ) ) )
14 9 13 rspc2v 
 |-  ( ( I e. N /\ J e. N ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i X j ) = .0. ) -> ( I =/= J -> ( I X J ) = .0. ) ) )
15 14 com23 
 |-  ( ( I e. N /\ J e. N ) -> ( I =/= J -> ( A. i e. N A. j e. N ( i =/= j -> ( i X j ) = .0. ) -> ( I X J ) = .0. ) ) )
16 15 3impia 
 |-  ( ( I e. N /\ J e. N /\ I =/= J ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i X j ) = .0. ) -> ( I X J ) = .0. ) )
17 16 com12 
 |-  ( A. i e. N A. j e. N ( i =/= j -> ( i X j ) = .0. ) -> ( ( I e. N /\ J e. N /\ I =/= J ) -> ( I X J ) = .0. ) )
18 17 2a1i 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. B -> ( A. i e. N A. j e. N ( i =/= j -> ( i X j ) = .0. ) -> ( ( I e. N /\ J e. N /\ I =/= J ) -> ( I X J ) = .0. ) ) ) )
19 18 impd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( X e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i X j ) = .0. ) ) -> ( ( I e. N /\ J e. N /\ I =/= J ) -> ( I X J ) = .0. ) ) )
20 5 19 sylbid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. D -> ( ( I e. N /\ J e. N /\ I =/= J ) -> ( I X J ) = .0. ) ) )
21 20 3impia 
 |-  ( ( N e. Fin /\ R e. Ring /\ X e. D ) -> ( ( I e. N /\ J e. N /\ I =/= J ) -> ( I X J ) = .0. ) )
22 21 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ X e. D ) /\ ( I e. N /\ J e. N /\ I =/= J ) ) -> ( I X J ) = .0. )