Step | Hyp | Ref
| Expression |
1 | | scmatrhmval.k |
. 2
⊢ 𝐾 = (Base‘𝑅) |
2 | | eqid 2778 |
. 2
⊢
(Base‘𝑆) =
(Base‘𝑆) |
3 | | eqid 2778 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | eqid 2778 |
. 2
⊢
(+g‘𝑆) = (+g‘𝑆) |
5 | | ringgrp 18939 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
6 | 5 | adantl 475 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Grp) |
7 | | scmatrhmval.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
8 | | eqid 2778 |
. . . 4
⊢
(Base‘𝐴) =
(Base‘𝐴) |
9 | | eqid 2778 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
10 | | scmatrhmval.c |
. . . 4
⊢ 𝐶 = (𝑁 ScMat 𝑅) |
11 | 7, 8, 1, 9, 10 | scmatsgrp 20730 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ (SubGrp‘𝐴)) |
12 | | scmatghm.s |
. . . 4
⊢ 𝑆 = (𝐴 ↾s 𝐶) |
13 | 12 | subggrp 17981 |
. . 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 20740 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶𝐶) |
19 | 7, 10, 12 | scmatstrbas 20737 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑆) = 𝐶) |
20 | 19 | feq3d 6278 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹:𝐾⟶(Base‘𝑆) ↔ 𝐹:𝐾⟶𝐶)) |
21 | 18, 20 | mpbird 249 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶(Base‘𝑆)) |
22 | 7 | matsca2 20630 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝐴)) |
23 | | ovex 6954 |
. . . . . . . . . . 11
⊢ (𝑁 ScMat 𝑅) ∈ V |
24 | 10, 23 | eqeltri 2855 |
. . . . . . . . . 10
⊢ 𝐶 ∈ V |
25 | | eqid 2778 |
. . . . . . . . . . 11
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
26 | 12, 25 | resssca 16423 |
. . . . . . . . . 10
⊢ (𝐶 ∈ V →
(Scalar‘𝐴) =
(Scalar‘𝑆)) |
27 | 24, 26 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Scalar‘𝐴) =
(Scalar‘𝑆)) |
28 | 22, 27 | eqtrd 2814 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑆)) |
29 | 28 | fveq2d 6450 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(+g‘𝑅) =
(+g‘(Scalar‘𝑆))) |
30 | 29 | oveqd 6939 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦(+g‘𝑅)𝑧) = (𝑦(+g‘(Scalar‘𝑆))𝑧)) |
31 | 30 | oveq1d 6937 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑦(+g‘𝑅)𝑧) ∗ 1 ) = ((𝑦(+g‘(Scalar‘𝑆))𝑧) ∗ 1 )) |
32 | 31 | adantr 474 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦(+g‘𝑅)𝑧) ∗ 1 ) = ((𝑦(+g‘(Scalar‘𝑆))𝑧) ∗ 1 )) |
33 | 7 | matlmod 20639 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
34 | 7, 10 | scmatlss 20736 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ (LSubSp‘𝐴)) |
35 | | eqid 2778 |
. . . . . . . 8
⊢
(LSubSp‘𝐴) =
(LSubSp‘𝐴) |
36 | 12, 35 | lsslmod 19355 |
. . . . . . 7
⊢ ((𝐴 ∈ LMod ∧ 𝐶 ∈ (LSubSp‘𝐴)) → 𝑆 ∈ LMod) |
37 | 33, 34, 36 | syl2anc 579 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑆 ∈ LMod) |
38 | 37 | adantr 474 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑆 ∈ LMod) |
39 | 28 | fveq2d 6450 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑆))) |
40 | 1, 39 | syl5eq 2826 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐾 =
(Base‘(Scalar‘𝑆))) |
41 | 40 | eleq2d 2845 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ (Base‘(Scalar‘𝑆)))) |
42 | 41 | biimpd 221 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝐾 → 𝑦 ∈ (Base‘(Scalar‘𝑆)))) |
43 | 42 | adantrd 487 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → 𝑦 ∈ (Base‘(Scalar‘𝑆)))) |
44 | 43 | imp 397 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑦 ∈ (Base‘(Scalar‘𝑆))) |
45 | 40 | eleq2d 2845 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ (Base‘(Scalar‘𝑆)))) |
46 | 45 | biimpd 221 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑧 ∈ 𝐾 → 𝑧 ∈ (Base‘(Scalar‘𝑆)))) |
47 | 46 | adantld 486 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → 𝑧 ∈ (Base‘(Scalar‘𝑆)))) |
48 | 47 | imp 397 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑧 ∈ (Base‘(Scalar‘𝑆))) |
49 | 7, 8, 1, 9, 10 | scmatid 20725 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝐴)
∈ 𝐶) |
50 | 15 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 =
(1r‘𝐴)) |
51 | 49, 50, 19 | 3eltr4d 2874 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 ∈
(Base‘𝑆)) |
52 | 51 | adantr 474 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 1 ∈ (Base‘𝑆)) |
53 | | eqid 2778 |
. . . . . 6
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
54 | 12, 16 | ressvsca 16424 |
. . . . . . 7
⊢ (𝐶 ∈ V → ∗ = (
·𝑠 ‘𝑆)) |
55 | 24, 54 | ax-mp 5 |
. . . . . 6
⊢ ∗ = (
·𝑠 ‘𝑆) |
56 | | eqid 2778 |
. . . . . 6
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
57 | | eqid 2778 |
. . . . . 6
⊢
(+g‘(Scalar‘𝑆)) =
(+g‘(Scalar‘𝑆)) |
58 | 2, 4, 53, 55, 56, 57 | lmodvsdir 19279 |
. . . . 5
⊢ ((𝑆 ∈ LMod ∧ (𝑦 ∈
(Base‘(Scalar‘𝑆)) ∧ 𝑧 ∈ (Base‘(Scalar‘𝑆)) ∧ 1 ∈ (Base‘𝑆))) → ((𝑦(+g‘(Scalar‘𝑆))𝑧) ∗ 1 ) = ((𝑦 ∗ 1
)(+g‘𝑆)(𝑧 ∗ 1 ))) |
59 | 38, 44, 48, 52, 58 | syl13anc 1440 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦(+g‘(Scalar‘𝑆))𝑧) ∗ 1 ) = ((𝑦 ∗ 1
)(+g‘𝑆)(𝑧 ∗ 1 ))) |
60 | 32, 59 | eqtrd 2814 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦(+g‘𝑅)𝑧) ∗ 1 ) = ((𝑦 ∗ 1
)(+g‘𝑆)(𝑧 ∗ 1 ))) |
61 | | simpr 479 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) |
62 | 61 | adantr 474 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑅 ∈ Ring) |
63 | 61 | anim1i 608 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑅 ∈ Ring ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾))) |
64 | | 3anass 1079 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ↔ (𝑅 ∈ Ring ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾))) |
65 | 63, 64 | sylibr 226 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) |
66 | 1, 3 | ringacl 18965 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → (𝑦(+g‘𝑅)𝑧) ∈ 𝐾) |
67 | 65, 66 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑦(+g‘𝑅)𝑧) ∈ 𝐾) |
68 | 1, 7, 15, 16, 17 | scmatrhmval 20738 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ (𝑦(+g‘𝑅)𝑧) ∈ 𝐾) → (𝐹‘(𝑦(+g‘𝑅)𝑧)) = ((𝑦(+g‘𝑅)𝑧) ∗ 1 )) |
69 | 62, 67, 68 | syl2anc 579 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘(𝑦(+g‘𝑅)𝑧)) = ((𝑦(+g‘𝑅)𝑧) ∗ 1 )) |
70 | 1, 7, 15, 16, 17 | scmatrhmval 20738 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (𝑦 ∗ 1 )) |
71 | 70 | ad2ant2lr 738 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘𝑦) = (𝑦 ∗ 1 )) |
72 | 1, 7, 15, 16, 17 | scmatrhmval 20738 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾) → (𝐹‘𝑧) = (𝑧 ∗ 1 )) |
73 | 72 | ad2ant2l 736 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘𝑧) = (𝑧 ∗ 1 )) |
74 | 71, 73 | oveq12d 6940 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝐹‘𝑦)(+g‘𝑆)(𝐹‘𝑧)) = ((𝑦 ∗ 1
)(+g‘𝑆)(𝑧 ∗ 1 ))) |
75 | 60, 69, 74 | 3eqtr4d 2824 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘(𝑦(+g‘𝑅)𝑧)) = ((𝐹‘𝑦)(+g‘𝑆)(𝐹‘𝑧))) |
76 | 1, 2, 3, 4, 6, 14,
21, 75 | isghmd 18053 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹 ∈ (𝑅 GrpHom 𝑆)) |