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