| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | scmatmhm.m | . . . 4
⊢ 𝑀 = (mulGrp‘𝑅) | 
| 2 | 1 | ringmgp 20236 | . . 3
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) | 
| 3 | 2 | adantl 481 | . 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑀 ∈ Mnd) | 
| 4 |  | scmatrhmval.a | . . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) | 
| 5 |  | eqid 2737 | . . . 4
⊢
(Base‘𝐴) =
(Base‘𝐴) | 
| 6 |  | scmatrhmval.k | . . . 4
⊢ 𝐾 = (Base‘𝑅) | 
| 7 |  | eqid 2737 | . . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) | 
| 8 |  | scmatrhmval.c | . . . 4
⊢ 𝐶 = (𝑁 ScMat 𝑅) | 
| 9 | 4, 5, 6, 7, 8 | scmatsrng 22526 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ (SubRing‘𝐴)) | 
| 10 |  | scmatghm.s | . . . 4
⊢ 𝑆 = (𝐴 ↾s 𝐶) | 
| 11 | 10 | subrgring 20574 | . . 3
⊢ (𝐶 ∈ (SubRing‘𝐴) → 𝑆 ∈ Ring) | 
| 12 |  | scmatmhm.t | . . . 4
⊢ 𝑇 = (mulGrp‘𝑆) | 
| 13 | 12 | ringmgp 20236 | . . 3
⊢ (𝑆 ∈ Ring → 𝑇 ∈ Mnd) | 
| 14 | 9, 11, 13 | 3syl 18 | . 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ Mnd) | 
| 15 |  | scmatrhmval.o | . . . . 5
⊢  1 =
(1r‘𝐴) | 
| 16 |  | scmatrhmval.t | . . . . 5
⊢  ∗ = (
·𝑠 ‘𝐴) | 
| 17 |  | scmatrhmval.f | . . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ (𝑥 ∗ 1 )) | 
| 18 | 6, 4, 15, 16, 17, 8 | scmatf 22535 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶𝐶) | 
| 19 | 4, 8, 10 | scmatstrbas 22532 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑆) = 𝐶) | 
| 20 | 19 | feq3d 6723 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹:𝐾⟶(Base‘𝑆) ↔ 𝐹:𝐾⟶𝐶)) | 
| 21 | 18, 20 | mpbird 257 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹:𝐾⟶(Base‘𝑆)) | 
| 22 |  | eqid 2737 | . . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 23 |  | eqid 2737 | . . . . . . 7
⊢
(.r‘𝐴) = (.r‘𝐴) | 
| 24 | 4, 6, 7, 15, 16, 22, 23 | scmatscmiddistr 22514 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦 ∗ 1
)(.r‘𝐴)(𝑧 ∗ 1 )) = ((𝑦(.r‘𝑅)𝑧) ∗ 1 )) | 
| 25 | 10, 23 | ressmulr 17351 | . . . . . . . . 9
⊢ (𝐶 ∈ (SubRing‘𝐴) →
(.r‘𝐴) =
(.r‘𝑆)) | 
| 26 | 9, 25 | syl 17 | . . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(.r‘𝐴) =
(.r‘𝑆)) | 
| 27 | 26 | adantr 480 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (.r‘𝐴) = (.r‘𝑆)) | 
| 28 | 27 | oveqd 7448 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦 ∗ 1
)(.r‘𝐴)(𝑧 ∗ 1 )) = ((𝑦 ∗ 1
)(.r‘𝑆)(𝑧 ∗ 1 ))) | 
| 29 | 24, 28 | eqtr3d 2779 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝑦(.r‘𝑅)𝑧) ∗ 1 ) = ((𝑦 ∗ 1
)(.r‘𝑆)(𝑧 ∗ 1 ))) | 
| 30 |  | simpr 484 | . . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) | 
| 31 | 30 | adantr 480 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → 𝑅 ∈ Ring) | 
| 32 | 30 | anim1i 615 | . . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑅 ∈ Ring ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾))) | 
| 33 |  | 3anass 1095 | . . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) ↔ (𝑅 ∈ Ring ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾))) | 
| 34 | 32, 33 | sylibr 234 | . . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) | 
| 35 | 6, 22 | ringcl 20247 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾) → (𝑦(.r‘𝑅)𝑧) ∈ 𝐾) | 
| 36 | 34, 35 | syl 17 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝑦(.r‘𝑅)𝑧) ∈ 𝐾) | 
| 37 | 6, 4, 15, 16, 17 | scmatrhmval 22533 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧ (𝑦(.r‘𝑅)𝑧) ∈ 𝐾) → (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝑦(.r‘𝑅)𝑧) ∗ 1 )) | 
| 38 | 31, 36, 37 | syl2anc 584 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝑦(.r‘𝑅)𝑧) ∗ 1 )) | 
| 39 | 6, 4, 15, 16, 17 | scmatrhmval 22533 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) = (𝑦 ∗ 1 )) | 
| 40 | 39 | ad2ant2lr 748 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘𝑦) = (𝑦 ∗ 1 )) | 
| 41 | 6, 4, 15, 16, 17 | scmatrhmval 22533 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑧 ∈ 𝐾) → (𝐹‘𝑧) = (𝑧 ∗ 1 )) | 
| 42 | 41 | ad2ant2l 746 | . . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘𝑧) = (𝑧 ∗ 1 )) | 
| 43 | 40, 42 | oveq12d 7449 | . . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧)) = ((𝑦 ∗ 1
)(.r‘𝑆)(𝑧 ∗ 1 ))) | 
| 44 | 29, 38, 43 | 3eqtr4d 2787 | . . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝐾)) → (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧))) | 
| 45 | 44 | ralrimivva 3202 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐾 (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧))) | 
| 46 |  | eqid 2737 | . . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 47 | 6, 46 | ringidcl 20262 | . . . . . 6
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐾) | 
| 48 | 6, 4, 15, 16, 17 | scmatrhmval 22533 | . . . . . 6
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
∈ 𝐾) → (𝐹‘(1r‘𝑅)) = ((1r‘𝑅) ∗ 1 )) | 
| 49 | 30, 47, 48 | syl2anc2 585 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹‘(1r‘𝑅)) = ((1r‘𝑅) ∗ 1 )) | 
| 50 | 4 | matsca2 22426 | . . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝐴)) | 
| 51 | 50 | fveq2d 6910 | . . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(1r‘𝑅) =
(1r‘(Scalar‘𝐴))) | 
| 52 | 51 | oveq1d 7446 | . . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
((1r‘𝑅)
∗
1 ) =
((1r‘(Scalar‘𝐴)) ∗ 1 )) | 
| 53 | 4 | matlmod 22435 | . . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) | 
| 54 | 4 | matring 22449 | . . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) | 
| 55 | 5, 15 | ringidcl 20262 | . . . . . . . 8
⊢ (𝐴 ∈ Ring → 1 ∈
(Base‘𝐴)) | 
| 56 | 54, 55 | syl 17 | . . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 ∈
(Base‘𝐴)) | 
| 57 |  | eqid 2737 | . . . . . . . 8
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) | 
| 58 |  | eqid 2737 | . . . . . . . 8
⊢
(1r‘(Scalar‘𝐴)) =
(1r‘(Scalar‘𝐴)) | 
| 59 | 5, 57, 16, 58 | lmodvs1 20888 | . . . . . . 7
⊢ ((𝐴 ∈ LMod ∧ 1 ∈
(Base‘𝐴)) →
((1r‘(Scalar‘𝐴)) ∗ 1 ) = 1 ) | 
| 60 | 53, 56, 59 | syl2anc 584 | . . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
((1r‘(Scalar‘𝐴)) ∗ 1 ) = 1 ) | 
| 61 | 52, 60 | eqtrd 2777 | . . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
((1r‘𝑅)
∗
1 ) =
1
) | 
| 62 | 49, 61 | eqtrd 2777 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹‘(1r‘𝑅)) = 1 ) | 
| 63 | 10, 15 | subrg1 20582 | . . . . 5
⊢ (𝐶 ∈ (SubRing‘𝐴) → 1 =
(1r‘𝑆)) | 
| 64 | 9, 63 | syl 17 | . . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 =
(1r‘𝑆)) | 
| 65 | 62, 64 | eqtrd 2777 | . . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹‘(1r‘𝑅)) = (1r‘𝑆)) | 
| 66 | 21, 45, 65 | 3jca 1129 | . 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝐹:𝐾⟶(Base‘𝑆) ∧ ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐾 (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧)) ∧ (𝐹‘(1r‘𝑅)) = (1r‘𝑆))) | 
| 67 | 1, 6 | mgpbas 20142 | . . 3
⊢ 𝐾 = (Base‘𝑀) | 
| 68 |  | eqid 2737 | . . . 4
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 69 | 12, 68 | mgpbas 20142 | . . 3
⊢
(Base‘𝑆) =
(Base‘𝑇) | 
| 70 | 1, 22 | mgpplusg 20141 | . . 3
⊢
(.r‘𝑅) = (+g‘𝑀) | 
| 71 |  | eqid 2737 | . . . 4
⊢
(.r‘𝑆) = (.r‘𝑆) | 
| 72 | 12, 71 | mgpplusg 20141 | . . 3
⊢
(.r‘𝑆) = (+g‘𝑇) | 
| 73 | 1, 46 | ringidval 20180 | . . 3
⊢
(1r‘𝑅) = (0g‘𝑀) | 
| 74 |  | eqid 2737 | . . . 4
⊢
(1r‘𝑆) = (1r‘𝑆) | 
| 75 | 12, 74 | ringidval 20180 | . . 3
⊢
(1r‘𝑆) = (0g‘𝑇) | 
| 76 | 67, 69, 70, 72, 73, 75 | ismhm 18798 | . 2
⊢ (𝐹 ∈ (𝑀 MndHom 𝑇) ↔ ((𝑀 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐾⟶(Base‘𝑆) ∧ ∀𝑦 ∈ 𝐾 ∀𝑧 ∈ 𝐾 (𝐹‘(𝑦(.r‘𝑅)𝑧)) = ((𝐹‘𝑦)(.r‘𝑆)(𝐹‘𝑧)) ∧ (𝐹‘(1r‘𝑅)) = (1r‘𝑆)))) | 
| 77 | 3, 14, 66, 76 | syl21anbrc 1345 | 1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐹 ∈ (𝑀 MndHom 𝑇)) |