Metamath Proof Explorer

Theorem dmatsubcl

Description: The difference of two diagonal matrices 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 dmatsubcl 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( -g ` A ) Y ) 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 matgrp 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Grp )
6 5 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> A e. Grp )
7 1 2 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. D -> X e. B ) )
8 7 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ X e. D ) -> X e. B )
9 8 adantrr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> X e. B )
10 1 2 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Y e. D -> Y e. B ) )
11 10 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. D ) -> Y e. B )
12 11 adantrl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> Y e. B )
13 eqid 
 |-  ( -g ` A ) = ( -g ` A )
14 2 13 grpsubcl 
 |-  ( ( A e. Grp /\ X e. B /\ Y e. B ) -> ( X ( -g ` A ) Y ) e. B )
15 6 9 12 14 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( -g ` A ) Y ) e. B )
16 simpr 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
17 16 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> R e. Ring )
18 17 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
19 7 10 anim12d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( X e. D /\ Y e. D ) -> ( X e. B /\ Y e. B ) ) )
20 19 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X e. B /\ Y e. B ) )
21 20 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) -> ( X e. B /\ Y e. B ) )
22 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) -> ( i e. N /\ j e. N ) )
23 eqid 
 |-  ( -g ` R ) = ( -g ` R )
24 1 2 13 23 matsubgcell 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( X ( -g ` A ) Y ) j ) = ( ( i X j ) ( -g ` R ) ( i Y j ) ) )
25 18 21 22 24 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( X ( -g ` A ) Y ) j ) = ( ( i X j ) ( -g ` R ) ( i Y j ) ) )
26 25 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i ( X ( -g ` A ) Y ) j ) = ( ( i X j ) ( -g ` R ) ( i Y j ) ) )
27 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> N e. Fin )
28 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> X e. D )
29 27 17 28 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( N e. Fin /\ R e. Ring /\ X e. D ) )
30 29 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) -> ( N e. Fin /\ R e. Ring /\ X e. D ) )
31 30 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( N e. Fin /\ R e. Ring /\ X e. D ) )
32 simplrl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> i e. N )
33 simplrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> j e. N )
34 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> i =/= j )
35 1 2 3 4 dmatelnd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ X e. D ) /\ ( i e. N /\ j e. N /\ i =/= j ) ) -> ( i X j ) = .0. )
36 31 32 33 34 35 syl13anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i X j ) = .0. )
37 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> Y e. D )
38 27 17 37 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( N e. Fin /\ R e. Ring /\ Y e. D ) )
39 38 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) -> ( N e. Fin /\ R e. Ring /\ Y e. D ) )
40 39 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( N e. Fin /\ R e. Ring /\ Y e. D ) )
41 1 2 3 4 dmatelnd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ Y e. D ) /\ ( i e. N /\ j e. N /\ i =/= j ) ) -> ( i Y j ) = .0. )
42 40 32 33 34 41 syl13anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i Y j ) = .0. )
43 36 42 oveq12d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( ( i X j ) ( -g ` R ) ( i Y j ) ) = ( .0. ( -g ` R ) .0. ) )
44 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
45 eqid 
 |-  ( Base ` R ) = ( Base ` R )
46 45 3 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
47 44 46 jca 
 |-  ( R e. Ring -> ( R e. Grp /\ .0. e. ( Base ` R ) ) )
48 47 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R e. Grp /\ .0. e. ( Base ` R ) ) )
49 45 3 23 grpsubid 
 |-  ( ( R e. Grp /\ .0. e. ( Base ` R ) ) -> ( .0. ( -g ` R ) .0. ) = .0. )
50 48 49 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( .0. ( -g ` R ) .0. ) = .0. )
51 50 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( .0. ( -g ` R ) .0. ) = .0. )
52 26 43 51 3eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i ( X ( -g ` A ) Y ) j ) = .0. )
53 52 ex 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) -> ( i =/= j -> ( i ( X ( -g ` A ) Y ) j ) = .0. ) )
54 53 ralrimivva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i ( X ( -g ` A ) Y ) j ) = .0. ) )
55 1 2 3 4 dmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( X ( -g ` A ) Y ) e. D <-> ( ( X ( -g ` A ) Y ) e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i ( X ( -g ` A ) Y ) j ) = .0. ) ) ) )
56 55 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( ( X ( -g ` A ) Y ) e. D <-> ( ( X ( -g ` A ) Y ) e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i ( X ( -g ` A ) Y ) j ) = .0. ) ) ) )
57 15 54 56 mpbir2and 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( -g ` A ) Y ) e. D )