Step | Hyp | Ref
| Expression |
1 | | scmatrhmval.k |
. 2
⊢ 𝐾 = (Base‘𝑅) |
2 | | eqid 2738 |
. 2
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2738 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | eqid 2738 |
. 2
⊢
(+g‘𝑆) = (+g‘𝑆) |
5 | | ringgrp 19421 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
6 | 5 | adantl 485 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Grp) |
7 | | scmatrhmval.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
8 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐴) =
(Base‘𝐴) |
9 | | eqid 2738 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
10 | | scmatrhmval.c |
. . . 4
⊢ 𝐶 = (𝑁 ScMat 𝑅) |
11 | 7, 8, 1, 9, 10 | scmatsgrp 21270 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ (SubGrp‘𝐴)) |
12 | | scmatghm.s |
. . . 4
⊢ 𝑆 = (𝐴 ↾s 𝐶) |
13 | 12 | subggrp 18400 |
. . 3
⊢ (𝐶 ∈ (SubGrp‘𝐴) → 𝑆 ∈ Grp) |
14 | 11, 13 | syl 17 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ Grp) |
15 | | scmatrhmval.o |
. . . 4
⊢ 1 =
(1r‘𝐴) |
16 | | scmatrhmval.t |
. . . 4
⊢ ∗ = (
·𝑠 ‘𝐴) |
17 | | scmatrhmval.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 )) |
18 | 1, 7, 15, 16, 17, 10 | scmatf 21280 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶𝐶) |
19 | 7, 10, 12 | scmatstrbas 21277 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑆) = 𝐶) |
20 | 19 | feq3d 6491 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹:𝐾⟶(Base‘𝑆) ↔ 𝐹:𝐾⟶𝐶)) |
21 | 18, 20 | mpbird 260 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶(Base‘𝑆)) |
22 | 7 | matsca2 21171 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝐴)) |
23 | 10 | ovexi 7204 |
. . . . . . . . . 10
⊢ 𝐶 ∈ V |
24 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
25 | 12, 24 | resssca 16753 |
. . . . . . . . . 10
⊢ (𝐶 ∈ V →
(Scalar‘𝐴) =
(Scalar‘𝑆)) |
26 | 23, 25 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Scalar‘𝐴) =
(Scalar‘𝑆)) |
27 | 22, 26 | eqtrd 2773 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑆)) |
28 | 27 | fveq2d 6678 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(+g‘𝑅) =
(+g‘(Scalar‘𝑆))) |
29 | 28 | oveqd 7187 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦(+g‘𝑅)𝑧) = (𝑦(+g‘(Scalar‘𝑆))𝑧)) |
30 | 29 | oveq1d 7185 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑦(+g‘𝑅)𝑧) ∗ 1 ) = ((𝑦(+g‘(Scalar‘𝑆))𝑧) ∗ 1 )) |
31 | 30 | adantr 484 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦(+g‘𝑅)𝑧) ∗ 1 ) = ((𝑦(+g‘(Scalar‘𝑆))𝑧) ∗ 1 )) |
32 | 7 | matlmod 21180 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
33 | 7, 10 | scmatlss 21276 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ (LSubSp‘𝐴)) |
34 | | eqid 2738 |
. . . . . . . 8
⊢
(LSubSp‘𝐴) =
(LSubSp‘𝐴) |
35 | 12, 34 | lsslmod 19851 |
. . . . . . 7
⊢ ((𝐴 ∈ LMod ∧ 𝐶 ∈ (LSubSp‘𝐴)) → 𝑆 ∈ LMod) |
36 | 32, 33, 35 | syl2anc 587 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ LMod) |
37 | 36 | adantr 484 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑆 ∈ LMod) |
38 | 27 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑆))) |
39 | 1, 38 | syl5eq 2785 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐾 =
(Base‘(Scalar‘𝑆))) |
40 | 39 | eleq2d 2818 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ (Base‘(Scalar‘𝑆)))) |
41 | 40 | biimpd 232 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝐾 → 𝑦 ∈ (Base‘(Scalar‘𝑆)))) |
42 | 41 | adantrd 495 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → 𝑦 ∈ (Base‘(Scalar‘𝑆)))) |
43 | 42 | imp 410 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑦 ∈ (Base‘(Scalar‘𝑆))) |
44 | 39 | eleq2d 2818 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ (Base‘(Scalar‘𝑆)))) |
45 | 44 | biimpd 232 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑧 ∈ 𝐾 → 𝑧 ∈ (Base‘(Scalar‘𝑆)))) |
46 | 45 | adantld 494 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → 𝑧 ∈ (Base‘(Scalar‘𝑆)))) |
47 | 46 | imp 410 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑧 ∈ (Base‘(Scalar‘𝑆))) |
48 | 7, 8, 1, 9, 10 | scmatid 21265 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴)
∈ 𝐶) |
49 | 15 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 =
(1r‘𝐴)) |
50 | 48, 49, 19 | 3eltr4d 2848 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 ∈
(Base‘𝑆)) |
51 | 50 | adantr 484 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 1 ∈ (Base‘𝑆)) |
52 | | eqid 2738 |
. . . . . 6
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
53 | 12, 16 | ressvsca 16754 |
. . . . . . 7
⊢ (𝐶 ∈ V → ∗ = (
·𝑠 ‘𝑆)) |
54 | 23, 53 | ax-mp 5 |
. . . . . 6
⊢ ∗ = (
·𝑠 ‘𝑆) |
55 | | eqid 2738 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
56 | | eqid 2738 |
. . . . . 6
⊢
(+g‘(Scalar‘𝑆)) =
(+g‘(Scalar‘𝑆)) |
57 | 2, 4, 52, 54, 55, 56 | lmodvsdir 19777 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ (𝑦 ∈
(Base‘(Scalar‘𝑆)) ∧ 𝑧 ∈ (Base‘(Scalar‘𝑆)) ∧ 1 ∈ (Base‘𝑆))) → ((𝑦(+g‘(Scalar‘𝑆))𝑧) ∗ 1 ) = ((𝑦 ∗ 1
)(+g‘𝑆)(𝑧 ∗ 1 ))) |
58 | 37, 43, 47, 51, 57 | syl13anc 1373 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦(+g‘(Scalar‘𝑆))𝑧) ∗ 1 ) = ((𝑦 ∗ 1
)(+g‘𝑆)(𝑧 ∗ 1 ))) |
59 | 31, 58 | eqtrd 2773 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦(+g‘𝑅)𝑧) ∗ 1 ) = ((𝑦 ∗ 1
)(+g‘𝑆)(𝑧 ∗ 1 ))) |
60 | | simpr 488 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) |
61 | 60 | adantr 484 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑅 ∈ Ring) |
62 | 60 | anim1i 618 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑅 ∈ Ring ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾))) |
63 | | 3anass 1096 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ↔ (𝑅 ∈ Ring ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾))) |
64 | 62, 63 | sylibr 237 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) |
65 | 1, 3 | ringacl 19450 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → (𝑦(+g‘𝑅)𝑧) ∈ 𝐾) |
66 | 64, 65 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑦(+g‘𝑅)𝑧) ∈ 𝐾) |
67 | 1, 7, 15, 16, 17 | scmatrhmval 21278 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑦(+g‘𝑅)𝑧) ∈ 𝐾) → (𝐹‘(𝑦(+g‘𝑅)𝑧)) = ((𝑦(+g‘𝑅)𝑧) ∗ 1 )) |
68 | 61, 66, 67 | syl2anc 587 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘(𝑦(+g‘𝑅)𝑧)) = ((𝑦(+g‘𝑅)𝑧) ∗ 1 )) |
69 | 1, 7, 15, 16, 17 | scmatrhmval 21278 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (𝑦 ∗ 1 )) |
70 | 69 | ad2ant2lr 748 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘𝑦) = (𝑦 ∗ 1 )) |
71 | 1, 7, 15, 16, 17 | scmatrhmval 21278 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾) → (𝐹‘𝑧) = (𝑧 ∗ 1 )) |
72 | 71 | ad2ant2l 746 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘𝑧) = (𝑧 ∗ 1 )) |
73 | 70, 72 | oveq12d 7188 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝐹‘𝑦)(+g‘𝑆)(𝐹‘𝑧)) = ((𝑦 ∗ 1
)(+g‘𝑆)(𝑧 ∗ 1 ))) |
74 | 59, 68, 73 | 3eqtr4d 2783 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘(𝑦(+g‘𝑅)𝑧)) = ((𝐹‘𝑦)(+g‘𝑆)(𝐹‘𝑧))) |
75 | 1, 2, 3, 4, 6, 14,
21, 74 | isghmd 18485 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |