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