mendring

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

		Ref	Expression
	Hypothesis	mendassa.a	$⊢ A = MEndo (M)$
	Assertion	mendring	$⊢ M \in LMod \to A \in Ring$

Proof

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

Metamath Proof Explorer

Theorem mendring

Proof