Proof of Theorem matsubgcell
Step | Hyp | Ref
| Expression |
1 | | matplusgcell.a |
. . . . . . . . . . 11
⊢ 𝐴 = (𝑁 Mat 𝑅) |
2 | | matplusgcell.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐴) |
3 | 1, 2 | matrcl 21020 |
. . . . . . . . . 10
⊢ (𝑋 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
4 | 3 | simpld 497 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 → 𝑁 ∈ Fin) |
5 | 4 | adantr 483 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑁 ∈ Fin) |
6 | 5 | 3ad2ant2 1130 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝑁 ∈ Fin) |
7 | | simp1 1132 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝑅 ∈ Ring) |
8 | | eqid 2821 |
. . . . . . . 8
⊢ (𝑅 freeLMod (𝑁 × 𝑁)) = (𝑅 freeLMod (𝑁 × 𝑁)) |
9 | 1, 8 | matsubg 21040 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(-g‘(𝑅
freeLMod (𝑁 × 𝑁))) = (-g‘𝐴)) |
10 | 6, 7, 9 | syl2anc 586 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (-g‘(𝑅 freeLMod (𝑁 × 𝑁))) = (-g‘𝐴)) |
11 | | matsubgcell.s |
. . . . . 6
⊢ 𝑆 = (-g‘𝐴) |
12 | 10, 11 | syl6reqr 2875 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝑆 = (-g‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
13 | 12 | oveqd 7172 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝑋𝑆𝑌) = (𝑋(-g‘(𝑅 freeLMod (𝑁 × 𝑁)))𝑌)) |
14 | | eqid 2821 |
. . . . 5
⊢
(Base‘(𝑅
freeLMod (𝑁 × 𝑁))) = (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) |
15 | | xpfi 8788 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝑁 × 𝑁) ∈ Fin) |
16 | 15 | anidms 569 |
. . . . . . . . 9
⊢ (𝑁 ∈ Fin → (𝑁 × 𝑁) ∈ Fin) |
17 | 16 | adantr 483 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ V) → (𝑁 × 𝑁) ∈ Fin) |
18 | 3, 17 | syl 17 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → (𝑁 × 𝑁) ∈ Fin) |
19 | 18 | adantr 483 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁 × 𝑁) ∈ Fin) |
20 | 19 | 3ad2ant2 1130 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝑁 × 𝑁) ∈ Fin) |
21 | 2 | eleq2i 2904 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐵 ↔ 𝑋 ∈ (Base‘𝐴)) |
22 | 21 | biimpi 218 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (Base‘𝐴)) |
23 | 1, 8 | matbas 21021 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ V) →
(Base‘(𝑅 freeLMod
(𝑁 × 𝑁))) = (Base‘𝐴)) |
24 | 3, 23 | syl 17 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) = (Base‘𝐴)) |
25 | 22, 24 | eleqtrrd 2916 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
26 | 25 | adantr 483 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
27 | 26 | 3ad2ant2 1130 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝑋 ∈ (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
28 | 2 | eleq2i 2904 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝐵 ↔ 𝑌 ∈ (Base‘𝐴)) |
29 | 28 | biimpi 218 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ (Base‘𝐴)) |
30 | 1, 2 | matrcl 21020 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝐵 → (𝑁 ∈ Fin ∧ 𝑅 ∈ V)) |
31 | 30, 23 | syl 17 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝐵 → (Base‘(𝑅 freeLMod (𝑁 × 𝑁))) = (Base‘𝐴)) |
32 | 29, 31 | eleqtrrd 2916 |
. . . . . . 7
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
33 | 32 | adantl 484 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
34 | 33 | 3ad2ant2 1130 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → 𝑌 ∈ (Base‘(𝑅 freeLMod (𝑁 × 𝑁)))) |
35 | | matsubgcell.m |
. . . . 5
⊢ − =
(-g‘𝑅) |
36 | | eqid 2821 |
. . . . 5
⊢
(-g‘(𝑅 freeLMod (𝑁 × 𝑁))) = (-g‘(𝑅 freeLMod (𝑁 × 𝑁))) |
37 | 8, 14, 7, 20, 27, 34, 35, 36 | frlmsubgval 20908 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝑋(-g‘(𝑅 freeLMod (𝑁 × 𝑁)))𝑌) = (𝑋 ∘f − 𝑌)) |
38 | 13, 37 | eqtrd 2856 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝑋𝑆𝑌) = (𝑋 ∘f − 𝑌)) |
39 | 38 | oveqd 7172 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋𝑆𝑌)𝐽) = (𝐼(𝑋 ∘f − 𝑌)𝐽)) |
40 | | df-ov 7158 |
. . 3
⊢ (𝐼(𝑋 ∘f − 𝑌)𝐽) = ((𝑋 ∘f − 𝑌)‘〈𝐼, 𝐽〉) |
41 | | opelxpi 5591 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → 〈𝐼, 𝐽〉 ∈ (𝑁 × 𝑁)) |
42 | 41 | anim2i 618 |
. . . . 5
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 〈𝐼, 𝐽〉 ∈ (𝑁 × 𝑁))) |
43 | 42 | 3adant1 1126 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 〈𝐼, 𝐽〉 ∈ (𝑁 × 𝑁))) |
44 | | eqid 2821 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
45 | 1, 44, 2 | matbas2i 21030 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
46 | | elmapfn 8428 |
. . . . . . 7
⊢ (𝑋 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑋 Fn (𝑁 × 𝑁)) |
47 | 45, 46 | syl 17 |
. . . . . 6
⊢ (𝑋 ∈ 𝐵 → 𝑋 Fn (𝑁 × 𝑁)) |
48 | 47 | adantr 483 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 Fn (𝑁 × 𝑁)) |
49 | 1, 44, 2 | matbas2i 21030 |
. . . . . . 7
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁))) |
50 | | elmapfn 8428 |
. . . . . . 7
⊢ (𝑌 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) → 𝑌 Fn (𝑁 × 𝑁)) |
51 | 49, 50 | syl 17 |
. . . . . 6
⊢ (𝑌 ∈ 𝐵 → 𝑌 Fn (𝑁 × 𝑁)) |
52 | 51 | adantl 484 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 Fn (𝑁 × 𝑁)) |
53 | | inidm 4194 |
. . . . 5
⊢ ((𝑁 × 𝑁) ∩ (𝑁 × 𝑁)) = (𝑁 × 𝑁) |
54 | | df-ov 7158 |
. . . . . . 7
⊢ (𝐼𝑋𝐽) = (𝑋‘〈𝐼, 𝐽〉) |
55 | 54 | eqcomi 2830 |
. . . . . 6
⊢ (𝑋‘〈𝐼, 𝐽〉) = (𝐼𝑋𝐽) |
56 | 55 | a1i 11 |
. . . . 5
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 〈𝐼, 𝐽〉 ∈ (𝑁 × 𝑁)) → (𝑋‘〈𝐼, 𝐽〉) = (𝐼𝑋𝐽)) |
57 | | df-ov 7158 |
. . . . . . 7
⊢ (𝐼𝑌𝐽) = (𝑌‘〈𝐼, 𝐽〉) |
58 | 57 | eqcomi 2830 |
. . . . . 6
⊢ (𝑌‘〈𝐼, 𝐽〉) = (𝐼𝑌𝐽) |
59 | 58 | a1i 11 |
. . . . 5
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 〈𝐼, 𝐽〉 ∈ (𝑁 × 𝑁)) → (𝑌‘〈𝐼, 𝐽〉) = (𝐼𝑌𝐽)) |
60 | 48, 52, 19, 19, 53, 56, 59 | ofval 7417 |
. . . 4
⊢ (((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 〈𝐼, 𝐽〉 ∈ (𝑁 × 𝑁)) → ((𝑋 ∘f − 𝑌)‘〈𝐼, 𝐽〉) = ((𝐼𝑋𝐽) − (𝐼𝑌𝐽))) |
61 | 43, 60 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → ((𝑋 ∘f − 𝑌)‘〈𝐼, 𝐽〉) = ((𝐼𝑋𝐽) − (𝐼𝑌𝐽))) |
62 | 40, 61 | syl5eq 2868 |
. 2
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋 ∘f − 𝑌)𝐽) = ((𝐼𝑋𝐽) − (𝐼𝑌𝐽))) |
63 | 39, 62 | eqtrd 2856 |
1
⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼(𝑋𝑆𝑌)𝐽) = ((𝐼𝑋𝐽) − (𝐼𝑌𝐽))) |