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