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 | | mendassa.s |
. . . 4
⊢ 𝑆 = (Scalar‘𝑀) |
5 | 1, 4 | mendsca 40586 |
. . 3
⊢ 𝑆 = (Scalar‘𝐴) |
6 | 5 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 = (Scalar‘𝐴)) |
7 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(Base‘𝑆) =
(Base‘𝑆)) |
8 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴)) |
9 | | eqidd 2739 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(.r‘𝐴) =
(.r‘𝐴)) |
10 | 1, 4 | mendlmod 40590 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) |
11 | 1 | mendring 40589 |
. . 3
⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) |
12 | 11 | adantr 484 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ Ring) |
13 | | simpr 488 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 ∈ CRing) |
14 | | simpr3 1197 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ (𝑀 LMHom 𝑀)) |
15 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝑀) =
(Base‘𝑀) |
16 | 15, 15 | lmhmf 19925 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑀 LMHom 𝑀) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
17 | 14, 16 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
18 | 17 | ffvelrnda 6861 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑧‘𝑣) ∈ (Base‘𝑀)) |
19 | 17 | feqmptd 6737 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 = (𝑣 ∈ (Base‘𝑀) ↦ (𝑧‘𝑣))) |
20 | | simpr1 1195 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (Base‘𝑆)) |
21 | | simpr2 1196 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
22 | | eqid 2738 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
23 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
24 | | eqid 2738 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
25 | 1, 22, 2, 4, 23, 15, 24 | mendvsca 40588 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
26 | 20, 21, 25 | syl2anc 587 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
27 | | fvexd 6689 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (Base‘𝑀) ∈ V) |
28 | | simplr1 1216 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑤 ∈ (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑆)) |
29 | | fvexd 6689 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑤 ∈ (Base‘𝑀)) → (𝑦‘𝑤) ∈ V) |
30 | | fconstmpt 5585 |
. . . . . . . 8
⊢
((Base‘𝑀)
× {𝑥}) = (𝑤 ∈ (Base‘𝑀) ↦ 𝑥) |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}) = (𝑤 ∈ (Base‘𝑀) ↦ 𝑥)) |
32 | 15, 15 | lmhmf 19925 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑀 LMHom 𝑀) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
33 | 21, 32 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
34 | 33 | feqmptd 6737 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 = (𝑤 ∈ (Base‘𝑀) ↦ (𝑦‘𝑤))) |
35 | 27, 28, 29, 31, 34 | offval2 7444 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦) = (𝑤 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)))) |
36 | 26, 35 | eqtrd 2773 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (𝑤 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)))) |
37 | | fveq2 6674 |
. . . . . 6
⊢ (𝑤 = (𝑧‘𝑣) → (𝑦‘𝑤) = (𝑦‘(𝑧‘𝑣))) |
38 | 37 | oveq2d 7186 |
. . . . 5
⊢ (𝑤 = (𝑧‘𝑣) → (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
39 | 18, 19, 36, 38 | fmptco 6901 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
40 | | simplr1 1216 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑆)) |
41 | | fvexd 6689 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑦‘(𝑧‘𝑣)) ∈ V) |
42 | | fconstmpt 5585 |
. . . . . 6
⊢
((Base‘𝑀)
× {𝑥}) = (𝑣 ∈ (Base‘𝑀) ↦ 𝑥) |
43 | 42 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}) = (𝑣 ∈ (Base‘𝑀) ↦ 𝑥)) |
44 | | eqid 2738 |
. . . . . . . 8
⊢
(.r‘𝐴) = (.r‘𝐴) |
45 | 1, 2, 44 | mendmulr 40585 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)𝑧) = (𝑦 ∘ 𝑧)) |
46 | 21, 14, 45 | syl2anc 587 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) = (𝑦 ∘ 𝑧)) |
47 | | fcompt 6905 |
. . . . . . 7
⊢ ((𝑦:(Base‘𝑀)⟶(Base‘𝑀) ∧ 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) → (𝑦 ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
48 | 33, 17, 47 | syl2anc 587 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
49 | 46, 48 | eqtrd 2773 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
50 | 27, 40, 41, 43, 49 | offval2 7444 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧)) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
51 | 39, 50 | eqtr4d 2776 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
52 | 10 | adantr 484 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝐴 ∈ LMod) |
53 | 2, 5, 24, 23 | lmodvscl 19770 |
. . . . 5
⊢ ((𝐴 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
54 | 52, 20, 21, 53 | syl3anc 1372 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
55 | 1, 2, 44 | mendmulr 40585 |
. . . 4
⊢ (((𝑥(
·𝑠 ‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧)) |
56 | 54, 14, 55 | syl2anc 587 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧)) |
57 | 12 | adantr 484 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝐴 ∈ Ring) |
58 | 2, 44 | ringcl 19433 |
. . . . 5
⊢ ((𝐴 ∈ Ring ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
59 | 57, 21, 14, 58 | syl3anc 1372 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
60 | 1, 22, 2, 4, 23, 15, 24 | mendvsca 40588 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
61 | 20, 59, 60 | syl2anc 587 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
62 | 51, 56, 61 | 3eqtr4d 2783 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧))) |
63 | | simplr2 1217 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
64 | 4, 23, 15, 22, 22 | lmhmlin 19926 |
. . . . . 6
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑥 ∈ (Base‘𝑆) ∧ (𝑧‘𝑣) ∈ (Base‘𝑀)) → (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
65 | 63, 40, 18, 64 | syl3anc 1372 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
66 | 65 | mpteq2dva 5125 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
67 | | simplll 775 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑀 ∈ LMod) |
68 | 15, 4, 22, 23 | lmodvscl 19770 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ (𝑧‘𝑣) ∈ (Base‘𝑀)) → (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) ∈ (Base‘𝑀)) |
69 | 67, 40, 18, 68 | syl3anc 1372 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) ∈ (Base‘𝑀)) |
70 | 1, 22, 2, 4, 23, 15, 24 | mendvsca 40588 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
71 | 20, 14, 70 | syl2anc 587 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
72 | | fvexd 6689 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑧‘𝑣) ∈ V) |
73 | 27, 40, 72, 43, 19 | offval2 7444 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
74 | 71, 73 | eqtrd 2773 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
75 | | fveq2 6674 |
. . . . 5
⊢ (𝑤 = (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) → (𝑦‘𝑤) = (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
76 | 69, 74, 34, 75 | fmptco 6901 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))))) |
77 | 66, 76, 50 | 3eqtr4d 2783 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
78 | 2, 5, 24, 23 | lmodvscl 19770 |
. . . . 5
⊢ ((𝐴 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
79 | 52, 20, 14, 78 | syl3anc 1372 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
80 | 1, 2, 44 | mendmulr 40585 |
. . . 4
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧))) |
81 | 21, 79, 80 | syl2anc 587 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧))) |
82 | 77, 81, 61 | 3eqtr4d 2783 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧))) |
83 | 3, 6, 7, 8, 9, 10,
12, 13, 62, 82 | isassad 20680 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg) |