Step | Hyp | Ref
| Expression |
1 | | mat1mhm.m |
. . . . 5
⊢ 𝑀 = (mulGrp‘𝑅) |
2 | 1 | ringmgp 18553 |
. . . 4
⊢ (𝑅 ∈ Ring → 𝑀 ∈ Mnd) |
3 | 2 | adantr 481 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑀 ∈ Mnd) |
4 | | snfi 8038 |
. . . . 5
⊢ {𝐸} ∈ Fin |
5 | | simpl 473 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Ring) |
6 | | mat1rhmval.a |
. . . . . 6
⊢ 𝐴 = ({𝐸} Mat 𝑅) |
7 | 6 | matring 20249 |
. . . . 5
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
8 | 4, 5, 7 | sylancr 695 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐴 ∈ Ring) |
9 | | mat1mhm.n |
. . . . 5
⊢ 𝑁 = (mulGrp‘𝐴) |
10 | 9 | ringmgp 18553 |
. . . 4
⊢ (𝐴 ∈ Ring → 𝑁 ∈ Mnd) |
11 | 8, 10 | syl 17 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑁 ∈ Mnd) |
12 | 3, 11 | jca 554 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd)) |
13 | | mat1rhmval.k |
. . . 4
⊢ 𝐾 = (Base‘𝑅) |
14 | | mat1rhmval.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
15 | | mat1rhmval.o |
. . . 4
⊢ 𝑂 = 〈𝐸, 𝐸〉 |
16 | | mat1rhmval.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) |
17 | 13, 6, 14, 15, 16 | mat1f 20288 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹:𝐾⟶𝐵) |
18 | | ringmnd 18556 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
19 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Mnd) |
20 | 19 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝑅 ∈ Mnd) |
21 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐸 ∈ 𝑉) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝐸 ∈ 𝑉) |
23 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝑅 ∈ Ring) |
24 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝐴) =
(Base‘𝐴) |
25 | | snidg 4206 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈ 𝑉 → 𝐸 ∈ {𝐸}) |
26 | 25 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝐸 ∈ {𝐸}) |
27 | | simprl 794 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝑤 ∈ 𝐾) |
28 | 13, 6, 24, 15, 16 | mat1rhmcl 20287 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾) → (𝐹‘𝑤) ∈ (Base‘𝐴)) |
29 | 23, 22, 27, 28 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘𝑤) ∈ (Base‘𝐴)) |
30 | 6, 13, 24, 26, 26, 29 | matecld 20232 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘𝑤)𝐸) ∈ 𝐾) |
31 | | simprr 796 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝑦 ∈ 𝐾) |
32 | 13, 6, 24, 15, 16 | mat1rhmcl 20287 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) ∈ (Base‘𝐴)) |
33 | 23, 22, 31, 32 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘𝑦) ∈ (Base‘𝐴)) |
34 | 6, 13, 24, 26, 26, 33 | matecld 20232 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘𝑦)𝐸) ∈ 𝐾) |
35 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
36 | 13, 35 | ringcl 18561 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝐸(𝐹‘𝑤)𝐸) ∈ 𝐾 ∧ (𝐸(𝐹‘𝑦)𝐸) ∈ 𝐾) → ((𝐸(𝐹‘𝑤)𝐸)(.r‘𝑅)(𝐸(𝐹‘𝑦)𝐸)) ∈ 𝐾) |
37 | 23, 30, 34, 36 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ((𝐸(𝐹‘𝑤)𝐸)(.r‘𝑅)(𝐸(𝐹‘𝑦)𝐸)) ∈ 𝐾) |
38 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝐸 → (𝐸(𝐹‘𝑤)𝑒) = (𝐸(𝐹‘𝑤)𝐸)) |
39 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝐸 → (𝑒(𝐹‘𝑦)𝐸) = (𝐸(𝐹‘𝑦)𝐸)) |
40 | 38, 39 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → ((𝐸(𝐹‘𝑤)𝑒)(.r‘𝑅)(𝑒(𝐹‘𝑦)𝐸)) = ((𝐸(𝐹‘𝑤)𝐸)(.r‘𝑅)(𝐸(𝐹‘𝑦)𝐸))) |
41 | 40 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑒 = 𝐸) → ((𝐸(𝐹‘𝑤)𝑒)(.r‘𝑅)(𝑒(𝐹‘𝑦)𝐸)) = ((𝐸(𝐹‘𝑤)𝐸)(.r‘𝑅)(𝐸(𝐹‘𝑦)𝐸))) |
42 | 13, 20, 22, 37, 41 | gsumsnd 18352 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑅 Σg (𝑒 ∈ {𝐸} ↦ ((𝐸(𝐹‘𝑤)𝑒)(.r‘𝑅)(𝑒(𝐹‘𝑦)𝐸)))) = ((𝐸(𝐹‘𝑤)𝐸)(.r‘𝑅)(𝐸(𝐹‘𝑦)𝐸))) |
43 | 13, 6, 14, 15, 16 | mat1rhmelval 20286 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾) → (𝐸(𝐹‘𝑤)𝐸) = 𝑤) |
44 | 23, 22, 27, 43 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘𝑤)𝐸) = 𝑤) |
45 | 13, 6, 14, 15, 16 | mat1rhmelval 20286 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾) → (𝐸(𝐹‘𝑦)𝐸) = 𝑦) |
46 | 23, 22, 31, 45 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘𝑦)𝐸) = 𝑦) |
47 | 44, 46 | oveq12d 6668 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ((𝐸(𝐹‘𝑤)𝐸)(.r‘𝑅)(𝐸(𝐹‘𝑦)𝐸)) = (𝑤(.r‘𝑅)𝑦)) |
48 | 42, 47 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑅 Σg (𝑒 ∈ {𝐸} ↦ ((𝐸(𝐹‘𝑤)𝑒)(.r‘𝑅)(𝑒(𝐹‘𝑦)𝐸)))) = (𝑤(.r‘𝑅)𝑦)) |
49 | 13, 6, 14, 15, 16 | mat1rhmcl 20287 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾) → (𝐹‘𝑤) ∈ 𝐵) |
50 | 23, 22, 27, 49 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘𝑤) ∈ 𝐵) |
51 | 13, 6, 14, 15, 16 | mat1rhmcl 20287 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) ∈ 𝐵) |
52 | 23, 22, 31, 51 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘𝑦) ∈ 𝐵) |
53 | 50, 52 | jca 554 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ((𝐹‘𝑤) ∈ 𝐵 ∧ (𝐹‘𝑦) ∈ 𝐵)) |
54 | 25, 25 | jca 554 |
. . . . . . . . 9
⊢ (𝐸 ∈ 𝑉 → (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸})) |
55 | 54 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸})) |
56 | | eqid 2622 |
. . . . . . . . 9
⊢
(.r‘𝐴) = (.r‘𝐴) |
57 | 6, 14, 35, 56 | matmulcell 20251 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ ((𝐹‘𝑤) ∈ 𝐵 ∧ (𝐹‘𝑦) ∈ 𝐵) ∧ (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸})) → (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝐸) = (𝑅 Σg (𝑒 ∈ {𝐸} ↦ ((𝐸(𝐹‘𝑤)𝑒)(.r‘𝑅)(𝑒(𝐹‘𝑦)𝐸))))) |
58 | 23, 53, 55, 57 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝐸) = (𝑅 Σg (𝑒 ∈ {𝐸} ↦ ((𝐸(𝐹‘𝑤)𝑒)(.r‘𝑅)(𝑒(𝐹‘𝑦)𝐸))))) |
59 | 13, 35 | ringcl 18561 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → (𝑤(.r‘𝑅)𝑦) ∈ 𝐾) |
60 | 23, 27, 31, 59 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑤(.r‘𝑅)𝑦) ∈ 𝐾) |
61 | 13, 6, 14, 15, 16 | mat1rhmelval 20286 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ (𝑤(.r‘𝑅)𝑦) ∈ 𝐾) → (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝐸) = (𝑤(.r‘𝑅)𝑦)) |
62 | 23, 22, 60, 61 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝐸) = (𝑤(.r‘𝑅)𝑦)) |
63 | 48, 58, 62 | 3eqtr4rd 2667 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝐸)) |
64 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐸 → (𝑖(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗)) |
65 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐸 → (𝑖((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗)) |
66 | 64, 65 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑖 = 𝐸 → ((𝑖(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗))) |
67 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐸 → (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝐸)) |
68 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑗 = 𝐸 → (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝐸)) |
69 | 67, 68 | eqeq12d 2637 |
. . . . . . . . 9
⊢ (𝑗 = 𝐸 → ((𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝐸))) |
70 | 66, 69 | 2ralsng 4220 |
. . . . . . . 8
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝐸))) |
71 | 21, 70 | sylancom 701 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝐸))) |
72 | 71 | adantr 481 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝐸))) |
73 | 63, 72 | mpbird 247 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗)) |
74 | 13, 6, 14, 15, 16 | mat1rhmcl 20287 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ (𝑤(.r‘𝑅)𝑦) ∈ 𝐾) → (𝐹‘(𝑤(.r‘𝑅)𝑦)) ∈ 𝐵) |
75 | 23, 22, 60, 74 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘(𝑤(.r‘𝑅)𝑦)) ∈ 𝐵) |
76 | 8 | adantr 481 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝐴 ∈ Ring) |
77 | 14, 56 | ringcl 18561 |
. . . . . . 7
⊢ ((𝐴 ∈ Ring ∧ (𝐹‘𝑤) ∈ 𝐵 ∧ (𝐹‘𝑦) ∈ 𝐵) → ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦)) ∈ 𝐵) |
78 | 76, 50, 52, 77 | syl3anc 1326 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦)) ∈ 𝐵) |
79 | 6, 14 | eqmat 20230 |
. . . . . 6
⊢ (((𝐹‘(𝑤(.r‘𝑅)𝑦)) ∈ 𝐵 ∧ ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦)) ∈ 𝐵) → ((𝐹‘(𝑤(.r‘𝑅)𝑦)) = ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦)) ↔ ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗))) |
80 | 75, 78, 79 | syl2anc 693 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ((𝐹‘(𝑤(.r‘𝑅)𝑦)) = ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦)) ↔ ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))𝑗))) |
81 | 73, 80 | mpbird 247 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘(𝑤(.r‘𝑅)𝑦)) = ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))) |
82 | 81 | ralrimivva 2971 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → ∀𝑤 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝐹‘(𝑤(.r‘𝑅)𝑦)) = ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦))) |
83 | | eqid 2622 |
. . . . . . 7
⊢
(1r‘𝑅) = (1r‘𝑅) |
84 | 13, 83 | ringidcl 18568 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐾) |
85 | 84 | adantr 481 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (1r‘𝑅) ∈ 𝐾) |
86 | 13, 6, 14, 15, 16 | mat1rhmval 20285 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ (1r‘𝑅) ∈ 𝐾) → (𝐹‘(1r‘𝑅)) = {〈𝑂, (1r‘𝑅)〉}) |
87 | 85, 86 | mpd3an3 1425 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝐹‘(1r‘𝑅)) = {〈𝑂, (1r‘𝑅)〉}) |
88 | 6, 13, 15 | mat1dimid 20280 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (1r‘𝐴) = {〈𝑂, (1r‘𝑅)〉}) |
89 | 87, 88 | eqtr4d 2659 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝐹‘(1r‘𝑅)) = (1r‘𝐴)) |
90 | 17, 82, 89 | 3jca 1242 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝐹:𝐾⟶𝐵 ∧ ∀𝑤 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝐹‘(𝑤(.r‘𝑅)𝑦)) = ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦)) ∧ (𝐹‘(1r‘𝑅)) = (1r‘𝐴))) |
91 | 1, 13 | mgpbas 18495 |
. . 3
⊢ 𝐾 = (Base‘𝑀) |
92 | 9, 14 | mgpbas 18495 |
. . 3
⊢ 𝐵 = (Base‘𝑁) |
93 | 1, 35 | mgpplusg 18493 |
. . 3
⊢
(.r‘𝑅) = (+g‘𝑀) |
94 | 9, 56 | mgpplusg 18493 |
. . 3
⊢
(.r‘𝐴) = (+g‘𝑁) |
95 | 1, 83 | ringidval 18503 |
. . 3
⊢
(1r‘𝑅) = (0g‘𝑀) |
96 | | eqid 2622 |
. . . 4
⊢
(1r‘𝐴) = (1r‘𝐴) |
97 | 9, 96 | ringidval 18503 |
. . 3
⊢
(1r‘𝐴) = (0g‘𝑁) |
98 | 91, 92, 93, 94, 95, 97 | ismhm 17337 |
. 2
⊢ (𝐹 ∈ (𝑀 MndHom 𝑁) ↔ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) ∧ (𝐹:𝐾⟶𝐵 ∧ ∀𝑤 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝐹‘(𝑤(.r‘𝑅)𝑦)) = ((𝐹‘𝑤)(.r‘𝐴)(𝐹‘𝑦)) ∧ (𝐹‘(1r‘𝑅)) = (1r‘𝐴)))) |
99 | 12, 90, 98 | sylanbrc 698 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹 ∈ (𝑀 MndHom 𝑁)) |