Step | Hyp | Ref
| Expression |
1 | | scmatmhm.m |
. . . . 5
⊢ 𝑀 = (mulGrp‘𝑅) |
2 | 1 | ringmgp 18553 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
3 | 2 | adantl 482 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑀 ∈ Mnd) |
4 | | scmatrhmval.a |
. . . . 5
⊢ 𝐴 = (𝑁 Mat 𝑅) |
5 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝐴) =
(Base‘𝐴) |
6 | | scmatrhmval.k |
. . . . 5
⊢ 𝐾 = (Base‘𝑅) |
7 | | eqid 2622 |
. . . . 5
⊢
(0g‘𝑅) = (0g‘𝑅) |
8 | | scmatrhmval.c |
. . . . 5
⊢ 𝐶 = (𝑁 ScMat 𝑅) |
9 | 4, 5, 6, 7, 8 | scmatsrng 20326 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ (SubRing‘𝐴)) |
10 | | scmatghm.s |
. . . . 5
⊢ 𝑆 = (𝐴 ↾s 𝐶) |
11 | 10 | subrgring 18783 |
. . . 4
⊢ (𝐶 ∈ (SubRing‘𝐴) → 𝑆 ∈ Ring) |
12 | | scmatmhm.t |
. . . . 5
⊢ 𝑇 = (mulGrp‘𝑆) |
13 | 12 | ringmgp 18553 |
. . . 4
⊢ (𝑆 ∈ Ring → 𝑇 ∈ Mnd) |
14 | 9, 11, 13 | 3syl 18 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ Mnd) |
15 | | scmatrhmval.o |
. . . . . 6
⊢ 1 =
(1r‘𝐴) |
16 | | scmatrhmval.t |
. . . . . 6
⊢ ∗ = (
·𝑠 ‘𝐴) |
17 | | scmatrhmval.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 )) |
18 | 6, 4, 15, 16, 17, 8 | scmatf 20335 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶𝐶) |
19 | 4, 8, 10 | scmatstrbas 20332 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑆) = 𝐶) |
20 | 19 | feq3d 6032 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹:𝐾⟶(Base‘𝑆) ↔ 𝐹:𝐾⟶𝐶)) |
21 | 18, 20 | mpbird 247 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶(Base‘𝑆)) |
22 | | eqid 2622 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
23 | | eqid 2622 |
. . . . . . . 8
⊢
(.r‘𝐴) = (.r‘𝐴) |
24 | 4, 6, 7, 15, 16, 22, 23 | scmatscmiddistr 20314 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦 ∗ 1
)(.r‘𝐴)(𝑧 ∗ 1 )) = ((𝑦(.r‘𝑅)𝑧) ∗ 1 )) |
25 | 10, 23 | ressmulr 16006 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (SubRing‘𝐴) →
(.r‘𝐴) =
(.r‘𝑆)) |
26 | 9, 25 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(.r‘𝐴) =
(.r‘𝑆)) |
27 | 26 | adantr 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (.r‘𝐴) = (.r‘𝑆)) |
28 | 27 | oveqd 6667 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦 ∗ 1
)(.r‘𝐴)(𝑧 ∗ 1 )) = ((𝑦 ∗ 1
)(.r‘𝑆)(𝑧 ∗ 1 ))) |
29 | 24, 28 | eqtr3d 2658 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦(.r‘𝑅)𝑧) ∗ 1 ) = ((𝑦 ∗ 1
)(.r‘𝑆)(𝑧 ∗ 1 ))) |
30 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑅 ∈ Ring) |
32 | 30 | anim1i 592 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑅 ∈ Ring ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾))) |
33 | | 3anass 1042 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ↔ (𝑅 ∈ Ring ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾))) |
34 | 32, 33 | sylibr 224 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) |
35 | 6, 22 | ringcl 18561 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → (𝑦(.r‘𝑅)𝑧) ∈ 𝐾) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑦(.r‘𝑅)𝑧) ∈ 𝐾) |
37 | 6, 4, 15, 16, 17 | scmatrhmval 20333 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝑦(.r‘𝑅)𝑧) ∈ 𝐾) → (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝑦(.r‘𝑅)𝑧) ∗ 1 )) |
38 | 31, 36, 37 | syl2anc 693 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝑦(.r‘𝑅)𝑧) ∗ 1 )) |
39 | 6, 4, 15, 16, 17 | scmatrhmval 20333 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (𝑦 ∗ 1 )) |
40 | 39 | ad2ant2lr 784 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘𝑦) = (𝑦 ∗ 1 )) |
41 | 6, 4, 15, 16, 17 | scmatrhmval 20333 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾) → (𝐹‘𝑧) = (𝑧 ∗ 1 )) |
42 | 41 | ad2ant2l 782 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘𝑧) = (𝑧 ∗ 1 )) |
43 | 40, 42 | oveq12d 6668 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧)) = ((𝑦 ∗ 1
)(.r‘𝑆)(𝑧 ∗ 1 ))) |
44 | 29, 38, 43 | 3eqtr4d 2666 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧))) |
45 | 44 | ralrimivva 2971 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐾 (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧))) |
46 | | eqid 2622 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (1r‘𝑅) |
47 | 6, 46 | ringidcl 18568 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐾) |
48 | 47 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝑅)
∈ 𝐾) |
49 | 6, 4, 15, 16, 17 | scmatrhmval 20333 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
∈ 𝐾) → (𝐹‘(1r‘𝑅)) = ((1r‘𝑅) ∗ 1 )) |
50 | 30, 48, 49 | syl2anc 693 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹‘(1r‘𝑅)) = ((1r‘𝑅) ∗ 1 )) |
51 | 4 | matsca2 20226 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝐴)) |
52 | 51 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝑅) =
(1r‘(Scalar‘𝐴))) |
53 | 52 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
((1r‘𝑅)
∗
1 ) =
((1r‘(Scalar‘𝐴)) ∗ 1 )) |
54 | 4 | matlmod 20235 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
55 | 4 | matring 20249 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
56 | 5, 15 | ringidcl 18568 |
. . . . . . . . 9
⊢ (𝐴 ∈ Ring → 1 ∈
(Base‘𝐴)) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 ∈
(Base‘𝐴)) |
58 | | eqid 2622 |
. . . . . . . . 9
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
59 | | eqid 2622 |
. . . . . . . . 9
⊢
(1r‘(Scalar‘𝐴)) =
(1r‘(Scalar‘𝐴)) |
60 | 5, 58, 16, 59 | lmodvs1 18891 |
. . . . . . . 8
⊢ ((𝐴 ∈ LMod ∧ 1 ∈
(Base‘𝐴)) →
((1r‘(Scalar‘𝐴)) ∗ 1 ) = 1 ) |
61 | 54, 57, 60 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
((1r‘(Scalar‘𝐴)) ∗ 1 ) = 1 ) |
62 | 53, 61 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
((1r‘𝑅)
∗
1 ) =
1
) |
63 | 50, 62 | eqtrd 2656 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹‘(1r‘𝑅)) = 1 ) |
64 | 10, 15 | subrg1 18790 |
. . . . . 6
⊢ (𝐶 ∈ (SubRing‘𝐴) → 1 =
(1r‘𝑆)) |
65 | 9, 64 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 =
(1r‘𝑆)) |
66 | 63, 65 | eqtrd 2656 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) |
67 | 21, 45, 66 | 3jca 1242 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹:𝐾⟶(Base‘𝑆) ∧ ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐾 (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧)) ∧ (𝐹‘(1r‘𝑅)) = (1r‘𝑆))) |
68 | 3, 14, 67 | jca31 557 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑀 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐾⟶(Base‘𝑆) ∧ ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐾 (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧)) ∧ (𝐹‘(1r‘𝑅)) = (1r‘𝑆)))) |
69 | 1, 6 | mgpbas 18495 |
. . 3
⊢ 𝐾 = (Base‘𝑀) |
70 | | eqid 2622 |
. . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) |
71 | 12, 70 | mgpbas 18495 |
. . 3
⊢
(Base‘𝑆) =
(Base‘𝑇) |
72 | 1, 22 | mgpplusg 18493 |
. . 3
⊢
(.r‘𝑅) = (+g‘𝑀) |
73 | | eqid 2622 |
. . . 4
⊢
(.r‘𝑆) = (.r‘𝑆) |
74 | 12, 73 | mgpplusg 18493 |
. . 3
⊢
(.r‘𝑆) = (+g‘𝑇) |
75 | 1, 46 | ringidval 18503 |
. . 3
⊢
(1r‘𝑅) = (0g‘𝑀) |
76 | | eqid 2622 |
. . . 4
⊢
(1r‘𝑆) = (1r‘𝑆) |
77 | 12, 76 | ringidval 18503 |
. . 3
⊢
(1r‘𝑆) = (0g‘𝑇) |
78 | 69, 71, 72, 74, 75, 77 | ismhm 17337 |
. 2
⊢ (𝐹 ∈ (𝑀 MndHom 𝑇) ↔ ((𝑀 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐾⟶(Base‘𝑆) ∧ ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐾 (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧)) ∧ (𝐹‘(1r‘𝑅)) = (1r‘𝑆)))) |
79 | 68, 78 | sylibr 224 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹 ∈ (𝑀 MndHom 𝑇)) |