| Step | Hyp | Ref
| Expression |
| 1 | | mendassa.a |
. . . 4
⊢ 𝐴 = (MEndo‘𝑀) |
| 2 | 1 | mendbas 43192 |
. . 3
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
| 3 | 2 | a1i 11 |
. 2
⊢ (𝑀 ∈ LMod → (𝑀 LMHom 𝑀) = (Base‘𝐴)) |
| 4 | | eqidd 2738 |
. 2
⊢ (𝑀 ∈ LMod →
(+g‘𝐴) =
(+g‘𝐴)) |
| 5 | | eqidd 2738 |
. 2
⊢ (𝑀 ∈ LMod →
(.r‘𝐴) =
(.r‘𝐴)) |
| 6 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 7 | | eqid 2737 |
. . . . . 6
⊢
(+g‘𝐴) = (+g‘𝐴) |
| 8 | 1, 2, 6, 7 | mendplusg 43194 |
. . . . 5
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥(+g‘𝐴)𝑦) = (𝑥 ∘f
(+g‘𝑀)𝑦)) |
| 9 | 6 | lmhmplusg 21043 |
. . . . 5
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥 ∘f
(+g‘𝑀)𝑦) ∈ (𝑀 LMHom 𝑀)) |
| 10 | 8, 9 | eqeltrd 2841 |
. . . 4
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥(+g‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
| 11 | 10 | 3adant1 1131 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥(+g‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
| 12 | | simpr1 1195 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (𝑀 LMHom 𝑀)) |
| 13 | | simpr2 1196 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
| 14 | 12, 13, 9 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥 ∘f
(+g‘𝑀)𝑦) ∈ (𝑀 LMHom 𝑀)) |
| 15 | | simpr3 1197 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ (𝑀 LMHom 𝑀)) |
| 16 | 1, 2, 6, 7 | mendplusg 43194 |
. . . . 5
⊢ (((𝑥 ∘f
(+g‘𝑀)𝑦) ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥 ∘f
(+g‘𝑀)𝑦)(+g‘𝐴)𝑧) = ((𝑥 ∘f
(+g‘𝑀)𝑦) ∘f
(+g‘𝑀)𝑧)) |
| 17 | 14, 15, 16 | syl2anc 584 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥 ∘f
(+g‘𝑀)𝑦)(+g‘𝐴)𝑧) = ((𝑥 ∘f
(+g‘𝑀)𝑦) ∘f
(+g‘𝑀)𝑧)) |
| 18 | 12, 13, 8 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(+g‘𝐴)𝑦) = (𝑥 ∘f
(+g‘𝑀)𝑦)) |
| 19 | 18 | oveq1d 7446 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝐴)𝑦)(+g‘𝐴)𝑧) = ((𝑥 ∘f
(+g‘𝑀)𝑦)(+g‘𝐴)𝑧)) |
| 20 | 6 | lmhmplusg 21043 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦 ∘f
(+g‘𝑀)𝑧) ∈ (𝑀 LMHom 𝑀)) |
| 21 | 13, 15, 20 | syl2anc 584 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘f
(+g‘𝑀)𝑧) ∈ (𝑀 LMHom 𝑀)) |
| 22 | 1, 2, 6, 7 | mendplusg 43194 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ (𝑦 ∘f
(+g‘𝑀)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥(+g‘𝐴)(𝑦 ∘f
(+g‘𝑀)𝑧)) = (𝑥 ∘f
(+g‘𝑀)(𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 23 | 12, 21, 22 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(+g‘𝐴)(𝑦 ∘f
(+g‘𝑀)𝑧)) = (𝑥 ∘f
(+g‘𝑀)(𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 24 | 1, 2, 6, 7 | mendplusg 43194 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(+g‘𝐴)𝑧) = (𝑦 ∘f
(+g‘𝑀)𝑧)) |
| 25 | 13, 15, 24 | syl2anc 584 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(+g‘𝐴)𝑧) = (𝑦 ∘f
(+g‘𝑀)𝑧)) |
| 26 | 25 | oveq2d 7447 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(+g‘𝐴)(𝑦(+g‘𝐴)𝑧)) = (𝑥(+g‘𝐴)(𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 27 | | lmodgrp 20865 |
. . . . . . . 8
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Grp) |
| 28 | 27 | grpmndd 18964 |
. . . . . . 7
⊢ (𝑀 ∈ LMod → 𝑀 ∈ Mnd) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑀 ∈ Mnd) |
| 30 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 31 | 30, 30 | lmhmf 21033 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑀 LMHom 𝑀) → 𝑥:(Base‘𝑀)⟶(Base‘𝑀)) |
| 32 | 12, 31 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥:(Base‘𝑀)⟶(Base‘𝑀)) |
| 33 | | fvex 6919 |
. . . . . . . 8
⊢
(Base‘𝑀)
∈ V |
| 34 | 33, 33 | elmap 8911 |
. . . . . . 7
⊢ (𝑥 ∈ ((Base‘𝑀) ↑m
(Base‘𝑀)) ↔
𝑥:(Base‘𝑀)⟶(Base‘𝑀)) |
| 35 | 32, 34 | sylibr 234 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ ((Base‘𝑀) ↑m (Base‘𝑀))) |
| 36 | 30, 30 | lmhmf 21033 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝑀 LMHom 𝑀) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
| 37 | 13, 36 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
| 38 | 33, 33 | elmap 8911 |
. . . . . . 7
⊢ (𝑦 ∈ ((Base‘𝑀) ↑m
(Base‘𝑀)) ↔
𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
| 39 | 37, 38 | sylibr 234 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ ((Base‘𝑀) ↑m (Base‘𝑀))) |
| 40 | 30, 30 | lmhmf 21033 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝑀 LMHom 𝑀) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
| 41 | 15, 40 | syl 17 |
. . . . . . 7
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
| 42 | 33, 33 | elmap 8911 |
. . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝑀) ↑m
(Base‘𝑀)) ↔
𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
| 43 | 41, 42 | sylibr 234 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ ((Base‘𝑀) ↑m (Base‘𝑀))) |
| 44 | 30, 6 | mndvass 18811 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ (𝑥 ∈ ((Base‘𝑀) ↑m
(Base‘𝑀)) ∧ 𝑦 ∈ ((Base‘𝑀) ↑m
(Base‘𝑀)) ∧ 𝑧 ∈ ((Base‘𝑀) ↑m
(Base‘𝑀)))) →
((𝑥 ∘f
(+g‘𝑀)𝑦) ∘f
(+g‘𝑀)𝑧) = (𝑥 ∘f
(+g‘𝑀)(𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 45 | 29, 35, 39, 43, 44 | syl13anc 1374 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥 ∘f
(+g‘𝑀)𝑦) ∘f
(+g‘𝑀)𝑧) = (𝑥 ∘f
(+g‘𝑀)(𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 46 | 23, 26, 45 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(+g‘𝐴)(𝑦(+g‘𝐴)𝑧)) = ((𝑥 ∘f
(+g‘𝑀)𝑦) ∘f
(+g‘𝑀)𝑧)) |
| 47 | 17, 19, 46 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝐴)𝑦)(+g‘𝐴)𝑧) = (𝑥(+g‘𝐴)(𝑦(+g‘𝐴)𝑧))) |
| 48 | | id 22 |
. . . 4
⊢ (𝑀 ∈ LMod → 𝑀 ∈ LMod) |
| 49 | | eqidd 2738 |
. . . 4
⊢ (𝑀 ∈ LMod →
(Scalar‘𝑀) =
(Scalar‘𝑀)) |
| 50 | | eqid 2737 |
. . . . 5
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 51 | | eqid 2737 |
. . . . 5
⊢
(Scalar‘𝑀) =
(Scalar‘𝑀) |
| 52 | 50, 30, 51, 51 | 0lmhm 21039 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑀 ∈ LMod ∧
(Scalar‘𝑀) =
(Scalar‘𝑀)) →
((Base‘𝑀) ×
{(0g‘𝑀)})
∈ (𝑀 LMHom 𝑀)) |
| 53 | 48, 48, 49, 52 | syl3anc 1373 |
. . 3
⊢ (𝑀 ∈ LMod →
((Base‘𝑀) ×
{(0g‘𝑀)})
∈ (𝑀 LMHom 𝑀)) |
| 54 | 1, 2, 6, 7 | mendplusg 43194 |
. . . . 5
⊢
((((Base‘𝑀)
× {(0g‘𝑀)}) ∈ (𝑀 LMHom 𝑀) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {(0g‘𝑀)})(+g‘𝐴)𝑥) = (((Base‘𝑀) × {(0g‘𝑀)}) ∘f
(+g‘𝑀)𝑥)) |
| 55 | 53, 54 | sylan 580 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {(0g‘𝑀)})(+g‘𝐴)𝑥) = (((Base‘𝑀) × {(0g‘𝑀)}) ∘f
(+g‘𝑀)𝑥)) |
| 56 | 31, 34 | sylibr 234 |
. . . . 5
⊢ (𝑥 ∈ (𝑀 LMHom 𝑀) → 𝑥 ∈ ((Base‘𝑀) ↑m (Base‘𝑀))) |
| 57 | 30, 6, 50 | mndvlid 18812 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝑥 ∈ ((Base‘𝑀) ↑m
(Base‘𝑀))) →
(((Base‘𝑀) ×
{(0g‘𝑀)})
∘f (+g‘𝑀)𝑥) = 𝑥) |
| 58 | 28, 56, 57 | syl2an 596 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {(0g‘𝑀)}) ∘f
(+g‘𝑀)𝑥) = 𝑥) |
| 59 | 55, 58 | eqtrd 2777 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {(0g‘𝑀)})(+g‘𝐴)𝑥) = 𝑥) |
| 60 | | eqid 2737 |
. . . . 5
⊢
(invg‘𝑀) = (invg‘𝑀) |
| 61 | 60 | invlmhm 21041 |
. . . 4
⊢ (𝑀 ∈ LMod →
(invg‘𝑀)
∈ (𝑀 LMHom 𝑀)) |
| 62 | | lmhmco 21042 |
. . . 4
⊢
(((invg‘𝑀) ∈ (𝑀 LMHom 𝑀) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → ((invg‘𝑀) ∘ 𝑥) ∈ (𝑀 LMHom 𝑀)) |
| 63 | 61, 62 | sylan 580 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → ((invg‘𝑀) ∘ 𝑥) ∈ (𝑀 LMHom 𝑀)) |
| 64 | 1, 2, 6, 7 | mendplusg 43194 |
. . . . 5
⊢
((((invg‘𝑀) ∘ 𝑥) ∈ (𝑀 LMHom 𝑀) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((invg‘𝑀) ∘ 𝑥)(+g‘𝐴)𝑥) = (((invg‘𝑀) ∘ 𝑥) ∘f
(+g‘𝑀)𝑥)) |
| 65 | 63, 64 | sylancom 588 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((invg‘𝑀) ∘ 𝑥)(+g‘𝐴)𝑥) = (((invg‘𝑀) ∘ 𝑥) ∘f
(+g‘𝑀)𝑥)) |
| 66 | 30, 6, 60, 50 | grpvlinv 22402 |
. . . . 5
⊢ ((𝑀 ∈ Grp ∧ 𝑥 ∈ ((Base‘𝑀) ↑m
(Base‘𝑀))) →
(((invg‘𝑀)
∘ 𝑥)
∘f (+g‘𝑀)𝑥) = ((Base‘𝑀) × {(0g‘𝑀)})) |
| 67 | 27, 56, 66 | syl2an 596 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((invg‘𝑀) ∘ 𝑥) ∘f
(+g‘𝑀)𝑥) = ((Base‘𝑀) × {(0g‘𝑀)})) |
| 68 | 65, 67 | eqtrd 2777 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((invg‘𝑀) ∘ 𝑥)(+g‘𝐴)𝑥) = ((Base‘𝑀) × {(0g‘𝑀)})) |
| 69 | 3, 4, 11, 47, 53, 59, 63, 68 | isgrpd 18976 |
. 2
⊢ (𝑀 ∈ LMod → 𝐴 ∈ Grp) |
| 70 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝐴) = (.r‘𝐴) |
| 71 | 1, 2, 70 | mendmulr 43196 |
. . . 4
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)𝑦) = (𝑥 ∘ 𝑦)) |
| 72 | | lmhmco 21042 |
. . . 4
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥 ∘ 𝑦) ∈ (𝑀 LMHom 𝑀)) |
| 73 | 71, 72 | eqeltrd 2841 |
. . 3
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
| 74 | 73 | 3adant1 1131 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
| 75 | | coass 6285 |
. . 3
⊢ ((𝑥 ∘ 𝑦) ∘ 𝑧) = (𝑥 ∘ (𝑦 ∘ 𝑧)) |
| 76 | 12, 13, 71 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝐴)𝑦) = (𝑥 ∘ 𝑦)) |
| 77 | 76 | oveq1d 7446 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥 ∘ 𝑦)(.r‘𝐴)𝑧)) |
| 78 | 12, 13, 72 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥 ∘ 𝑦) ∈ (𝑀 LMHom 𝑀)) |
| 79 | 1, 2, 70 | mendmulr 43196 |
. . . . 5
⊢ (((𝑥 ∘ 𝑦) ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥 ∘ 𝑦)(.r‘𝐴)𝑧) = ((𝑥 ∘ 𝑦) ∘ 𝑧)) |
| 80 | 78, 15, 79 | syl2anc 584 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥 ∘ 𝑦)(.r‘𝐴)𝑧) = ((𝑥 ∘ 𝑦) ∘ 𝑧)) |
| 81 | 77, 80 | eqtrd 2777 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥 ∘ 𝑦) ∘ 𝑧)) |
| 82 | 1, 2, 70 | mendmulr 43196 |
. . . . . 6
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)𝑧) = (𝑦 ∘ 𝑧)) |
| 83 | 13, 15, 82 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) = (𝑦 ∘ 𝑧)) |
| 84 | 83 | oveq2d 7447 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝐴)(𝑦(.r‘𝐴)𝑧)) = (𝑥(.r‘𝐴)(𝑦 ∘ 𝑧))) |
| 85 | | lmhmco 21042 |
. . . . . 6
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦 ∘ 𝑧) ∈ (𝑀 LMHom 𝑀)) |
| 86 | 13, 15, 85 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ 𝑧) ∈ (𝑀 LMHom 𝑀)) |
| 87 | 1, 2, 70 | mendmulr 43196 |
. . . . 5
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ (𝑦 ∘ 𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)(𝑦 ∘ 𝑧)) = (𝑥 ∘ (𝑦 ∘ 𝑧))) |
| 88 | 12, 86, 87 | syl2anc 584 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝐴)(𝑦 ∘ 𝑧)) = (𝑥 ∘ (𝑦 ∘ 𝑧))) |
| 89 | 84, 88 | eqtrd 2777 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝐴)(𝑦(.r‘𝐴)𝑧)) = (𝑥 ∘ (𝑦 ∘ 𝑧))) |
| 90 | 75, 81, 89 | 3eqtr4a 2803 |
. 2
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝐴)𝑦)(.r‘𝐴)𝑧) = (𝑥(.r‘𝐴)(𝑦(.r‘𝐴)𝑧))) |
| 91 | 1, 2, 70 | mendmulr 43196 |
. . . 4
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ (𝑦 ∘f
(+g‘𝑀)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)(𝑦 ∘f
(+g‘𝑀)𝑧)) = (𝑥 ∘ (𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 92 | 12, 21, 91 | syl2anc 584 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝐴)(𝑦 ∘f
(+g‘𝑀)𝑧)) = (𝑥 ∘ (𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 93 | 25 | oveq2d 7447 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝐴)(𝑦(+g‘𝐴)𝑧)) = (𝑥(.r‘𝐴)(𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 94 | | lmhmco 21042 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥 ∘ 𝑧) ∈ (𝑀 LMHom 𝑀)) |
| 95 | 12, 15, 94 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥 ∘ 𝑧) ∈ (𝑀 LMHom 𝑀)) |
| 96 | 1, 2, 6, 7 | mendplusg 43194 |
. . . . 5
⊢ (((𝑥 ∘ 𝑦) ∈ (𝑀 LMHom 𝑀) ∧ (𝑥 ∘ 𝑧) ∈ (𝑀 LMHom 𝑀)) → ((𝑥 ∘ 𝑦)(+g‘𝐴)(𝑥 ∘ 𝑧)) = ((𝑥 ∘ 𝑦) ∘f
(+g‘𝑀)(𝑥 ∘ 𝑧))) |
| 97 | 78, 95, 96 | syl2anc 584 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥 ∘ 𝑦)(+g‘𝐴)(𝑥 ∘ 𝑧)) = ((𝑥 ∘ 𝑦) ∘f
(+g‘𝑀)(𝑥 ∘ 𝑧))) |
| 98 | 1, 2, 70 | mendmulr 43196 |
. . . . . 6
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)𝑧) = (𝑥 ∘ 𝑧)) |
| 99 | 12, 15, 98 | syl2anc 584 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝐴)𝑧) = (𝑥 ∘ 𝑧)) |
| 100 | 76, 99 | oveq12d 7449 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝐴)𝑦)(+g‘𝐴)(𝑥(.r‘𝐴)𝑧)) = ((𝑥 ∘ 𝑦)(+g‘𝐴)(𝑥 ∘ 𝑧))) |
| 101 | | lmghm 21030 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀 LMHom 𝑀) → 𝑥 ∈ (𝑀 GrpHom 𝑀)) |
| 102 | | ghmmhm 19244 |
. . . . . 6
⊢ (𝑥 ∈ (𝑀 GrpHom 𝑀) → 𝑥 ∈ (𝑀 MndHom 𝑀)) |
| 103 | 12, 101, 102 | 3syl 18 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (𝑀 MndHom 𝑀)) |
| 104 | 30, 6, 6 | mhmvlin 18814 |
. . . . 5
⊢ ((𝑥 ∈ (𝑀 MndHom 𝑀) ∧ 𝑦 ∈ ((Base‘𝑀) ↑m (Base‘𝑀)) ∧ 𝑧 ∈ ((Base‘𝑀) ↑m (Base‘𝑀))) → (𝑥 ∘ (𝑦 ∘f
(+g‘𝑀)𝑧)) = ((𝑥 ∘ 𝑦) ∘f
(+g‘𝑀)(𝑥 ∘ 𝑧))) |
| 105 | 103, 39, 43, 104 | syl3anc 1373 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥 ∘ (𝑦 ∘f
(+g‘𝑀)𝑧)) = ((𝑥 ∘ 𝑦) ∘f
(+g‘𝑀)(𝑥 ∘ 𝑧))) |
| 106 | 97, 100, 105 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝐴)𝑦)(+g‘𝐴)(𝑥(.r‘𝐴)𝑧)) = (𝑥 ∘ (𝑦 ∘f
(+g‘𝑀)𝑧))) |
| 107 | 92, 93, 106 | 3eqtr4d 2787 |
. 2
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝐴)(𝑦(+g‘𝐴)𝑧)) = ((𝑥(.r‘𝐴)𝑦)(+g‘𝐴)(𝑥(.r‘𝐴)𝑧))) |
| 108 | 1, 2, 70 | mendmulr 43196 |
. . . 4
⊢ (((𝑥 ∘f
(+g‘𝑀)𝑦) ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥 ∘f
(+g‘𝑀)𝑦)(.r‘𝐴)𝑧) = ((𝑥 ∘f
(+g‘𝑀)𝑦) ∘ 𝑧)) |
| 109 | 14, 15, 108 | syl2anc 584 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥 ∘f
(+g‘𝑀)𝑦)(.r‘𝐴)𝑧) = ((𝑥 ∘f
(+g‘𝑀)𝑦) ∘ 𝑧)) |
| 110 | 18 | oveq1d 7446 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥 ∘f
(+g‘𝑀)𝑦)(.r‘𝐴)𝑧)) |
| 111 | 1, 2, 6, 7 | mendplusg 43194 |
. . . . 5
⊢ (((𝑥 ∘ 𝑧) ∈ (𝑀 LMHom 𝑀) ∧ (𝑦 ∘ 𝑧) ∈ (𝑀 LMHom 𝑀)) → ((𝑥 ∘ 𝑧)(+g‘𝐴)(𝑦 ∘ 𝑧)) = ((𝑥 ∘ 𝑧) ∘f
(+g‘𝑀)(𝑦 ∘ 𝑧))) |
| 112 | 95, 86, 111 | syl2anc 584 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥 ∘ 𝑧)(+g‘𝐴)(𝑦 ∘ 𝑧)) = ((𝑥 ∘ 𝑧) ∘f
(+g‘𝑀)(𝑦 ∘ 𝑧))) |
| 113 | 99, 83 | oveq12d 7449 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝐴)𝑧)(+g‘𝐴)(𝑦(.r‘𝐴)𝑧)) = ((𝑥 ∘ 𝑧)(+g‘𝐴)(𝑦 ∘ 𝑧))) |
| 114 | | ffn 6736 |
. . . . . 6
⊢ (𝑥:(Base‘𝑀)⟶(Base‘𝑀) → 𝑥 Fn (Base‘𝑀)) |
| 115 | 12, 31, 114 | 3syl 18 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 Fn (Base‘𝑀)) |
| 116 | | ffn 6736 |
. . . . . 6
⊢ (𝑦:(Base‘𝑀)⟶(Base‘𝑀) → 𝑦 Fn (Base‘𝑀)) |
| 117 | 13, 36, 116 | 3syl 18 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 Fn (Base‘𝑀)) |
| 118 | 33 | a1i 11 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (Base‘𝑀) ∈ V) |
| 119 | | inidm 4227 |
. . . . 5
⊢
((Base‘𝑀)
∩ (Base‘𝑀)) =
(Base‘𝑀) |
| 120 | 115, 117,
41, 118, 118, 118, 119 | ofco 7722 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥 ∘f
(+g‘𝑀)𝑦) ∘ 𝑧) = ((𝑥 ∘ 𝑧) ∘f
(+g‘𝑀)(𝑦 ∘ 𝑧))) |
| 121 | 112, 113,
120 | 3eqtr4d 2787 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝐴)𝑧)(+g‘𝐴)(𝑦(.r‘𝐴)𝑧)) = ((𝑥 ∘f
(+g‘𝑀)𝑦) ∘ 𝑧)) |
| 122 | 109, 110,
121 | 3eqtr4d 2787 |
. 2
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (𝑀 LMHom 𝑀) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥(.r‘𝐴)𝑧)(+g‘𝐴)(𝑦(.r‘𝐴)𝑧))) |
| 123 | 30 | idlmhm 21040 |
. 2
⊢ (𝑀 ∈ LMod → ( I ↾
(Base‘𝑀)) ∈
(𝑀 LMHom 𝑀)) |
| 124 | 1, 2, 70 | mendmulr 43196 |
. . . 4
⊢ ((( I
↾ (Base‘𝑀))
∈ (𝑀 LMHom 𝑀) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (( I ↾ (Base‘𝑀))(.r‘𝐴)𝑥) = (( I ↾ (Base‘𝑀)) ∘ 𝑥)) |
| 125 | 123, 124 | sylan 580 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (( I ↾ (Base‘𝑀))(.r‘𝐴)𝑥) = (( I ↾ (Base‘𝑀)) ∘ 𝑥)) |
| 126 | 31 | adantl 481 |
. . . 4
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → 𝑥:(Base‘𝑀)⟶(Base‘𝑀)) |
| 127 | | fcoi2 6783 |
. . . 4
⊢ (𝑥:(Base‘𝑀)⟶(Base‘𝑀) → (( I ↾ (Base‘𝑀)) ∘ 𝑥) = 𝑥) |
| 128 | 126, 127 | syl 17 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (( I ↾ (Base‘𝑀)) ∘ 𝑥) = 𝑥) |
| 129 | 125, 128 | eqtrd 2777 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (( I ↾ (Base‘𝑀))(.r‘𝐴)𝑥) = 𝑥) |
| 130 | | id 22 |
. . . 4
⊢ (𝑥 ∈ (𝑀 LMHom 𝑀) → 𝑥 ∈ (𝑀 LMHom 𝑀)) |
| 131 | 1, 2, 70 | mendmulr 43196 |
. . . 4
⊢ ((𝑥 ∈ (𝑀 LMHom 𝑀) ∧ ( I ↾ (Base‘𝑀)) ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)( I ↾ (Base‘𝑀))) = (𝑥 ∘ ( I ↾ (Base‘𝑀)))) |
| 132 | 130, 123,
131 | syl2anr 597 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)( I ↾ (Base‘𝑀))) = (𝑥 ∘ ( I ↾ (Base‘𝑀)))) |
| 133 | | fcoi1 6782 |
. . . 4
⊢ (𝑥:(Base‘𝑀)⟶(Base‘𝑀) → (𝑥 ∘ ( I ↾ (Base‘𝑀))) = 𝑥) |
| 134 | 126, 133 | syl 17 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (𝑥 ∘ ( I ↾ (Base‘𝑀))) = 𝑥) |
| 135 | 132, 134 | eqtrd 2777 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (𝑥(.r‘𝐴)( I ↾ (Base‘𝑀))) = 𝑥) |
| 136 | 3, 4, 5, 69, 74, 90, 107, 122, 123, 129, 135 | isringd 20288 |
1
⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) |