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 = ( -g ` A )
matsubgcell.m 
|- .- = ( -g ` R )
Assertion matsubgcell 
|- ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. 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 = ( -g ` A )
4 matsubgcell.m 
 |-  .- = ( -g ` R )
5 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
6 5 simpld 
 |-  ( X e. B -> N e. Fin )
7 6 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> N e. Fin )
8 7 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> N e. Fin )
9 simp1 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> R e. Ring )
10 eqid 
 |-  ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
11 1 10 matsubg 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( -g ` ( R freeLMod ( N X. N ) ) ) = ( -g ` A ) )
12 8 9 11 syl2anc 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( -g ` ( R freeLMod ( N X. N ) ) ) = ( -g ` A ) )
13 3 12 eqtr4id 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> S = ( -g ` ( R freeLMod ( N X. N ) ) ) )
14 13 oveqd 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( X S Y ) = ( X ( -g ` ( R freeLMod ( N X. N ) ) ) Y ) )
15 eqid 
 |-  ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` ( R freeLMod ( N X. N ) ) )
16 xpfi 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
17 16 anidms 
 |-  ( N e. Fin -> ( N X. N ) e. Fin )
18 17 adantr 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( N X. N ) e. Fin )
19 5 18 syl 
 |-  ( X e. B -> ( N X. N ) e. Fin )
20 19 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> ( N X. N ) e. Fin )
21 20 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( N X. N ) e. Fin )
22 2 eleq2i 
 |-  ( X e. B <-> X e. ( Base ` A ) )
23 22 biimpi 
 |-  ( X e. B -> X e. ( Base ` A ) )
24 1 10 matbas 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
25 5 24 syl 
 |-  ( X e. B -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
26 23 25 eleqtrrd 
 |-  ( X e. B -> X e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
27 26 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> X e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
28 27 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> X e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
29 2 eleq2i 
 |-  ( Y e. B <-> Y e. ( Base ` A ) )
30 29 biimpi 
 |-  ( Y e. B -> Y e. ( Base ` A ) )
31 1 2 matrcl 
 |-  ( Y e. B -> ( N e. Fin /\ R e. _V ) )
32 31 24 syl 
 |-  ( Y e. B -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
33 30 32 eleqtrrd 
 |-  ( Y e. B -> Y e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
34 33 adantl 
 |-  ( ( X e. B /\ Y e. B ) -> Y e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
35 34 3ad2ant2 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> Y e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
36 eqid 
 |-  ( -g ` ( R freeLMod ( N X. N ) ) ) = ( -g ` ( R freeLMod ( N X. N ) ) )
37 10 15 9 21 28 35 4 36 frlmsubgval 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( X ( -g ` ( R freeLMod ( N X. N ) ) ) Y ) = ( X oF .- Y ) )
38 14 37 eqtrd 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( X S Y ) = ( X oF .- Y ) )
39 38 oveqd 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X S Y ) J ) = ( I ( X oF .- Y ) J ) )
40 df-ov 
 |-  ( I ( X oF .- Y ) J ) = ( ( X oF .- Y ) ` <. I , J >. )
41 opelxpi 
 |-  ( ( I e. N /\ J e. N ) -> <. I , J >. e. ( N X. N ) )
42 41 anim2i 
 |-  ( ( ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( ( X e. B /\ Y e. B ) /\ <. I , J >. e. ( N X. N ) ) )
43 42 3adant1 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( ( X e. B /\ Y e. B ) /\ <. I , J >. e. ( N X. N ) ) )
44 eqid 
 |-  ( Base ` R ) = ( Base ` R )
45 1 44 2 matbas2i 
 |-  ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
46 elmapfn 
 |-  ( X e. ( ( Base ` R ) ^m ( N X. N ) ) -> X Fn ( N X. N ) )
47 45 46 syl 
 |-  ( X e. B -> X Fn ( N X. N ) )
48 47 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> X Fn ( N X. N ) )
49 1 44 2 matbas2i 
 |-  ( Y e. B -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
50 elmapfn 
 |-  ( Y e. ( ( Base ` R ) ^m ( N X. N ) ) -> Y Fn ( N X. N ) )
51 49 50 syl 
 |-  ( Y e. B -> Y Fn ( N X. N ) )
52 51 adantl 
 |-  ( ( X e. B /\ Y e. B ) -> Y Fn ( N X. N ) )
53 inidm 
 |-  ( ( N X. N ) i^i ( N X. N ) ) = ( N X. N )
54 df-ov 
 |-  ( I X J ) = ( X ` <. I , J >. )
55 54 eqcomi 
 |-  ( X ` <. I , J >. ) = ( I X J )
56 55 a1i 
 |-  ( ( ( X e. B /\ Y e. B ) /\ <. I , J >. e. ( N X. 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 e. B /\ Y e. B ) /\ <. I , J >. e. ( N X. N ) ) -> ( Y ` <. I , J >. ) = ( I Y J ) )
60 48 52 20 20 53 56 59 ofval 
 |-  ( ( ( X e. B /\ Y e. B ) /\ <. I , J >. e. ( N X. N ) ) -> ( ( X oF .- Y ) ` <. I , J >. ) = ( ( I X J ) .- ( I Y J ) ) )
61 43 60 syl 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( ( X oF .- Y ) ` <. I , J >. ) = ( ( I X J ) .- ( I Y J ) ) )
62 40 61 eqtrid 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X oF .- Y ) J ) = ( ( I X J ) .- ( I Y J ) ) )
63 39 62 eqtrd 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X S Y ) J ) = ( ( I X J ) .- ( I Y J ) ) )