Step | Hyp | Ref
| Expression |
1 | | matplusgcell.a |
. . . . . . . . . 10
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | matplusgcell.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐴) |
3 | 1, 2 | matrcl 20037 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
4 | 3 | simpld 474 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin) |
5 | 4 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑁 ∈ Fin) |
6 | | simpl 472 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑅 ∈ Ring) |
7 | 1 | matgrp 20055 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Grp) |
8 | 5, 6, 7 | syl2anc 691 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝐴 ∈ Grp) |
9 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐴) = (0g‘𝐴) |
10 | 2, 9 | grpidcl 17273 |
. . . . . 6
⊢ (𝐴 ∈ Grp →
(0g‘𝐴)
∈ 𝐵) |
11 | 8, 10 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (0g‘𝐴) ∈ 𝐵) |
12 | | simpr 476 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
13 | 11, 12 | jca 553 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ((0g‘𝐴) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
14 | 13 | 3adant3 1074 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → ((0g‘𝐴) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
15 | | eqid 2610 |
. . . 4
⊢
(-g‘𝐴) = (-g‘𝐴) |
16 | | eqid 2610 |
. . . 4
⊢
(-g‘𝑅) = (-g‘𝑅) |
17 | 1, 2, 15, 16 | matsubgcell 20059 |
. . 3
⊢ ((𝑅 ∈ Ring ∧
((0g‘𝐴)
∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼((0g‘𝐴)(-g‘𝐴)𝑋)𝐽) = ((𝐼(0g‘𝐴)𝐽)(-g‘𝑅)(𝐼𝑋𝐽))) |
18 | 14, 17 | syld3an2 1365 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼((0g‘𝐴)(-g‘𝐴)𝑋)𝐽) = ((𝐼(0g‘𝐴)𝐽)(-g‘𝑅)(𝐼𝑋𝐽))) |
19 | | matinvgcell.w |
. . . . . 6
⊢ 𝑊 = (invg‘𝐴) |
20 | 2, 15, 19, 9 | grpinvval2 17321 |
. . . . 5
⊢ ((𝐴 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑊‘𝑋) = ((0g‘𝐴)(-g‘𝐴)𝑋)) |
21 | 8, 12, 20 | syl2anc 691 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑊‘𝑋) = ((0g‘𝐴)(-g‘𝐴)𝑋)) |
22 | 21 | 3adant3 1074 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝑊‘𝑋) = ((0g‘𝐴)(-g‘𝐴)𝑋)) |
23 | 22 | oveqd 6566 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑊‘𝑋)𝐽) = (𝐼((0g‘𝐴)(-g‘𝐴)𝑋)𝐽)) |
24 | | ringgrp 18375 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
25 | 24 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝑅 ∈ Grp) |
26 | | simp3 1056 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) |
27 | 2 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ (Base‘𝐴)) |
28 | 27 | biimpi 205 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (Base‘𝐴)) |
29 | 28 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝑋 ∈ (Base‘𝐴)) |
30 | | df-3an 1033 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑋 ∈ (Base‘𝐴)) ↔ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) ∧ 𝑋 ∈ (Base‘𝐴))) |
31 | 26, 29, 30 | sylanbrc 695 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑋 ∈ (Base‘𝐴))) |
32 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
33 | 1, 32 | matecl 20050 |
. . . . 5
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ∧ 𝑋 ∈ (Base‘𝐴)) → (𝐼𝑋𝐽) ∈ (Base‘𝑅)) |
34 | 31, 33 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼𝑋𝐽) ∈ (Base‘𝑅)) |
35 | | matinvgcell.v |
. . . . 5
⊢ 𝑉 = (invg‘𝑅) |
36 | | eqid 2610 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
37 | 32, 16, 35, 36 | grpinvval2 17321 |
. . . 4
⊢ ((𝑅 ∈ Grp ∧ (𝐼𝑋𝐽) ∈ (Base‘𝑅)) → (𝑉‘(𝐼𝑋𝐽)) = ((0g‘𝑅)(-g‘𝑅)(𝐼𝑋𝐽))) |
38 | 25, 34, 37 | syl2anc 691 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝑉‘(𝐼𝑋𝐽)) = ((0g‘𝑅)(-g‘𝑅)(𝐼𝑋𝐽))) |
39 | 4 | anim1i 590 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑅 ∈ Ring) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
40 | 39 | ancoms 468 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
41 | 1, 36 | mat0op 20044 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (0g‘𝑅))) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (0g‘𝐴) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (0g‘𝑅))) |
43 | 42 | 3adant3 1074 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (0g‘𝐴) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (0g‘𝑅))) |
44 | | eqidd 2611 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) ∧ (𝑥 = 𝐼 ∧ 𝑦 = 𝐽)) → (0g‘𝑅) = (0g‘𝑅)) |
45 | 26 | simpld 474 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝐼 ∈ 𝑁) |
46 | | simp3r 1083 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝐽 ∈ 𝑁) |
47 | | fvex 6113 |
. . . . . . 7
⊢
(0g‘𝑅) ∈ V |
48 | 47 | a1i 11 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (0g‘𝑅) ∈ V) |
49 | 43, 44, 45, 46, 48 | ovmpt2d 6686 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(0g‘𝐴)𝐽) = (0g‘𝑅)) |
50 | 49 | eqcomd 2616 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (0g‘𝑅) = (𝐼(0g‘𝐴)𝐽)) |
51 | 50 | oveq1d 6564 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → ((0g‘𝑅)(-g‘𝑅)(𝐼𝑋𝐽)) = ((𝐼(0g‘𝐴)𝐽)(-g‘𝑅)(𝐼𝑋𝐽))) |
52 | 38, 51 | eqtrd 2644 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝑉‘(𝐼𝑋𝐽)) = ((𝐼(0g‘𝐴)𝐽)(-g‘𝑅)(𝐼𝑋𝐽))) |
53 | 18, 23, 52 | 3eqtr4d 2654 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑊‘𝑋)𝐽) = (𝑉‘(𝐼𝑋𝐽))) |