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 𝐴 = ( 𝑁 Mat 𝑅 )
dmatid.b 𝐵 = ( Base ‘ 𝐴 )
dmatid.0 0 = ( 0g𝑅 )
dmatid.d 𝐷 = ( 𝑁 DMat 𝑅 )
Assertion dmatsubcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → ( 𝑋 ( -g𝐴 ) 𝑌 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 dmatid.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 dmatid.b 𝐵 = ( Base ‘ 𝐴 )
3 dmatid.0 0 = ( 0g𝑅 )
4 dmatid.d 𝐷 = ( 𝑁 DMat 𝑅 )
5 1 matgrp ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp )
6 5 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → 𝐴 ∈ Grp )
7 1 2 3 4 dmatmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑋𝐷𝑋𝐵 ) )
8 7 imp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑋𝐷 ) → 𝑋𝐵 )
9 8 adantrr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → 𝑋𝐵 )
10 1 2 3 4 dmatmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑌𝐷𝑌𝐵 ) )
11 10 imp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌𝐷 ) → 𝑌𝐵 )
12 11 adantrl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → 𝑌𝐵 )
13 eqid ( -g𝐴 ) = ( -g𝐴 )
14 2 13 grpsubcl ( ( 𝐴 ∈ Grp ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 ( -g𝐴 ) 𝑌 ) ∈ 𝐵 )
15 6 9 12 14 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → ( 𝑋 ( -g𝐴 ) 𝑌 ) ∈ 𝐵 )
16 simpr ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
17 16 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → 𝑅 ∈ Ring )
18 17 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → 𝑅 ∈ Ring )
19 7 10 anim12d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑋𝐷𝑌𝐷 ) → ( 𝑋𝐵𝑌𝐵 ) ) )
20 19 imp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → ( 𝑋𝐵𝑌𝐵 ) )
21 20 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑋𝐵𝑌𝐵 ) )
22 simpr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖𝑁𝑗𝑁 ) )
23 eqid ( -g𝑅 ) = ( -g𝑅 )
24 1 2 13 23 matsubgcell ( ( 𝑅 ∈ Ring ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑋 ( -g𝐴 ) 𝑌 ) 𝑗 ) = ( ( 𝑖 𝑋 𝑗 ) ( -g𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
25 18 21 22 24 syl3anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑋 ( -g𝐴 ) 𝑌 ) 𝑗 ) = ( ( 𝑖 𝑋 𝑗 ) ( -g𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
26 25 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → ( 𝑖 ( 𝑋 ( -g𝐴 ) 𝑌 ) 𝑗 ) = ( ( 𝑖 𝑋 𝑗 ) ( -g𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
27 simpll ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → 𝑁 ∈ Fin )
28 simprl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → 𝑋𝐷 )
29 27 17 28 3jca ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋𝐷 ) )
30 29 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋𝐷 ) )
31 30 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋𝐷 ) )
32 simplrl ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → 𝑖𝑁 )
33 simplrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → 𝑗𝑁 )
34 simpr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → 𝑖𝑗 )
35 1 2 3 4 dmatelnd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑋𝐷 ) ∧ ( 𝑖𝑁𝑗𝑁𝑖𝑗 ) ) → ( 𝑖 𝑋 𝑗 ) = 0 )
36 31 32 33 34 35 syl13anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → ( 𝑖 𝑋 𝑗 ) = 0 )
37 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → 𝑌𝐷 )
38 27 17 37 3jca ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌𝐷 ) )
39 38 adantr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌𝐷 ) )
40 39 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌𝐷 ) )
41 1 2 3 4 dmatelnd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌𝐷 ) ∧ ( 𝑖𝑁𝑗𝑁𝑖𝑗 ) ) → ( 𝑖 𝑌 𝑗 ) = 0 )
42 40 32 33 34 41 syl13anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → ( 𝑖 𝑌 𝑗 ) = 0 )
43 36 42 oveq12d ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → ( ( 𝑖 𝑋 𝑗 ) ( -g𝑅 ) ( 𝑖 𝑌 𝑗 ) ) = ( 0 ( -g𝑅 ) 0 ) )
44 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
45 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
46 45 3 ring0cl ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
47 44 46 jca ( 𝑅 ∈ Ring → ( 𝑅 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝑅 ) ) )
48 47 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑅 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝑅 ) ) )
49 45 3 23 grpsubid ( ( 𝑅 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( -g𝑅 ) 0 ) = 0 )
50 48 49 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0 ( -g𝑅 ) 0 ) = 0 )
51 50 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → ( 0 ( -g𝑅 ) 0 ) = 0 )
52 26 43 51 3eqtrd ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) ∧ 𝑖𝑗 ) → ( 𝑖 ( 𝑋 ( -g𝐴 ) 𝑌 ) 𝑗 ) = 0 )
53 52 ex ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖𝑗 → ( 𝑖 ( 𝑋 ( -g𝐴 ) 𝑌 ) 𝑗 ) = 0 ) )
54 53 ralrimivva ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 ( 𝑋 ( -g𝐴 ) 𝑌 ) 𝑗 ) = 0 ) )
55 1 2 3 4 dmatel ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑋 ( -g𝐴 ) 𝑌 ) ∈ 𝐷 ↔ ( ( 𝑋 ( -g𝐴 ) 𝑌 ) ∈ 𝐵 ∧ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 ( 𝑋 ( -g𝐴 ) 𝑌 ) 𝑗 ) = 0 ) ) ) )
56 55 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → ( ( 𝑋 ( -g𝐴 ) 𝑌 ) ∈ 𝐷 ↔ ( ( 𝑋 ( -g𝐴 ) 𝑌 ) ∈ 𝐵 ∧ ∀ 𝑖𝑁𝑗𝑁 ( 𝑖𝑗 → ( 𝑖 ( 𝑋 ( -g𝐴 ) 𝑌 ) 𝑗 ) = 0 ) ) ) )
57 15 54 56 mpbir2and ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋𝐷𝑌𝐷 ) ) → ( 𝑋 ( -g𝐴 ) 𝑌 ) ∈ 𝐷 )