Metamath Proof Explorer

Theorem mendring

Description: The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypothesis mendassa.a ⊢ 𝐴 = ( MEndo ‘ 𝑀 )
Assertion mendring ( 𝑀 ∈ LMod → 𝐴 ∈ Ring )

Proof

Step Hyp Ref Expression
1 mendassa.a ⊢ 𝐴 = ( MEndo ‘ 𝑀 )
2 1 mendbas ⊢ ( 𝑀 LMHom 𝑀 ) = ( Base ‘ 𝐴 )
3 2 a1i ⊢ ( 𝑀 ∈ LMod → ( 𝑀 LMHom 𝑀 ) = ( Base ‘ 𝐴 ) )
4 eqidd ⊢ ( 𝑀 ∈ LMod → ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 ) )
5 eqidd ⊢ ( 𝑀 ∈ LMod → ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 ) )
6 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
7 eqid ⊢ ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 )
8 1 2 6 7 mendplusg ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) )
9 6 lmhmplusg ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) )
10 8 9 eqeltrd ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) )
11 10 3adant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) )
12 simpr1 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) )
13 simpr2 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) )
14 12 13 9 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) )
15 simpr3 ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) )
16 1 2 6 7 mendplusg ⊢ ( ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘f ( +g ‘ 𝑀 ) 𝑧 ) )
17 14 15 16 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘f ( +g ‘ 𝑀 ) 𝑧 ) )
18 12 13 8 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) )
19 18 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ( +g ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝐴 ) 𝑧 ) )
20 6 lmhmplusg ⊢ ( ( 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) )
21 13 15 20 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) )
22 1 2 6 7 mendplusg ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝐴 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) = ( 𝑥 ∘f ( +g ‘ 𝑀 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
23 12 21 22 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( +g ‘ 𝐴 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) = ( 𝑥 ∘f ( +g ‘ 𝑀 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
24 1 2 6 7 mendplusg ⊢ ( ( 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) = ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) )
25 13 15 24 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) = ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) )
26 25 oveq2d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( +g ‘ 𝐴 ) ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) ) = ( 𝑥 ( +g ‘ 𝐴 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
27 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
28 grpmnd ⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd )
29 27 28 syl ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
30 29 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑀 ∈ Mnd )
31 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
32 31 31 lmhmf ⊢ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) → 𝑥 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
33 12 32 syl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑥 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
34 fvex ⊢ ( Base ‘ 𝑀 ) ∈ V
35 34 34 elmap ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ↔ 𝑥 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
36 33 35 sylibr ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑥 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) )
37 31 31 lmhmf ⊢ ( 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) → 𝑦 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
38 13 37 syl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑦 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
39 34 34 elmap ⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ↔ 𝑦 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
40 38 39 sylibr ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑦 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) )
41 31 31 lmhmf ⊢ ( 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) → 𝑧 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
42 15 41 syl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑧 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
43 34 34 elmap ⊢ ( 𝑧 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ↔ 𝑧 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
44 42 43 sylibr ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑧 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) )
45 31 6 mndvass ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘f ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ∘f ( +g ‘ 𝑀 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
46 30 36 40 44 45 syl13anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘f ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ∘f ( +g ‘ 𝑀 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
47 23 26 46 3eqtr4d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( +g ‘ 𝐴 ) ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) ) = ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘f ( +g ‘ 𝑀 ) 𝑧 ) )
48 17 19 47 3eqtr4d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ( +g ‘ 𝐴 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐴 ) ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) ) )
49 id ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ LMod )
50 eqidd ⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 ) )
51 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
52 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
53 51 31 52 52 0lmhm ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑀 ∈ LMod ∧ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 ) ) → ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ∈ ( 𝑀 LMHom 𝑀 ) )
54 49 49 50 53 syl3anc ⊢ ( 𝑀 ∈ LMod → ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ∈ ( 𝑀 LMHom 𝑀 ) )
55 1 2 6 7 mendplusg ⊢ ( ( ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ( +g ‘ 𝐴 ) 𝑥 ) = ( ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ∘f ( +g ‘ 𝑀 ) 𝑥 ) )
56 54 55 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ( +g ‘ 𝐴 ) 𝑥 ) = ( ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ∘f ( +g ‘ 𝑀 ) 𝑥 ) )
57 32 35 sylibr ⊢ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) → 𝑥 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) )
58 31 6 51 mndvlid ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑥 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ) → ( ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ∘f ( +g ‘ 𝑀 ) 𝑥 ) = 𝑥 )
59 29 57 58 syl2an ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ∘f ( +g ‘ 𝑀 ) 𝑥 ) = 𝑥 )
60 56 59 eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) ( +g ‘ 𝐴 ) 𝑥 ) = 𝑥 )
61 eqid ⊢ ( invg ‘ 𝑀 ) = ( invg ‘ 𝑀 )
62 61 invlmhm ⊢ ( 𝑀 ∈ LMod → ( invg ‘ 𝑀 ) ∈ ( 𝑀 LMHom 𝑀 ) )
63 lmhmco ⊢ ( ( ( invg ‘ 𝑀 ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ∈ ( 𝑀 LMHom 𝑀 ) )
64 62 63 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ∈ ( 𝑀 LMHom 𝑀 ) )
65 1 2 6 7 mendplusg ⊢ ( ( ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ( +g ‘ 𝐴 ) 𝑥 ) = ( ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ∘f ( +g ‘ 𝑀 ) 𝑥 ) )
66 64 65 sylancom ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ( +g ‘ 𝐴 ) 𝑥 ) = ( ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ∘f ( +g ‘ 𝑀 ) 𝑥 ) )
67 31 6 61 51 grpvlinv ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑥 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ) → ( ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ∘f ( +g ‘ 𝑀 ) 𝑥 ) = ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) )
68 27 57 67 syl2an ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ∘f ( +g ‘ 𝑀 ) 𝑥 ) = ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) )
69 66 68 eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( ( invg ‘ 𝑀 ) ∘ 𝑥 ) ( +g ‘ 𝐴 ) 𝑥 ) = ( ( Base ‘ 𝑀 ) × { ( 0g ‘ 𝑀 ) } ) )
70 3 4 11 48 54 60 64 69 isgrpd ⊢ ( 𝑀 ∈ LMod → 𝐴 ∈ Grp )
71 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
72 1 2 71 mendmulr ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
73 lmhmco ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ∘ 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) )
74 72 73 eqeltrd ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) )
75 74 3adant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) )
76 coass ⊢ ( ( 𝑥 ∘ 𝑦 ) ∘ 𝑧 ) = ( 𝑥 ∘ ( 𝑦 ∘ 𝑧 ) )
77 12 13 72 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
78 77 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘ 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) )
79 12 13 73 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ∘ 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) )
80 1 2 71 mendmulr ⊢ ( ( ( 𝑥 ∘ 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( 𝑥 ∘ 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘ 𝑦 ) ∘ 𝑧 ) )
81 79 15 80 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ∘ 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘ 𝑦 ) ∘ 𝑧 ) )
82 78 81 eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘ 𝑦 ) ∘ 𝑧 ) )
83 1 2 71 mendmulr ⊢ ( ( 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑧 ) = ( 𝑦 ∘ 𝑧 ) )
84 13 15 83 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑧 ) = ( 𝑦 ∘ 𝑧 ) )
85 84 oveq2d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( .r ‘ 𝐴 ) 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ∘ 𝑧 ) ) )
86 lmhmco ⊢ ( ( 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑦 ∘ 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) )
87 13 15 86 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑦 ∘ 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) )
88 1 2 71 mendmulr ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ ( 𝑦 ∘ 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ∘ 𝑧 ) ) = ( 𝑥 ∘ ( 𝑦 ∘ 𝑧 ) ) )
89 12 87 88 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ∘ 𝑧 ) ) = ( 𝑥 ∘ ( 𝑦 ∘ 𝑧 ) ) )
90 85 89 eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( .r ‘ 𝐴 ) 𝑧 ) ) = ( 𝑥 ∘ ( 𝑦 ∘ 𝑧 ) ) )
91 76 82 90 3eqtr4a ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( .r ‘ 𝐴 ) 𝑧 ) ) )
92 1 2 71 mendmulr ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) = ( 𝑥 ∘ ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
93 12 21 92 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) = ( 𝑥 ∘ ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
94 25 oveq2d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
95 lmhmco ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ∘ 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) )
96 12 15 95 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ∘ 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) )
97 1 2 6 7 mendplusg ⊢ ( ( ( 𝑥 ∘ 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ ( 𝑥 ∘ 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( 𝑥 ∘ 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ∘ 𝑧 ) ) = ( ( 𝑥 ∘ 𝑦 ) ∘f ( +g ‘ 𝑀 ) ( 𝑥 ∘ 𝑧 ) ) )
98 79 96 97 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ∘ 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ∘ 𝑧 ) ) = ( ( 𝑥 ∘ 𝑦 ) ∘f ( +g ‘ 𝑀 ) ( 𝑥 ∘ 𝑧 ) ) )
99 1 2 71 mendmulr ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑧 ) = ( 𝑥 ∘ 𝑧 ) )
100 12 15 99 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑧 ) = ( 𝑥 ∘ 𝑧 ) )
101 77 100 oveq12d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) 𝑧 ) ) = ( ( 𝑥 ∘ 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ∘ 𝑧 ) ) )
102 lmghm ⊢ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) → 𝑥 ∈ ( 𝑀 GrpHom 𝑀 ) )
103 ghmmhm ⊢ ( 𝑥 ∈ ( 𝑀 GrpHom 𝑀 ) → 𝑥 ∈ ( 𝑀 MndHom 𝑀 ) )
104 12 102 103 3syl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑥 ∈ ( 𝑀 MndHom 𝑀 ) )
105 31 6 6 mhmvlin ⊢ ( ( 𝑥 ∈ ( 𝑀 MndHom 𝑀 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ∧ 𝑧 ∈ ( ( Base ‘ 𝑀 ) ↑m ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ∘ ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) = ( ( 𝑥 ∘ 𝑦 ) ∘f ( +g ‘ 𝑀 ) ( 𝑥 ∘ 𝑧 ) ) )
106 104 40 44 105 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ∘ ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) = ( ( 𝑥 ∘ 𝑦 ) ∘f ( +g ‘ 𝑀 ) ( 𝑥 ∘ 𝑧 ) ) )
107 98 101 106 3eqtr4d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) 𝑧 ) ) = ( 𝑥 ∘ ( 𝑦 ∘f ( +g ‘ 𝑀 ) 𝑧 ) ) )
108 93 94 107 3eqtr4d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( 𝑦 ( +g ‘ 𝐴 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ( +g ‘ 𝐴 ) ( 𝑥 ( .r ‘ 𝐴 ) 𝑧 ) ) )
109 1 2 71 mendmulr ⊢ ( ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘ 𝑧 ) )
110 14 15 109 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘ 𝑧 ) )
111 18 oveq1d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) )
112 1 2 6 7 mendplusg ⊢ ( ( ( 𝑥 ∘ 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ ( 𝑦 ∘ 𝑧 ) ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( 𝑥 ∘ 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ∘ 𝑧 ) ) = ( ( 𝑥 ∘ 𝑧 ) ∘f ( +g ‘ 𝑀 ) ( 𝑦 ∘ 𝑧 ) ) )
113 96 87 112 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ∘ 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ∘ 𝑧 ) ) = ( ( 𝑥 ∘ 𝑧 ) ∘f ( +g ‘ 𝑀 ) ( 𝑦 ∘ 𝑧 ) ) )
114 100 84 oveq12d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ( .r ‘ 𝐴 ) 𝑧 ) ) = ( ( 𝑥 ∘ 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ∘ 𝑧 ) ) )
115 ffn ⊢ ( 𝑥 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) → 𝑥 Fn ( Base ‘ 𝑀 ) )
116 12 32 115 3syl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑥 Fn ( Base ‘ 𝑀 ) )
117 ffn ⊢ ( 𝑦 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) → 𝑦 Fn ( Base ‘ 𝑀 ) )
118 13 37 117 3syl ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → 𝑦 Fn ( Base ‘ 𝑀 ) )
119 34 a1i ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( Base ‘ 𝑀 ) ∈ V )
120 inidm ⊢ ( ( Base ‘ 𝑀 ) ∩ ( Base ‘ 𝑀 ) ) = ( Base ‘ 𝑀 )
121 116 118 42 119 119 119 120 ofco ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘ 𝑧 ) = ( ( 𝑥 ∘ 𝑧 ) ∘f ( +g ‘ 𝑀 ) ( 𝑦 ∘ 𝑧 ) ) )
122 113 114 121 3eqtr4d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ( .r ‘ 𝐴 ) 𝑧 ) ) = ( ( 𝑥 ∘f ( +g ‘ 𝑀 ) 𝑦 ) ∘ 𝑧 ) )
123 110 111 122 3eqtr4d ⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑦 ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑧 ∈ ( 𝑀 LMHom 𝑀 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ( .r ‘ 𝐴 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝐴 ) 𝑧 ) ( +g ‘ 𝐴 ) ( 𝑦 ( .r ‘ 𝐴 ) 𝑧 ) ) )
124 31 idlmhm ⊢ ( 𝑀 ∈ LMod → ( I ↾ ( Base ‘ 𝑀 ) ) ∈ ( 𝑀 LMHom 𝑀 ) )
125 1 2 71 mendmulr ⊢ ( ( ( I ↾ ( Base ‘ 𝑀 ) ) ∈ ( 𝑀 LMHom 𝑀 ) ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( I ↾ ( Base ‘ 𝑀 ) ) ( .r ‘ 𝐴 ) 𝑥 ) = ( ( I ↾ ( Base ‘ 𝑀 ) ) ∘ 𝑥 ) )
126 124 125 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( I ↾ ( Base ‘ 𝑀 ) ) ( .r ‘ 𝐴 ) 𝑥 ) = ( ( I ↾ ( Base ‘ 𝑀 ) ) ∘ 𝑥 ) )
127 32 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → 𝑥 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) )
128 fcoi2 ⊢ ( 𝑥 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) → ( ( I ↾ ( Base ‘ 𝑀 ) ) ∘ 𝑥 ) = 𝑥 )
129 127 128 syl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( I ↾ ( Base ‘ 𝑀 ) ) ∘ 𝑥 ) = 𝑥 )
130 126 129 eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( ( I ↾ ( Base ‘ 𝑀 ) ) ( .r ‘ 𝐴 ) 𝑥 ) = 𝑥 )
131 id ⊢ ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) → 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) )
132 1 2 71 mendmulr ⊢ ( ( 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ∧ ( I ↾ ( Base ‘ 𝑀 ) ) ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( I ↾ ( Base ‘ 𝑀 ) ) ) = ( 𝑥 ∘ ( I ↾ ( Base ‘ 𝑀 ) ) ) )
133 131 124 132 syl2anr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( I ↾ ( Base ‘ 𝑀 ) ) ) = ( 𝑥 ∘ ( I ↾ ( Base ‘ 𝑀 ) ) ) )
134 fcoi1 ⊢ ( 𝑥 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑀 ) → ( 𝑥 ∘ ( I ↾ ( Base ‘ 𝑀 ) ) ) = 𝑥 )
135 127 134 syl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ∘ ( I ↾ ( Base ‘ 𝑀 ) ) ) = 𝑥 )
136 133 135 eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( 𝑀 LMHom 𝑀 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) ( I ↾ ( Base ‘ 𝑀 ) ) ) = 𝑥 )
137 3 4 5 70 75 91 108 123 124 130 136 isringd ⊢ ( 𝑀 ∈ LMod → 𝐴 ∈ Ring )