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

Metamath Proof Explorer

Theorem mendring

Proof