Step | Hyp | Ref
| Expression |
1 | | mendassa.a |
. . . 4
⊢ 𝐴 = (MEndo‘𝑀) |
2 | 1 | mendbas 40581 |
. . 3
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
3 | 2 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (𝑀 LMHom 𝑀) = (Base‘𝐴)) |
4 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(+g‘𝐴) =
(+g‘𝐴)) |
5 | | mendassa.s |
. . . 4
⊢ 𝑆 = (Scalar‘𝑀) |
6 | 1, 5 | mendsca 40586 |
. . 3
⊢ 𝑆 = (Scalar‘𝐴) |
7 | 6 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 = (Scalar‘𝐴)) |
8 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴)) |
9 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(Base‘𝑆) =
(Base‘𝑆)) |
10 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(+g‘𝑆) =
(+g‘𝑆)) |
11 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(.r‘𝑆) =
(.r‘𝑆)) |
12 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(1r‘𝑆) =
(1r‘𝑆)) |
13 | | crngring 19428 |
. . 3
⊢ (𝑆 ∈ CRing → 𝑆 ∈ Ring) |
14 | 13 | adantl 485 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 ∈ Ring) |
15 | 1 | mendring 40589 |
. . . 4
⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) |
16 | 15 | adantr 484 |
. . 3
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ Ring) |
17 | | ringgrp 19421 |
. . 3
⊢ (𝐴 ∈ Ring → 𝐴 ∈ Grp) |
18 | 16, 17 | syl 17 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ Grp) |
19 | | eqid 2738 |
. . . . 5
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
20 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑆) =
(Base‘𝑆) |
21 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝑀) =
(Base‘𝑀) |
22 | | eqid 2738 |
. . . . 5
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
23 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 40588 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
24 | 23 | 3adant1 1131 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
25 | 21, 19, 5, 20 | lmhmvsca 19936 |
. . . 4
⊢ ((𝑆 ∈ CRing ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦) ∈ (𝑀 LMHom 𝑀)) |
26 | 25 | 3adant1l 1177 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦) ∈ (𝑀 LMHom 𝑀)) |
27 | 24, 26 | eqeltrd 2833 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
28 | | simpr2 1196 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
29 | | simpr3 1197 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ (𝑀 LMHom 𝑀)) |
30 | | eqid 2738 |
. . . . . 6
⊢
(+g‘𝑀) = (+g‘𝑀) |
31 | | eqid 2738 |
. . . . . 6
⊢
(+g‘𝐴) = (+g‘𝐴) |
32 | 1, 2, 30, 31 | mendplusg 40583 |
. . . . 5
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(+g‘𝐴)𝑧) = (𝑦 ∘f
(+g‘𝑀)𝑧)) |
33 | 28, 29, 32 | syl2anc 587 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(+g‘𝐴)𝑧) = (𝑦 ∘f
(+g‘𝑀)𝑧)) |
34 | 33 | oveq2d 7186 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(+g‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦 ∘f
(+g‘𝑀)𝑧))) |
35 | | simpr1 1195 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (Base‘𝑆)) |
36 | 18 | adantr 484 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝐴 ∈ Grp) |
37 | 2, 31 | grpcl 18227 |
. . . . 5
⊢ ((𝐴 ∈ Grp ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(+g‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
38 | 36, 28, 29, 37 | syl3anc 1372 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(+g‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
39 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 40588 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ (𝑦(+g‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)(𝑦(+g‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(+g‘𝐴)𝑧))) |
40 | 35, 38, 39 | syl2anc 587 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(+g‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(+g‘𝐴)𝑧))) |
41 | 35, 28, 23 | syl2anc 587 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
42 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 40588 |
. . . . . 6
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
43 | 35, 29, 42 | syl2anc 587 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
44 | 41, 43 | oveq12d 7188 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦) ∘f
(+g‘𝑀)(𝑥( ·𝑠
‘𝐴)𝑧)) = ((((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦) ∘f
(+g‘𝑀)(((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧))) |
45 | 27 | 3adant3r3 1185 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
46 | | eleq1w 2815 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑦 ∈ (𝑀 LMHom 𝑀) ↔ 𝑧 ∈ (𝑀 LMHom 𝑀))) |
47 | 46 | 3anbi3d 1443 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) ↔ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)))) |
48 | | oveq2 7178 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑥( ·𝑠
‘𝐴)𝑦) = (𝑥( ·𝑠
‘𝐴)𝑧)) |
49 | 48 | eleq1d 2817 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀) ↔ (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀))) |
50 | 47, 49 | imbi12d 348 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) ↔ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)))) |
51 | 50, 27 | chvarvv 2010 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
52 | 51 | 3adant3r2 1184 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
53 | 1, 2, 30, 31 | mendplusg 40583 |
. . . . 5
⊢ (((𝑥(
·𝑠 ‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀) ∧ (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → ((𝑥( ·𝑠
‘𝐴)𝑦)(+g‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘f
(+g‘𝑀)(𝑥( ·𝑠
‘𝐴)𝑧))) |
54 | 45, 52, 53 | syl2anc 587 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(+g‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘f
(+g‘𝑀)(𝑥( ·𝑠
‘𝐴)𝑧))) |
55 | | fvexd 6689 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (Base‘𝑀) ∈ V) |
56 | | fconst6g 6567 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝑆) → ((Base‘𝑀) × {𝑥}):(Base‘𝑀)⟶(Base‘𝑆)) |
57 | 35, 56 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}):(Base‘𝑀)⟶(Base‘𝑆)) |
58 | 21, 21 | lmhmf 19925 |
. . . . . 6
⊢ (𝑦 ∈ (𝑀 LMHom 𝑀) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
59 | 28, 58 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
60 | 21, 21 | lmhmf 19925 |
. . . . . 6
⊢ (𝑧 ∈ (𝑀 LMHom 𝑀) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
61 | 29, 60 | syl 17 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
62 | | simpll 767 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑀 ∈ LMod) |
63 | 21, 30, 5, 19, 20 | lmodvsdi 19776 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑤 ∈ (Base‘𝑆) ∧ 𝑣 ∈ (Base‘𝑀) ∧ 𝑢 ∈ (Base‘𝑀))) → (𝑤( ·𝑠
‘𝑀)(𝑣(+g‘𝑀)𝑢)) = ((𝑤( ·𝑠
‘𝑀)𝑣)(+g‘𝑀)(𝑤( ·𝑠
‘𝑀)𝑢))) |
64 | 62, 63 | sylan 583 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ (𝑤 ∈ (Base‘𝑆) ∧ 𝑣 ∈ (Base‘𝑀) ∧ 𝑢 ∈ (Base‘𝑀))) → (𝑤( ·𝑠
‘𝑀)(𝑣(+g‘𝑀)𝑢)) = ((𝑤( ·𝑠
‘𝑀)𝑣)(+g‘𝑀)(𝑤( ·𝑠
‘𝑀)𝑢))) |
65 | 55, 57, 59, 61, 64 | caofdi 7463 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦 ∘f
(+g‘𝑀)𝑧)) = ((((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦) ∘f
(+g‘𝑀)(((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧))) |
66 | 44, 54, 65 | 3eqtr4d 2783 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(+g‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦 ∘f
(+g‘𝑀)𝑧))) |
67 | 34, 40, 66 | 3eqtr4d 2783 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(+g‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑦)(+g‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧))) |
68 | | fvexd 6689 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (Base‘𝑀) ∈ V) |
69 | | simpr3 1197 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ (𝑀 LMHom 𝑀)) |
70 | 69, 60 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
71 | | simpr1 1195 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (Base‘𝑆)) |
72 | 71, 56 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}):(Base‘𝑀)⟶(Base‘𝑆)) |
73 | | simpr2 1196 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ (Base‘𝑆)) |
74 | | fconst6g 6567 |
. . . . 5
⊢ (𝑦 ∈ (Base‘𝑆) → ((Base‘𝑀) × {𝑦}):(Base‘𝑀)⟶(Base‘𝑆)) |
75 | 73, 74 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑦}):(Base‘𝑀)⟶(Base‘𝑆)) |
76 | | simpll 767 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑀 ∈ LMod) |
77 | | eqid 2738 |
. . . . . 6
⊢
(+g‘𝑆) = (+g‘𝑆) |
78 | 21, 30, 5, 19, 20, 77 | lmodvsdir 19777 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ (𝑤 ∈ (Base‘𝑆) ∧ 𝑣 ∈ (Base‘𝑆) ∧ 𝑢 ∈ (Base‘𝑀))) → ((𝑤(+g‘𝑆)𝑣)( ·𝑠
‘𝑀)𝑢) = ((𝑤( ·𝑠
‘𝑀)𝑢)(+g‘𝑀)(𝑣( ·𝑠
‘𝑀)𝑢))) |
79 | 76, 78 | sylan 583 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ (𝑤 ∈ (Base‘𝑆) ∧ 𝑣 ∈ (Base‘𝑆) ∧ 𝑢 ∈ (Base‘𝑀))) → ((𝑤(+g‘𝑆)𝑣)( ·𝑠
‘𝑀)𝑢) = ((𝑤( ·𝑠
‘𝑀)𝑢)(+g‘𝑀)(𝑣( ·𝑠
‘𝑀)𝑢))) |
80 | 68, 70, 72, 75, 79 | caofdir 7464 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((((Base‘𝑀) × {𝑥}) ∘f
(+g‘𝑆)((Base‘𝑀) × {𝑦})) ∘f (
·𝑠 ‘𝑀)𝑧) = ((((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧) ∘f
(+g‘𝑀)(((Base‘𝑀) × {𝑦}) ∘f (
·𝑠 ‘𝑀)𝑧))) |
81 | 14 | adantr 484 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑆 ∈ Ring) |
82 | 20, 77 | ringacl 19450 |
. . . . . 6
⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆)) |
83 | 81, 71, 73, 82 | syl3anc 1372 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆)) |
84 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 40588 |
. . . . 5
⊢ (((𝑥(+g‘𝑆)𝑦) ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥(+g‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {(𝑥(+g‘𝑆)𝑦)}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
85 | 83, 69, 84 | syl2anc 587 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {(𝑥(+g‘𝑆)𝑦)}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
86 | 68, 71, 73 | ofc12 7452 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f
(+g‘𝑆)((Base‘𝑀) × {𝑦})) = ((Base‘𝑀) × {(𝑥(+g‘𝑆)𝑦)})) |
87 | 86 | oveq1d 7185 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((((Base‘𝑀) × {𝑥}) ∘f
(+g‘𝑆)((Base‘𝑀) × {𝑦})) ∘f (
·𝑠 ‘𝑀)𝑧) = (((Base‘𝑀) × {(𝑥(+g‘𝑆)𝑦)}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
88 | 85, 87 | eqtr4d 2776 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = ((((Base‘𝑀) × {𝑥}) ∘f
(+g‘𝑆)((Base‘𝑀) × {𝑦})) ∘f (
·𝑠 ‘𝑀)𝑧)) |
89 | 51 | 3adant3r2 1184 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
90 | | eleq1w 2815 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (Base‘𝑆) ↔ 𝑦 ∈ (Base‘𝑆))) |
91 | 90 | 3anbi2d 1442 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) ↔ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)))) |
92 | | oveq1 7177 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥( ·𝑠
‘𝐴)𝑧) = (𝑦( ·𝑠
‘𝐴)𝑧)) |
93 | 92 | eleq1d 2817 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀) ↔ (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀))) |
94 | 91, 93 | imbi12d 348 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) ↔ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)))) |
95 | 94, 51 | chvarvv 2010 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
96 | 95 | 3adant3r1 1183 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
97 | 1, 2, 30, 31 | mendplusg 40583 |
. . . . 5
⊢ (((𝑥(
·𝑠 ‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀) ∧ (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → ((𝑥( ·𝑠
‘𝐴)𝑧)(+g‘𝐴)(𝑦( ·𝑠
‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑧) ∘f
(+g‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧))) |
98 | 89, 96, 97 | syl2anc 587 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑧)(+g‘𝐴)(𝑦( ·𝑠
‘𝐴)𝑧)) = ((𝑥( ·𝑠
‘𝐴)𝑧) ∘f
(+g‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧))) |
99 | 71, 69, 42 | syl2anc 587 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
100 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 40588 |
. . . . . 6
⊢ ((𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑦}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
101 | 73, 69, 100 | syl2anc 587 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑦}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
102 | 99, 101 | oveq12d 7188 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑧) ∘f
(+g‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧)) = ((((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧) ∘f
(+g‘𝑀)(((Base‘𝑀) × {𝑦}) ∘f (
·𝑠 ‘𝑀)𝑧))) |
103 | 98, 102 | eqtrd 2773 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑧)(+g‘𝐴)(𝑦( ·𝑠
‘𝐴)𝑧)) = ((((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧) ∘f
(+g‘𝑀)(((Base‘𝑀) × {𝑦}) ∘f (
·𝑠 ‘𝑀)𝑧))) |
104 | 80, 88, 103 | 3eqtr4d 2783 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(+g‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = ((𝑥( ·𝑠
‘𝐴)𝑧)(+g‘𝐴)(𝑦( ·𝑠
‘𝐴)𝑧))) |
105 | | ovexd 7205 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → (𝑥(.r‘𝑆)𝑦) ∈ V) |
106 | 70 | ffvelrnda 6861 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → (𝑧‘𝑘) ∈ (Base‘𝑀)) |
107 | | fconstmpt 5585 |
. . . . 5
⊢
((Base‘𝑀)
× {(𝑥(.r‘𝑆)𝑦)}) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑥(.r‘𝑆)𝑦)) |
108 | 107 | a1i 11 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {(𝑥(.r‘𝑆)𝑦)}) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑥(.r‘𝑆)𝑦))) |
109 | 70 | feqmptd 6737 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 = (𝑘 ∈ (Base‘𝑀) ↦ (𝑧‘𝑘))) |
110 | 68, 105, 106, 108, 109 | offval2 7444 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {(𝑥(.r‘𝑆)𝑦)}) ∘f (
·𝑠 ‘𝑀)𝑧) = (𝑘 ∈ (Base‘𝑀) ↦ ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘)))) |
111 | | eqid 2738 |
. . . . . 6
⊢
(.r‘𝑆) = (.r‘𝑆) |
112 | 20, 111 | ringcl 19433 |
. . . . 5
⊢ ((𝑆 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥(.r‘𝑆)𝑦) ∈ (Base‘𝑆)) |
113 | 81, 71, 73, 112 | syl3anc 1372 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥(.r‘𝑆)𝑦) ∈ (Base‘𝑆)) |
114 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 40588 |
. . . 4
⊢ (((𝑥(.r‘𝑆)𝑦) ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {(𝑥(.r‘𝑆)𝑦)}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
115 | 113, 69, 114 | syl2anc 587 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {(𝑥(.r‘𝑆)𝑦)}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
116 | 71 | adantr 484 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑆)) |
117 | | ovexd 7205 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → (𝑦( ·𝑠
‘𝑀)(𝑧‘𝑘)) ∈ V) |
118 | | fconstmpt 5585 |
. . . . . 6
⊢
((Base‘𝑀)
× {𝑥}) = (𝑘 ∈ (Base‘𝑀) ↦ 𝑥) |
119 | 118 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}) = (𝑘 ∈ (Base‘𝑀) ↦ 𝑥)) |
120 | | simplr2 1217 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → 𝑦 ∈ (Base‘𝑆)) |
121 | | fconstmpt 5585 |
. . . . . . . 8
⊢
((Base‘𝑀)
× {𝑦}) = (𝑘 ∈ (Base‘𝑀) ↦ 𝑦) |
122 | 121 | a1i 11 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑦}) = (𝑘 ∈ (Base‘𝑀) ↦ 𝑦)) |
123 | 68, 120, 106, 122, 109 | offval2 7444 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑦}) ∘f (
·𝑠 ‘𝑀)𝑧) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑦( ·𝑠
‘𝑀)(𝑧‘𝑘)))) |
124 | 101, 123 | eqtrd 2773 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦( ·𝑠
‘𝐴)𝑧) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑦( ·𝑠
‘𝑀)(𝑧‘𝑘)))) |
125 | 68, 116, 117, 119, 124 | offval2 7444 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧)) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘))))) |
126 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 40588 |
. . . . 5
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ (𝑦( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)(𝑦(
·𝑠 ‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧))) |
127 | 71, 96, 126 | syl2anc 587 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(
·𝑠 ‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦( ·𝑠
‘𝐴)𝑧))) |
128 | 76 | adantr 484 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → 𝑀 ∈ LMod) |
129 | 21, 5, 19, 20, 111 | lmodvsass 19778 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ (𝑧‘𝑘) ∈ (Base‘𝑀))) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘)) = (𝑥( ·𝑠
‘𝑀)(𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘)))) |
130 | 128, 116,
120, 106, 129 | syl13anc 1373 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑘 ∈ (Base‘𝑀)) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘)) = (𝑥( ·𝑠
‘𝑀)(𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘)))) |
131 | 130 | mpteq2dva 5125 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑘 ∈ (Base‘𝑀) ↦ ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘))) = (𝑘 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦(
·𝑠 ‘𝑀)(𝑧‘𝑘))))) |
132 | 125, 127,
131 | 3eqtr4d 2783 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(
·𝑠 ‘𝐴)𝑧)) = (𝑘 ∈ (Base‘𝑀) ↦ ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝑀)(𝑧‘𝑘)))) |
133 | 110, 115,
132 | 3eqtr4d 2783 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥(.r‘𝑆)𝑦)( ·𝑠
‘𝐴)𝑧) = (𝑥( ·𝑠
‘𝐴)(𝑦(
·𝑠 ‘𝐴)𝑧))) |
134 | 14 | adantr 484 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → 𝑆 ∈ Ring) |
135 | | eqid 2738 |
. . . . . 6
⊢
(1r‘𝑆) = (1r‘𝑆) |
136 | 20, 135 | ringidcl 19440 |
. . . . 5
⊢ (𝑆 ∈ Ring →
(1r‘𝑆)
∈ (Base‘𝑆)) |
137 | 134, 136 | syl 17 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (1r‘𝑆) ∈ (Base‘𝑆)) |
138 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 40588 |
. . . 4
⊢
(((1r‘𝑆) ∈ (Base‘𝑆) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → ((1r‘𝑆)(
·𝑠 ‘𝐴)𝑥) = (((Base‘𝑀) × {(1r‘𝑆)}) ∘f (
·𝑠 ‘𝑀)𝑥)) |
139 | 137, 138 | sylancom 591 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → ((1r‘𝑆)(
·𝑠 ‘𝐴)𝑥) = (((Base‘𝑀) × {(1r‘𝑆)}) ∘f (
·𝑠 ‘𝑀)𝑥)) |
140 | | fvexd 6689 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (Base‘𝑀) ∈ V) |
141 | 21, 21 | lmhmf 19925 |
. . . . 5
⊢ (𝑥 ∈ (𝑀 LMHom 𝑀) → 𝑥:(Base‘𝑀)⟶(Base‘𝑀)) |
142 | 141 | adantl 485 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → 𝑥:(Base‘𝑀)⟶(Base‘𝑀)) |
143 | | simpll 767 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → 𝑀 ∈ LMod) |
144 | 21, 5, 19, 135 | lmodvs1 19781 |
. . . . 5
⊢ ((𝑀 ∈ LMod ∧ 𝑦 ∈ (Base‘𝑀)) →
((1r‘𝑆)(
·𝑠 ‘𝑀)𝑦) = 𝑦) |
145 | 143, 144 | sylan 583 |
. . . 4
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) ∧ 𝑦 ∈ (Base‘𝑀)) → ((1r‘𝑆)(
·𝑠 ‘𝑀)𝑦) = 𝑦) |
146 | 140, 142,
137, 145 | caofid0l 7455 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → (((Base‘𝑀) × {(1r‘𝑆)}) ∘f (
·𝑠 ‘𝑀)𝑥) = 𝑥) |
147 | 139, 146 | eqtrd 2773 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ 𝑥 ∈ (𝑀 LMHom 𝑀)) → ((1r‘𝑆)(
·𝑠 ‘𝐴)𝑥) = 𝑥) |
148 | 3, 4, 7, 8, 9, 10,
11, 12, 14, 18, 27, 67, 104, 133, 147 | islmodd 19759 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) |