Metamath Proof Explorer


Theorem matsubgcell

Description: Subtraction in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses matplusgcell.a A = N Mat R
matplusgcell.b B = Base A
matsubgcell.s S = - A
matsubgcell.m - ˙ = - R
Assertion matsubgcell R Ring X B Y B I N J N I X S Y J = I X J - ˙ I Y J

Proof

Step Hyp Ref Expression
1 matplusgcell.a A = N Mat R
2 matplusgcell.b B = Base A
3 matsubgcell.s S = - A
4 matsubgcell.m - ˙ = - R
5 1 2 matrcl X B N Fin R V
6 5 simpld X B N Fin
7 6 adantr X B Y B N Fin
8 7 3ad2ant2 R Ring X B Y B I N J N N Fin
9 simp1 R Ring X B Y B I N J N R Ring
10 eqid R freeLMod N × N = R freeLMod N × N
11 1 10 matsubg N Fin R Ring - R freeLMod N × N = - A
12 8 9 11 syl2anc R Ring X B Y B I N J N - R freeLMod N × N = - A
13 12 3 syl6reqr R Ring X B Y B I N J N S = - R freeLMod N × N
14 13 oveqd R Ring X B Y B I N J N X S Y = X - R freeLMod N × N Y
15 eqid Base R freeLMod N × N = Base R freeLMod N × N
16 xpfi N Fin N Fin N × N Fin
17 16 anidms N Fin N × N Fin
18 17 adantr N Fin R V N × N Fin
19 5 18 syl X B N × N Fin
20 19 adantr X B Y B N × N Fin
21 20 3ad2ant2 R Ring X B Y B I N J N N × N Fin
22 2 eleq2i X B X Base A
23 22 biimpi X B X Base A
24 1 10 matbas N Fin R V Base R freeLMod N × N = Base A
25 5 24 syl X B Base R freeLMod N × N = Base A
26 23 25 eleqtrrd X B X Base R freeLMod N × N
27 26 adantr X B Y B X Base R freeLMod N × N
28 27 3ad2ant2 R Ring X B Y B I N J N X Base R freeLMod N × N
29 2 eleq2i Y B Y Base A
30 29 biimpi Y B Y Base A
31 1 2 matrcl Y B N Fin R V
32 31 24 syl Y B Base R freeLMod N × N = Base A
33 30 32 eleqtrrd Y B Y Base R freeLMod N × N
34 33 adantl X B Y B Y Base R freeLMod N × N
35 34 3ad2ant2 R Ring X B Y B I N J N Y Base R freeLMod N × N
36 eqid - R freeLMod N × N = - R freeLMod N × N
37 10 15 9 21 28 35 4 36 frlmsubgval R Ring X B Y B I N J N X - R freeLMod N × N Y = X - ˙ f Y
38 14 37 eqtrd R Ring X B Y B I N J N X S Y = X - ˙ f Y
39 38 oveqd R Ring X B Y B I N J N I X S Y J = I X - ˙ f Y J
40 df-ov I X - ˙ f Y J = X - ˙ f Y I J
41 opelxpi I N J N I J N × N
42 41 anim2i X B Y B I N J N X B Y B I J N × N
43 42 3adant1 R Ring X B Y B I N J N X B Y B I J N × N
44 eqid Base R = Base R
45 1 44 2 matbas2i X B X Base R N × N
46 elmapfn X Base R N × N X Fn N × N
47 45 46 syl X B X Fn N × N
48 47 adantr X B Y B X Fn N × N
49 1 44 2 matbas2i Y B Y Base R N × N
50 elmapfn Y Base R N × N Y Fn N × N
51 49 50 syl Y B Y Fn N × N
52 51 adantl X B Y B Y Fn N × N
53 inidm N × N N × N = N × N
54 df-ov I X J = X I J
55 54 eqcomi X I J = I X J
56 55 a1i X B Y B I J N × N X I J = I X J
57 df-ov I Y J = Y I J
58 57 eqcomi Y I J = I Y J
59 58 a1i X B Y B I J N × N Y I J = I Y J
60 48 52 20 20 53 56 59 ofval X B Y B I J N × N X - ˙ f Y I J = I X J - ˙ I Y J
61 43 60 syl R Ring X B Y B I N J N X - ˙ f Y I J = I X J - ˙ I Y J
62 40 61 syl5eq R Ring X B Y B I N J N I X - ˙ f Y J = I X J - ˙ I Y J
63 39 62 eqtrd R Ring X B Y B I N J N I X S Y J = I X J - ˙ I Y J