This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑊 ‘ 𝑋 ) 𝐽 ) = ( 𝑉 ‘ ( 𝐼 𝑋 𝐽 ) ) )