Metamath Proof Explorer

Theorem mendassa

Description: The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses mendassa.a ⊢ 𝐴 = ( MEndo ‘ 𝑀 )
mendassa.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
Assertion mendassa ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ CRing ) → 𝐴 ∈ AssAlg )

Proof

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