Step | Hyp | Ref
| Expression |
1 | | mendassa.a |
. . . 4
⊢ 𝐴 = (MEndo‘𝑀) |
2 | 1 | mendbas 41697 |
. . 3
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
3 | 2 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (𝑀 LMHom 𝑀) = (Base‘𝐴)) |
4 | | mendassa.s |
. . . 4
⊢ 𝑆 = (Scalar‘𝑀) |
5 | 1, 4 | mendsca 41702 |
. . 3
⊢ 𝑆 = (Scalar‘𝐴) |
6 | 5 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 = (Scalar‘𝐴)) |
7 | | eqidd 2732 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(Base‘𝑆) =
(Base‘𝑆)) |
8 | | eqidd 2732 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴)) |
9 | | eqidd 2732 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(.r‘𝐴) =
(.r‘𝐴)) |
10 | 1, 4 | mendlmod 41706 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) |
11 | 1 | mendring 41705 |
. . 3
⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) |
12 | 11 | adantr 481 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ Ring) |
13 | | simpr3 1196 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ (𝑀 LMHom 𝑀)) |
14 | | eqid 2731 |
. . . . . . . 8
⊢
(Base‘𝑀) =
(Base‘𝑀) |
15 | 14, 14 | lmhmf 20594 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑀 LMHom 𝑀) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
16 | 13, 15 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
17 | 16 | ffvelcdmda 7071 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑧‘𝑣) ∈ (Base‘𝑀)) |
18 | 16 | feqmptd 6946 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 = (𝑣 ∈ (Base‘𝑀) ↦ (𝑧‘𝑣))) |
19 | | simpr1 1194 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (Base‘𝑆)) |
20 | | simpr2 1195 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
21 | | eqid 2731 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
22 | | eqid 2731 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
23 | | eqid 2731 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
24 | 1, 21, 2, 4, 22, 14, 23 | mendvsca 41704 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
25 | 19, 20, 24 | syl2anc 584 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦)) |
26 | | fvexd 6893 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (Base‘𝑀) ∈ V) |
27 | | simplr1 1215 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑤 ∈ (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑆)) |
28 | | fvexd 6893 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑤 ∈ (Base‘𝑀)) → (𝑦‘𝑤) ∈ V) |
29 | | fconstmpt 5730 |
. . . . . . . 8
⊢
((Base‘𝑀)
× {𝑥}) = (𝑤 ∈ (Base‘𝑀) ↦ 𝑥) |
30 | 29 | a1i 11 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}) = (𝑤 ∈ (Base‘𝑀) ↦ 𝑥)) |
31 | 14, 14 | lmhmf 20594 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑀 LMHom 𝑀) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
32 | 20, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
33 | 32 | feqmptd 6946 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 = (𝑤 ∈ (Base‘𝑀) ↦ (𝑦‘𝑤))) |
34 | 26, 27, 28, 30, 33 | offval2 7673 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑦) = (𝑤 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)))) |
35 | 25, 34 | eqtrd 2771 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (𝑤 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)))) |
36 | | fveq2 6878 |
. . . . . 6
⊢ (𝑤 = (𝑧‘𝑣) → (𝑦‘𝑤) = (𝑦‘(𝑧‘𝑣))) |
37 | 36 | oveq2d 7409 |
. . . . 5
⊢ (𝑤 = (𝑧‘𝑣) → (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
38 | 17, 18, 35, 37 | fmptco 7111 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
39 | | simplr1 1215 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑆)) |
40 | | fvexd 6893 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑦‘(𝑧‘𝑣)) ∈ V) |
41 | | fconstmpt 5730 |
. . . . . 6
⊢
((Base‘𝑀)
× {𝑥}) = (𝑣 ∈ (Base‘𝑀) ↦ 𝑥) |
42 | 41 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}) = (𝑣 ∈ (Base‘𝑀) ↦ 𝑥)) |
43 | | eqid 2731 |
. . . . . . . 8
⊢
(.r‘𝐴) = (.r‘𝐴) |
44 | 1, 2, 43 | mendmulr 41701 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)𝑧) = (𝑦 ∘ 𝑧)) |
45 | 20, 13, 44 | syl2anc 584 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) = (𝑦 ∘ 𝑧)) |
46 | | fcompt 7115 |
. . . . . . 7
⊢ ((𝑦:(Base‘𝑀)⟶(Base‘𝑀) ∧ 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) → (𝑦 ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
47 | 32, 16, 46 | syl2anc 584 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
48 | 45, 47 | eqtrd 2771 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
49 | 26, 39, 40, 42, 48 | offval2 7673 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧)) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
50 | 38, 49 | eqtr4d 2774 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
51 | 10 | adantr 481 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝐴 ∈ LMod) |
52 | 2, 5, 23, 22 | lmodvscl 20438 |
. . . . 5
⊢ ((𝐴 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
53 | 51, 19, 20, 52 | syl3anc 1371 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
54 | 1, 2, 43 | mendmulr 41701 |
. . . 4
⊢ (((𝑥(
·𝑠 ‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧)) |
55 | 53, 13, 54 | syl2anc 584 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧)) |
56 | 12 | adantr 481 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝐴 ∈ Ring) |
57 | 2, 43 | ringcl 20031 |
. . . . 5
⊢ ((𝐴 ∈ Ring ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
58 | 56, 20, 13, 57 | syl3anc 1371 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
59 | 1, 21, 2, 4, 22, 14, 23 | mendvsca 41704 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
60 | 19, 58, 59 | syl2anc 584 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
61 | 50, 55, 60 | 3eqtr4d 2781 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧))) |
62 | | simplr2 1216 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
63 | 4, 22, 14, 21, 21 | lmhmlin 20595 |
. . . . . 6
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑥 ∈ (Base‘𝑆) ∧ (𝑧‘𝑣) ∈ (Base‘𝑀)) → (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
64 | 62, 39, 17, 63 | syl3anc 1371 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
65 | 64 | mpteq2dva 5241 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
66 | | simplll 773 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑀 ∈ LMod) |
67 | 14, 4, 21, 22 | lmodvscl 20438 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ (𝑧‘𝑣) ∈ (Base‘𝑀)) → (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) ∈ (Base‘𝑀)) |
68 | 66, 39, 17, 67 | syl3anc 1371 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) ∈ (Base‘𝑀)) |
69 | 1, 21, 2, 4, 22, 14, 23 | mendvsca 41704 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
70 | 19, 13, 69 | syl2anc 584 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧)) |
71 | | fvexd 6893 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑧‘𝑣) ∈ V) |
72 | 26, 39, 71, 42, 18 | offval2 7673 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
73 | 70, 72 | eqtrd 2771 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
74 | | fveq2 6878 |
. . . . 5
⊢ (𝑤 = (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) → (𝑦‘𝑤) = (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
75 | 68, 73, 33, 74 | fmptco 7111 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))))) |
76 | 65, 75, 49 | 3eqtr4d 2781 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘f (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
77 | 2, 5, 23, 22 | lmodvscl 20438 |
. . . . 5
⊢ ((𝐴 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
78 | 51, 19, 13, 77 | syl3anc 1371 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
79 | 1, 2, 43 | mendmulr 41701 |
. . . 4
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧))) |
80 | 20, 78, 79 | syl2anc 584 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧))) |
81 | 76, 80, 60 | 3eqtr4d 2781 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧))) |
82 | 3, 6, 7, 8, 9, 10,
12, 61, 81 | isassad 21352 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg) |