Metamath Proof Explorer

Theorem matinvgcell

Description: Additive inversion in the matrix ring is cell-wise. (Contributed by AV, 17-Nov-2019)

Ref Expression
Hypotheses matplusgcell.a 
|- A = ( N Mat R )
matplusgcell.b 
|- B = ( Base ` A )
matinvgcell.v 
|- V = ( invg ` R )
matinvgcell.w 
|- W = ( invg ` A )
Assertion matinvgcell 
|- ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( I ( W ` X ) J ) = ( V ` ( I X J ) ) )

Proof

Step Hyp Ref Expression
1 matplusgcell.a 
 |-  A = ( N Mat R )
2 matplusgcell.b 
 |-  B = ( Base ` A )
3 matinvgcell.v 
 |-  V = ( invg ` R )
4 matinvgcell.w 
 |-  W = ( invg ` A )
5 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
6 5 simpld 
 |-  ( X e. B -> N e. Fin )
7 simpl 
 |-  ( ( R e. Ring /\ X e. B ) -> R e. Ring )
8 1 matgrp 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Grp )
9 6 7 8 syl2an2 
 |-  ( ( R e. Ring /\ X e. B ) -> A e. Grp )
10 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
11 2 10 grpidcl 
 |-  ( A e. Grp -> ( 0g ` A ) e. B )
12 9 11 syl 
 |-  ( ( R e. Ring /\ X e. B ) -> ( 0g ` A ) e. B )
13 simpr 
 |-  ( ( R e. Ring /\ X e. B ) -> X e. B )
14 12 13 jca 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( 0g ` A ) e. B /\ X e. B ) )
15 14 3adant3 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( ( 0g ` A ) e. B /\ X e. B ) )
16 eqid 
 |-  ( -g ` A ) = ( -g ` A )
17 eqid 
 |-  ( -g ` R ) = ( -g ` R )
18 1 2 16 17 matsubgcell 
 |-  ( ( R e. Ring /\ ( ( 0g ` A ) e. B /\ X e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( ( 0g ` A ) ( -g ` A ) X ) J ) = ( ( I ( 0g ` A ) J ) ( -g ` R ) ( I X J ) ) )
19 15 18 syld3an2 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( I ( ( 0g ` A ) ( -g ` A ) X ) J ) = ( ( I ( 0g ` A ) J ) ( -g ` R ) ( I X J ) ) )
20 2 16 4 10 grpinvval2 
 |-  ( ( A e. Grp /\ X e. B ) -> ( W ` X ) = ( ( 0g ` A ) ( -g ` A ) X ) )
21 9 13 20 syl2anc 
 |-  ( ( R e. Ring /\ X e. B ) -> ( W ` X ) = ( ( 0g ` A ) ( -g ` A ) X ) )
22 21 3adant3 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( W ` X ) = ( ( 0g ` A ) ( -g ` A ) X ) )
23 22 oveqd 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( I ( W ` X ) J ) = ( I ( ( 0g ` A ) ( -g ` A ) X ) J ) )
24 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
25 24 3ad2ant1 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> R e. Grp )
26 simp3 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( I e. N /\ J e. N ) )
27 2 eleq2i 
 |-  ( X e. B <-> X e. ( Base ` A ) )
28 27 biimpi 
 |-  ( X e. B -> X e. ( Base ` A ) )
29 28 3ad2ant2 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> X e. ( Base ` A ) )
30 df-3an 
 |-  ( ( I e. N /\ J e. N /\ X e. ( Base ` A ) ) <-> ( ( I e. N /\ J e. N ) /\ X e. ( Base ` A ) ) )
31 26 29 30 sylanbrc 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( I e. N /\ J e. N /\ X e. ( Base ` A ) ) )
32 eqid 
 |-  ( Base ` R ) = ( Base ` R )
33 1 32 matecl 
 |-  ( ( I e. N /\ J e. N /\ X e. ( Base ` A ) ) -> ( I X J ) e. ( Base ` R ) )
34 31 33 syl 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( I X J ) e. ( Base ` R ) )
35 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
36 32 17 3 35 grpinvval2 
 |-  ( ( R e. Grp /\ ( I X J ) e. ( Base ` R ) ) -> ( V ` ( I X J ) ) = ( ( 0g ` R ) ( -g ` R ) ( I X J ) ) )
37 25 34 36 syl2anc 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( V ` ( I X J ) ) = ( ( 0g ` R ) ( -g ` R ) ( I X J ) ) )
38 6 anim1i 
 |-  ( ( X e. B /\ R e. Ring ) -> ( N e. Fin /\ R e. Ring ) )
39 38 ancoms 
 |-  ( ( R e. Ring /\ X e. B ) -> ( N e. Fin /\ R e. Ring ) )
40 1 35 mat0op 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( x e. N , y e. N |-> ( 0g ` R ) ) )
41 39 40 syl 
 |-  ( ( R e. Ring /\ X e. B ) -> ( 0g ` A ) = ( x e. N , y e. N |-> ( 0g ` R ) ) )
42 41 3adant3 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( 0g ` A ) = ( x e. N , y e. N |-> ( 0g ` R ) ) )
43 eqidd 
 |-  ( ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) /\ ( x = I /\ y = J ) ) -> ( 0g ` R ) = ( 0g ` R ) )
44 26 simpld 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> I e. N )
45 simp3r 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> J e. N )
46 fvexd 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( 0g ` R ) e. _V )
47 42 43 44 45 46 ovmpod 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( I ( 0g ` A ) J ) = ( 0g ` R ) )
48 47 eqcomd 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( 0g ` R ) = ( I ( 0g ` A ) J ) )
49 48 oveq1d 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( ( 0g ` R ) ( -g ` R ) ( I X J ) ) = ( ( I ( 0g ` A ) J ) ( -g ` R ) ( I X J ) ) )
50 37 49 eqtrd 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( V ` ( I X J ) ) = ( ( I ( 0g ` A ) J ) ( -g ` R ) ( I X J ) ) )
51 19 23 50 3eqtr4d 
 |-  ( ( R e. Ring /\ X e. B /\ ( I e. N /\ J e. N ) ) -> ( I ( W ` X ) J ) = ( V ` ( I X J ) ) )