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 𝐴 = ( 𝑁 Mat 𝑅 )
matplusgcell.b 𝐵 = ( Base ‘ 𝐴 )
matinvgcell.v 𝑉 = ( invg𝑅 )
matinvgcell.w 𝑊 = ( invg𝐴 )
Assertion matinvgcell ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( 𝑊𝑋 ) 𝐽 ) = ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 matplusgcell.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 matplusgcell.b 𝐵 = ( Base ‘ 𝐴 )
3 matinvgcell.v 𝑉 = ( invg𝑅 )
4 matinvgcell.w 𝑊 = ( invg𝐴 )
5 1 2 matrcl ( 𝑋𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
6 5 simpld ( 𝑋𝐵𝑁 ∈ Fin )
7 simpl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → 𝑅 ∈ Ring )
8 1 matgrp ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp )
9 6 7 8 syl2an2 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → 𝐴 ∈ Grp )
10 eqid ( 0g𝐴 ) = ( 0g𝐴 )
11 2 10 grpidcl ( 𝐴 ∈ Grp → ( 0g𝐴 ) ∈ 𝐵 )
12 9 11 syl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( 0g𝐴 ) ∈ 𝐵 )
13 simpr ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → 𝑋𝐵 )
14 12 13 jca ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( ( 0g𝐴 ) ∈ 𝐵𝑋𝐵 ) )
15 14 3adant3 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( ( 0g𝐴 ) ∈ 𝐵𝑋𝐵 ) )
16 eqid ( -g𝐴 ) = ( -g𝐴 )
17 eqid ( -g𝑅 ) = ( -g𝑅 )
18 1 2 16 17 matsubgcell ( ( 𝑅 ∈ Ring ∧ ( ( 0g𝐴 ) ∈ 𝐵𝑋𝐵 ) ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( ( 0g𝐴 ) ( -g𝐴 ) 𝑋 ) 𝐽 ) = ( ( 𝐼 ( 0g𝐴 ) 𝐽 ) ( -g𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
19 15 18 syld3an2 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( ( 0g𝐴 ) ( -g𝐴 ) 𝑋 ) 𝐽 ) = ( ( 𝐼 ( 0g𝐴 ) 𝐽 ) ( -g𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
20 2 16 4 10 grpinvval2 ( ( 𝐴 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑊𝑋 ) = ( ( 0g𝐴 ) ( -g𝐴 ) 𝑋 ) )
21 9 13 20 syl2anc ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( 𝑊𝑋 ) = ( ( 0g𝐴 ) ( -g𝐴 ) 𝑋 ) )
22 21 3adant3 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑊𝑋 ) = ( ( 0g𝐴 ) ( -g𝐴 ) 𝑋 ) )
23 22 oveqd ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( 𝑊𝑋 ) 𝐽 ) = ( 𝐼 ( ( 0g𝐴 ) ( -g𝐴 ) 𝑋 ) 𝐽 ) )
24 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
25 24 3ad2ant1 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → 𝑅 ∈ Grp )
26 simp3 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼𝑁𝐽𝑁 ) )
27 2 eleq2i ( 𝑋𝐵𝑋 ∈ ( Base ‘ 𝐴 ) )
28 27 biimpi ( 𝑋𝐵𝑋 ∈ ( Base ‘ 𝐴 ) )
29 28 3ad2ant2 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → 𝑋 ∈ ( Base ‘ 𝐴 ) )
30 df-3an ( ( 𝐼𝑁𝐽𝑁𝑋 ∈ ( Base ‘ 𝐴 ) ) ↔ ( ( 𝐼𝑁𝐽𝑁 ) ∧ 𝑋 ∈ ( Base ‘ 𝐴 ) ) )
31 26 29 30 sylanbrc ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼𝑁𝐽𝑁𝑋 ∈ ( Base ‘ 𝐴 ) ) )
32 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
33 1 32 matecl ( ( 𝐼𝑁𝐽𝑁𝑋 ∈ ( Base ‘ 𝐴 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
34 31 33 syl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 𝑋 𝐽 ) ∈ ( Base ‘ 𝑅 ) )
35 eqid ( 0g𝑅 ) = ( 0g𝑅 )
36 32 17 3 35 grpinvval2 ( ( 𝑅 ∈ Grp ∧ ( 𝐼 𝑋 𝐽 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) = ( ( 0g𝑅 ) ( -g𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
37 25 34 36 syl2anc ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) = ( ( 0g𝑅 ) ( -g𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
38 6 anim1i ( ( 𝑋𝐵𝑅 ∈ Ring ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
39 38 ancoms ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
40 1 35 mat0op ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g𝐴 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 0g𝑅 ) ) )
41 39 40 syl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( 0g𝐴 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 0g𝑅 ) ) )
42 41 3adant3 ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 0g𝐴 ) = ( 𝑥𝑁 , 𝑦𝑁 ↦ ( 0g𝑅 ) ) )
43 eqidd ( ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) ∧ ( 𝑥 = 𝐼𝑦 = 𝐽 ) ) → ( 0g𝑅 ) = ( 0g𝑅 ) )
44 26 simpld ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → 𝐼𝑁 )
45 simp3r ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → 𝐽𝑁 )
46 fvexd ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 0g𝑅 ) ∈ V )
47 42 43 44 45 46 ovmpod ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( 0g𝐴 ) 𝐽 ) = ( 0g𝑅 ) )
48 47 eqcomd ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 0g𝑅 ) = ( 𝐼 ( 0g𝐴 ) 𝐽 ) )
49 48 oveq1d ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( ( 0g𝑅 ) ( -g𝑅 ) ( 𝐼 𝑋 𝐽 ) ) = ( ( 𝐼 ( 0g𝐴 ) 𝐽 ) ( -g𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
50 37 49 eqtrd ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) = ( ( 𝐼 ( 0g𝐴 ) 𝐽 ) ( -g𝑅 ) ( 𝐼 𝑋 𝐽 ) ) )
51 19 23 50 3eqtr4d ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ∧ ( 𝐼𝑁𝐽𝑁 ) ) → ( 𝐼 ( 𝑊𝑋 ) 𝐽 ) = ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) )