| Step | Hyp | Ref
| Expression |
| 1 | | mat1rhmval.k |
. 2
⊢ 𝐾 = (Base‘𝑅) |
| 2 | | mat1rhmval.b |
. 2
⊢ 𝐵 = (Base‘𝐴) |
| 3 | | eqid 2737 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 4 | | eqid 2737 |
. 2
⊢
(+g‘𝐴) = (+g‘𝐴) |
| 5 | | ringgrp 20235 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
| 6 | 5 | adantr 480 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Grp) |
| 7 | | snfi 9083 |
. . 3
⊢ {𝐸} ∈ Fin |
| 8 | | simpl 482 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝑅 ∈ Ring) |
| 9 | | mat1rhmval.a |
. . . 4
⊢ 𝐴 = ({𝐸} Mat 𝑅) |
| 10 | 9 | matgrp 22436 |
. . 3
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Grp) |
| 11 | 7, 8, 10 | sylancr 587 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐴 ∈ Grp) |
| 12 | | mat1rhmval.o |
. . 3
⊢ 𝑂 = 〈𝐸, 𝐸〉 |
| 13 | | mat1rhmval.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐾 ↦ {〈𝑂, 𝑥〉}) |
| 14 | 1, 9, 2, 12, 13 | mat1f 22488 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹:𝐾⟶𝐵) |
| 15 | 8 | adantr 480 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝑅 ∈ Ring) |
| 16 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐸 ∈ 𝑉) |
| 17 | 16 | adantr 480 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝐸 ∈ 𝑉) |
| 18 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → 𝑤 ∈ 𝐾) |
| 19 | 18 | adantl 481 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝑤 ∈ 𝐾) |
| 20 | 1, 9, 2, 12, 13 | mat1rhmelval 22486 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾) → (𝐸(𝐹‘𝑤)𝐸) = 𝑤) |
| 21 | 15, 17, 19, 20 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘𝑤)𝐸) = 𝑤) |
| 22 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → 𝑦 ∈ 𝐾) |
| 23 | 22 | adantl 481 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝑦 ∈ 𝐾) |
| 24 | 1, 9, 2, 12, 13 | mat1rhmelval 22486 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾) → (𝐸(𝐹‘𝑦)𝐸) = 𝑦) |
| 25 | 15, 17, 23, 24 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘𝑦)𝐸) = 𝑦) |
| 26 | 21, 25 | oveq12d 7449 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ((𝐸(𝐹‘𝑤)𝐸)(+g‘𝑅)(𝐸(𝐹‘𝑦)𝐸)) = (𝑤(+g‘𝑅)𝑦)) |
| 27 | 1, 9, 2, 12, 13 | mat1rhmcl 22487 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾) → (𝐹‘𝑤) ∈ 𝐵) |
| 28 | 15, 17, 19, 27 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘𝑤) ∈ 𝐵) |
| 29 | 1, 9, 2, 12, 13 | mat1rhmcl 22487 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾) → (𝐹‘𝑦) ∈ 𝐵) |
| 30 | 15, 17, 23, 29 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘𝑦) ∈ 𝐵) |
| 31 | | snidg 4660 |
. . . . . . . . 9
⊢ (𝐸 ∈ 𝑉 → 𝐸 ∈ {𝐸}) |
| 32 | 31, 31 | jca 511 |
. . . . . . . 8
⊢ (𝐸 ∈ 𝑉 → (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸})) |
| 33 | 32 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸})) |
| 34 | 33 | adantr 480 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸})) |
| 35 | 9, 2, 4, 3 | matplusgcell 22439 |
. . . . . 6
⊢ ((((𝐹‘𝑤) ∈ 𝐵 ∧ (𝐹‘𝑦) ∈ 𝐵) ∧ (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸})) → (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝐸) = ((𝐸(𝐹‘𝑤)𝐸)(+g‘𝑅)(𝐸(𝐹‘𝑦)𝐸))) |
| 36 | 28, 30, 34, 35 | syl21anc 838 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝐸) = ((𝐸(𝐹‘𝑤)𝐸)(+g‘𝑅)(𝐸(𝐹‘𝑦)𝐸))) |
| 37 | 1, 3 | ringacl 20275 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾) → (𝑤(+g‘𝑅)𝑦) ∈ 𝐾) |
| 38 | 15, 19, 23, 37 | syl3anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑤(+g‘𝑅)𝑦) ∈ 𝐾) |
| 39 | 1, 9, 2, 12, 13 | mat1rhmelval 22486 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ (𝑤(+g‘𝑅)𝑦) ∈ 𝐾) → (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝐸) = (𝑤(+g‘𝑅)𝑦)) |
| 40 | 15, 17, 38, 39 | syl3anc 1373 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝐸) = (𝑤(+g‘𝑅)𝑦)) |
| 41 | 26, 36, 40 | 3eqtr4rd 2788 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝐸)) |
| 42 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑖 = 𝐸 → (𝑖(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗)) |
| 43 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑖 = 𝐸 → (𝑖((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗)) |
| 44 | 42, 43 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑖 = 𝐸 → ((𝑖(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗))) |
| 45 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑗 = 𝐸 → (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝐸)) |
| 46 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑗 = 𝐸 → (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝐸)) |
| 47 | 45, 46 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑗 = 𝐸 → ((𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝐸))) |
| 48 | 44, 47 | 2ralsng 4678 |
. . . . . 6
⊢ ((𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝐸))) |
| 49 | 16, 16, 48 | syl2anc 584 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝐸))) |
| 50 | 49 | adantr 480 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(+g‘𝑅)𝑦))𝐸) = (𝐸((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝐸))) |
| 51 | 41, 50 | mpbird 257 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗)) |
| 52 | 1, 9, 2, 12, 13 | mat1rhmcl 22487 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ (𝑤(+g‘𝑅)𝑦) ∈ 𝐾) → (𝐹‘(𝑤(+g‘𝑅)𝑦)) ∈ 𝐵) |
| 53 | 15, 17, 38, 52 | syl3anc 1373 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘(𝑤(+g‘𝑅)𝑦)) ∈ 𝐵) |
| 54 | 9 | matring 22449 |
. . . . . . 7
⊢ (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
| 55 | 7, 8, 54 | sylancr 587 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐴 ∈ Ring) |
| 56 | 55 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → 𝐴 ∈ Ring) |
| 57 | 2, 4 | ringacl 20275 |
. . . . 5
⊢ ((𝐴 ∈ Ring ∧ (𝐹‘𝑤) ∈ 𝐵 ∧ (𝐹‘𝑦) ∈ 𝐵) → ((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦)) ∈ 𝐵) |
| 58 | 56, 28, 30, 57 | syl3anc 1373 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦)) ∈ 𝐵) |
| 59 | 9, 2 | eqmat 22430 |
. . . 4
⊢ (((𝐹‘(𝑤(+g‘𝑅)𝑦)) ∈ 𝐵 ∧ ((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦)) ∈ 𝐵) → ((𝐹‘(𝑤(+g‘𝑅)𝑦)) = ((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦)) ↔ ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗))) |
| 60 | 53, 58, 59 | syl2anc 584 |
. . 3
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → ((𝐹‘(𝑤(+g‘𝑅)𝑦)) = ((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦)) ↔ ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(+g‘𝑅)𝑦))𝑗) = (𝑖((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))𝑗))) |
| 61 | 51, 60 | mpbird 257 |
. 2
⊢ (((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) ∧ (𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝐹‘(𝑤(+g‘𝑅)𝑦)) = ((𝐹‘𝑤)(+g‘𝐴)(𝐹‘𝑦))) |
| 62 | 1, 2, 3, 4, 6, 11,
14, 61 | isghmd 19243 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉) → 𝐹 ∈ (𝑅 GrpHom 𝐴)) |