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 ‘ 𝐴 ) 𝑌 ) ∈ 𝐷 )