Step | Hyp | Ref
| Expression |
1 | | mendassa.a |
. . . 4
⊢ 𝐴 = (MEndo‘𝑀) |
2 | 1 | mendbas 36773 |
. . 3
⊢ (𝑀 LMHom 𝑀) = (Base‘𝐴) |
3 | 2 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (𝑀 LMHom 𝑀) = (Base‘𝐴)) |
4 | | mendassa.s |
. . . 4
⊢ 𝑆 = (Scalar‘𝑀) |
5 | 1, 4 | mendsca 36778 |
. . 3
⊢ 𝑆 = (Scalar‘𝐴) |
6 | 5 | a1i 11 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 = (Scalar‘𝐴)) |
7 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(Base‘𝑆) =
(Base‘𝑆)) |
8 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴)) |
9 | | eqidd 2611 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) →
(.r‘𝐴) =
(.r‘𝐴)) |
10 | 1, 4 | mendlmod 36782 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ LMod) |
11 | 1 | mendring 36781 |
. . 3
⊢ (𝑀 ∈ LMod → 𝐴 ∈ Ring) |
12 | 11 | adantr 480 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ Ring) |
13 | | simpr 476 |
. 2
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝑆 ∈ CRing) |
14 | | simpr3 1062 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 ∈ (𝑀 LMHom 𝑀)) |
15 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑀) =
(Base‘𝑀) |
16 | 15, 15 | lmhmf 18855 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑀 LMHom 𝑀) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
17 | 14, 16 | syl 17 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) |
18 | 17 | ffvelrnda 6267 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑧‘𝑣) ∈ (Base‘𝑀)) |
19 | 17 | feqmptd 6159 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑧 = (𝑣 ∈ (Base‘𝑀) ↦ (𝑧‘𝑣))) |
20 | | simpr1 1060 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑥 ∈ (Base‘𝑆)) |
21 | | simpr2 1061 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
22 | | eqid 2610 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝑀) = ( ·𝑠
‘𝑀) |
23 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
24 | | eqid 2610 |
. . . . . . . 8
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘𝐴) |
25 | 1, 22, 2, 4, 23, 15, 24 | mendvsca 36780 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) |
26 | 20, 21, 25 | syl2anc 691 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦)) |
27 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝑀)
∈ V |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (Base‘𝑀) ∈ V) |
29 | | simplr1 1096 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑤 ∈ (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑆)) |
30 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑦‘𝑤) ∈ V |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑤 ∈ (Base‘𝑀)) → (𝑦‘𝑤) ∈ V) |
32 | | fconstmpt 5085 |
. . . . . . . 8
⊢
((Base‘𝑀)
× {𝑥}) = (𝑤 ∈ (Base‘𝑀) ↦ 𝑥) |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}) = (𝑤 ∈ (Base‘𝑀) ↦ 𝑥)) |
34 | 15, 15 | lmhmf 18855 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑀 LMHom 𝑀) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
35 | 21, 34 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦:(Base‘𝑀)⟶(Base‘𝑀)) |
36 | 35 | feqmptd 6159 |
. . . . . . 7
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝑦 = (𝑤 ∈ (Base‘𝑀) ↦ (𝑦‘𝑤))) |
37 | 28, 29, 31, 33, 36 | offval2 6812 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑦) = (𝑤 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)))) |
38 | 26, 37 | eqtrd 2644 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) = (𝑤 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)))) |
39 | | fveq2 6103 |
. . . . . 6
⊢ (𝑤 = (𝑧‘𝑣) → (𝑦‘𝑤) = (𝑦‘(𝑧‘𝑣))) |
40 | 39 | oveq2d 6565 |
. . . . 5
⊢ (𝑤 = (𝑧‘𝑣) → (𝑥( ·𝑠
‘𝑀)(𝑦‘𝑤)) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
41 | 18, 19, 38, 40 | fmptco 6303 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
42 | | simplr1 1096 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑥 ∈ (Base‘𝑆)) |
43 | | fvex 6113 |
. . . . . 6
⊢ (𝑦‘(𝑧‘𝑣)) ∈ V |
44 | 43 | a1i 11 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑦‘(𝑧‘𝑣)) ∈ V) |
45 | | fconstmpt 5085 |
. . . . . 6
⊢
((Base‘𝑀)
× {𝑥}) = (𝑣 ∈ (Base‘𝑀) ↦ 𝑥) |
46 | 45 | a1i 11 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((Base‘𝑀) × {𝑥}) = (𝑣 ∈ (Base‘𝑀) ↦ 𝑥)) |
47 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘𝐴) = (.r‘𝐴) |
48 | 1, 2, 47 | mendmulr 36777 |
. . . . . . 7
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)𝑧) = (𝑦 ∘ 𝑧)) |
49 | 21, 14, 48 | syl2anc 691 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) = (𝑦 ∘ 𝑧)) |
50 | | fcompt 6306 |
. . . . . . 7
⊢ ((𝑦:(Base‘𝑀)⟶(Base‘𝑀) ∧ 𝑧:(Base‘𝑀)⟶(Base‘𝑀)) → (𝑦 ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
51 | 35, 17, 50 | syl2anc 691 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ 𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
52 | 49, 51 | eqtrd 2644 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑧‘𝑣)))) |
53 | 28, 42, 44, 46, 52 | offval2 6812 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧)) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
54 | 41, 53 | eqtr4d 2647 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
55 | 10 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝐴 ∈ LMod) |
56 | 2, 5, 24, 23 | lmodvscl 18703 |
. . . . 5
⊢ ((𝐴 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
57 | 55, 20, 21, 56 | syl3anc 1318 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀)) |
58 | 1, 2, 47 | mendmulr 36777 |
. . . 4
⊢ (((𝑥(
·𝑠 ‘𝐴)𝑦) ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧)) |
59 | 57, 14, 58 | syl2anc 691 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = ((𝑥( ·𝑠
‘𝐴)𝑦) ∘ 𝑧)) |
60 | 12 | adantr 480 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → 𝐴 ∈ Ring) |
61 | 2, 47 | ringcl 18384 |
. . . . 5
⊢ ((𝐴 ∈ Ring ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
62 | 60, 21, 14, 61 | syl3anc 1318 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
63 | 1, 22, 2, 4, 23, 15, 24 | mendvsca 36780 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ (𝑦(.r‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
64 | 20, 62, 63 | syl2anc 691 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
65 | 54, 59, 64 | 3eqtr4d 2654 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → ((𝑥( ·𝑠
‘𝐴)𝑦)(.r‘𝐴)𝑧) = (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧))) |
66 | | simplr2 1097 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑦 ∈ (𝑀 LMHom 𝑀)) |
67 | 4, 23, 15, 22, 22 | lmhmlin 18856 |
. . . . . 6
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑥 ∈ (Base‘𝑆) ∧ (𝑧‘𝑣) ∈ (Base‘𝑀)) → (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
68 | 66, 42, 18, 67 | syl3anc 1318 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))) = (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣)))) |
69 | 68 | mpteq2dva 4672 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑦‘(𝑧‘𝑣))))) |
70 | | simplll 794 |
. . . . . 6
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → 𝑀 ∈ LMod) |
71 | 15, 4, 22, 23 | lmodvscl 18703 |
. . . . . 6
⊢ ((𝑀 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ (𝑧‘𝑣) ∈ (Base‘𝑀)) → (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) ∈ (Base‘𝑀)) |
72 | 70, 42, 18, 71 | syl3anc 1318 |
. . . . 5
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) ∈ (Base‘𝑀)) |
73 | 1, 22, 2, 4, 23, 15, 24 | mendvsca 36780 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
74 | 20, 14, 73 | syl2anc 691 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧)) |
75 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑧‘𝑣) ∈ V |
76 | 75 | a1i 11 |
. . . . . . 7
⊢ ((((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) ∧ 𝑣 ∈ (Base‘𝑀)) → (𝑧‘𝑣) ∈ V) |
77 | 28, 42, 76, 46, 19 | offval2 6812 |
. . . . . 6
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
78 | 74, 77 | eqtrd 2644 |
. . . . 5
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
79 | | fveq2 6103 |
. . . . 5
⊢ (𝑤 = (𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)) → (𝑦‘𝑤) = (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣)))) |
80 | 72, 78, 36, 79 | fmptco 6303 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑣 ∈ (Base‘𝑀) ↦ (𝑦‘(𝑥( ·𝑠
‘𝑀)(𝑧‘𝑣))))) |
81 | 69, 80, 53 | 3eqtr4d 2654 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧)) = (((Base‘𝑀) × {𝑥}) ∘𝑓 (
·𝑠 ‘𝑀)(𝑦(.r‘𝐴)𝑧))) |
82 | 2, 5, 24, 23 | lmodvscl 18703 |
. . . . 5
⊢ ((𝐴 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑆) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀)) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
83 | 55, 20, 14, 82 | syl3anc 1318 |
. . . 4
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) |
84 | 1, 2, 47 | mendmulr 36777 |
. . . 4
⊢ ((𝑦 ∈ (𝑀 LMHom 𝑀) ∧ (𝑥( ·𝑠
‘𝐴)𝑧) ∈ (𝑀 LMHom 𝑀)) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧))) |
85 | 21, 83, 84 | syl2anc 691 |
. . 3
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑦 ∘ (𝑥( ·𝑠
‘𝐴)𝑧))) |
86 | 81, 85, 64 | 3eqtr4d 2654 |
. 2
⊢ (((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) ∧ (𝑥 ∈ (Base‘𝑆) ∧ 𝑦 ∈ (𝑀 LMHom 𝑀) ∧ 𝑧 ∈ (𝑀 LMHom 𝑀))) → (𝑦(.r‘𝐴)(𝑥( ·𝑠
‘𝐴)𝑧)) = (𝑥( ·𝑠
‘𝐴)(𝑦(.r‘𝐴)𝑧))) |
87 | 3, 6, 7, 8, 9, 10,
12, 13, 65, 86 | isassad 19144 |
1
⊢ ((𝑀 ∈ LMod ∧ 𝑆 ∈ CRing) → 𝐴 ∈ AssAlg) |