mendlmod

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

	Ref	Expression
Hypotheses	mendassa.a	$⊢ A = MEndo (M)$
	mendassa.s	$⊢ S = Scalar (M)$
Assertion	mendlmod	$⊢ (M \in LMod \land S \in CRing) \to A \in LMod$

Proof

Step	Hyp	Ref	Expression
1		mendassa.a	$⊢ A = MEndo (M)$
2		mendassa.s	$⊢ S = Scalar (M)$
3	1	mendbas	$⊢ M LMHom M = {Base}_{A}$
4	3	a1i	$⊢ (M \in LMod \land S \in CRing) \to M LMHom M = {Base}_{A}$
5		eqidd	$⊢ (M \in LMod \land S \in CRing) \to +_{A} = +_{A}$
6	1 2	mendsca	$⊢ S = Scalar (A)$
7	6	a1i	$⊢ (M \in LMod \land S \in CRing) \to S = Scalar (A)$
8		eqidd	$⊢ (M \in LMod \land S \in CRing) \to \cdot_{A} = \cdot_{A}$
9		eqidd	$⊢ (M \in LMod \land S \in CRing) \to {Base}_{S} = {Base}_{S}$
10		eqidd	$⊢ (M \in LMod \land S \in CRing) \to +_{S} = +_{S}$
11		eqidd	$⊢ (M \in LMod \land S \in CRing) \to \cdot_{S} = \cdot_{S}$
12		eqidd	$⊢ (M \in LMod \land S \in CRing) \to 1_{S} = 1_{S}$
13		crngring	$⊢ S \in CRing \to S \in Ring$
14	13	adantl	$⊢ (M \in LMod \land S \in CRing) \to S \in Ring$
15	1	mendring	$⊢ M \in LMod \to A \in Ring$
16	15	adantr	$⊢ (M \in LMod \land S \in CRing) \to A \in Ring$
17		ringgrp	$⊢ A \in Ring \to A \in Grp$
18	16 17	syl	$⊢ (M \in LMod \land S \in CRing) \to A \in Grp$
19		eqid	$⊢ \cdot_{M} = \cdot_{M}$
20		eqid	$⊢ {Base}_{S} = {Base}_{S}$
21		eqid	$⊢ {Base}_{M} = {Base}_{M}$
22		eqid	$⊢ \cdot_{A} = \cdot_{A}$
23	1 19 3 2 20 21 22	mendvsca	$⊢ (x \in {Base}_{S} \land y \in (M LMHom M)) \to x \cdot_{A} y = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y$
24	23	3adant1	$⊢ ((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land y \in (M LMHom M)) \to x \cdot_{A} y = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y$
25	21 19 2 20	lmhmvsca	$⊢ (S \in CRing \land x \in {Base}_{S} \land y \in (M LMHom M)) \to ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y \in (M LMHom M)$
26	25	3adant1l	$⊢ ((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land y \in (M LMHom M)) \to ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y \in (M LMHom M)$
27	24 26	eqeltrd	$⊢ ((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land y \in (M LMHom M)) \to x \cdot_{A} y \in (M LMHom M)$
28		simpr2	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to y \in (M LMHom M)$
29		simpr3	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to z \in (M LMHom M)$
30		eqid	$⊢ +_{M} = +_{M}$
31		eqid	$⊢ +_{A} = +_{A}$
32	1 3 30 31	mendplusg	$⊢ (y \in (M LMHom M) \land z \in (M LMHom M)) \to y +_{A} z = y {+_{M}}_{f} z$
33	28 29 32	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to y +_{A} z = y {+_{M}}_{f} z$
34	33	oveq2d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y +_{A} z) = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y {+_{M}}_{f} z)$
35		simpr1	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to x \in {Base}_{S}$
36	18	adantr	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to A \in Grp$
37	3 31	grpcl	$⊢ (A \in Grp \land y \in (M LMHom M) \land z \in (M LMHom M)) \to y +_{A} z \in (M LMHom M)$
38	36 28 29 37	syl3anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to y +_{A} z \in (M LMHom M)$
39	1 19 3 2 20 21 22	mendvsca	$⊢ (x \in {Base}_{S} \land y +_{A} z \in (M LMHom M)) \to x \cdot_{A} (y +_{A} z) = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y +_{A} z)$
40	35 38 39	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to x \cdot_{A} (y +_{A} z) = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y +_{A} z)$
41	35 28 23	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to x \cdot_{A} y = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y$
42	1 19 3 2 20 21 22	mendvsca	$⊢ (x \in {Base}_{S} \land z \in (M LMHom M)) \to x \cdot_{A} z = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z$
43	35 29 42	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to x \cdot_{A} z = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z$
44	41 43	oveq12d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to (x \cdot_{A} y) {+_{M}}_{f} (x \cdot_{A} z) = (({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y) {+_{M}}_{f} (({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z)$
45	27	3adant3r3	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to x \cdot_{A} y \in (M LMHom M)$
46		eleq1w	$⊢ y = z \to (y \in (M LMHom M) \leftrightarrow z \in (M LMHom M))$
47	46	3anbi3d	$⊢ y = z \to (((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land y \in (M LMHom M)) \leftrightarrow ((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land z \in (M LMHom M)))$
48		oveq2	$⊢ y = z \to x \cdot_{A} y = x \cdot_{A} z$
49	48	eleq1d	$⊢ y = z \to (x \cdot_{A} y \in (M LMHom M) \leftrightarrow x \cdot_{A} z \in (M LMHom M))$
50	47 49	imbi12d	$⊢ y = z \to ((((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land y \in (M LMHom M)) \to x \cdot_{A} y \in (M LMHom M)) \leftrightarrow (((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land z \in (M LMHom M)) \to x \cdot_{A} z \in (M LMHom M)))$
51	50 27	chvarvv	$⊢ ((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land z \in (M LMHom M)) \to x \cdot_{A} z \in (M LMHom M)$
52	51	3adant3r2	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to x \cdot_{A} z \in (M LMHom M)$
53	1 3 30 31	mendplusg	$⊢ (x \cdot_{A} y \in (M LMHom M) \land x \cdot_{A} z \in (M LMHom M)) \to (x \cdot_{A} y) +_{A} (x \cdot_{A} z) = (x \cdot_{A} y) {+_{M}}_{f} (x \cdot_{A} z)$
54	45 52 53	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to (x \cdot_{A} y) +_{A} (x \cdot_{A} z) = (x \cdot_{A} y) {+_{M}}_{f} (x \cdot_{A} z)$
55		fvexd	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to {Base}_{M} \in V$
56		fconst6g	$⊢ x \in {Base}_{S} \to ({Base}_{M} \times \{x\}) : {Base}_{M} ⟶ {Base}_{S}$
57	35 56	syl	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to ({Base}_{M} \times \{x\}) : {Base}_{M} ⟶ {Base}_{S}$
58	21 21	lmhmf	$⊢ y \in (M LMHom M) \to y : {Base}_{M} ⟶ {Base}_{M}$
59	28 58	syl	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to y : {Base}_{M} ⟶ {Base}_{M}$
60	21 21	lmhmf	$⊢ z \in (M LMHom M) \to z : {Base}_{M} ⟶ {Base}_{M}$
61	29 60	syl	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to z : {Base}_{M} ⟶ {Base}_{M}$
62		simpll	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to M \in LMod$
63	21 30 2 19 20	lmodvsdi	$⊢ (M \in LMod \land (w \in {Base}_{S} \land v \in {Base}_{M} \land u \in {Base}_{M})) \to w \cdot_{M} (v +_{M} u) = (w \cdot_{M} v) +_{M} (w \cdot_{M} u)$
64	62 63	sylan	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \land (w \in {Base}_{S} \land v \in {Base}_{M} \land u \in {Base}_{M})) \to w \cdot_{M} (v +_{M} u) = (w \cdot_{M} v) +_{M} (w \cdot_{M} u)$
65	55 57 59 61 64	caofdi	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y {+_{M}}_{f} z) = (({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y) {+_{M}}_{f} (({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z)$
66	44 54 65	3eqtr4d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in (M LMHom M) \land z \in (M LMHom M))) \to (x \cdot_{A} y) +_{A} (x \cdot_{A} z) = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y {+_{M}}_{f} z)$
67	34 40 66	3eqtr4d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \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)$
68		fvexd	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to {Base}_{M} \in V$
69		simpr3	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to z \in (M LMHom M)$
70	69 60	syl	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to z : {Base}_{M} ⟶ {Base}_{M}$
71		simpr1	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to x \in {Base}_{S}$
72	71 56	syl	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to ({Base}_{M} \times \{x\}) : {Base}_{M} ⟶ {Base}_{S}$
73		simpr2	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to y \in {Base}_{S}$
74		fconst6g	$⊢ y \in {Base}_{S} \to ({Base}_{M} \times \{y\}) : {Base}_{M} ⟶ {Base}_{S}$
75	73 74	syl	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to ({Base}_{M} \times \{y\}) : {Base}_{M} ⟶ {Base}_{S}$
76		simpll	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to M \in LMod$
77		eqid	$⊢ +_{S} = +_{S}$
78	21 30 2 19 20 77	lmodvsdir	$⊢ (M \in LMod \land (w \in {Base}_{S} \land v \in {Base}_{S} \land u \in {Base}_{M})) \to (w +_{S} v) \cdot_{M} u = (w \cdot_{M} u) +_{M} (v \cdot_{M} u)$
79	76 78	sylan	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \land (w \in {Base}_{S} \land v \in {Base}_{S} \land u \in {Base}_{M})) \to (w +_{S} v) \cdot_{M} u = (w \cdot_{M} u) +_{M} (v \cdot_{M} u)$
80	68 70 72 75 79	caofdir	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (({Base}_{M} \times \{x\}) {+_{S}}_{f} ({Base}_{M} \times \{y\})) {\cdot_{M}}_{f} z = (({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z) {+_{M}}_{f} (({Base}_{M} \times \{y\}) {\cdot_{M}}_{f} z)$
81	14	adantr	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to S \in Ring$
82	20 77	ringacl	$⊢ (S \in Ring \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x +_{S} y \in {Base}_{S}$
83	81 71 73 82	syl3anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to x +_{S} y \in {Base}_{S}$
84	1 19 3 2 20 21 22	mendvsca	$⊢ (x +_{S} y \in {Base}_{S} \land z \in (M LMHom M)) \to (x +_{S} y) \cdot_{A} z = ({Base}_{M} \times \{x +_{S} y\}) {\cdot_{M}}_{f} z$
85	83 69 84	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (x +_{S} y) \cdot_{A} z = ({Base}_{M} \times \{x +_{S} y\}) {\cdot_{M}}_{f} z$
86	68 71 73	ofc12	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to ({Base}_{M} \times \{x\}) {+_{S}}_{f} ({Base}_{M} \times \{y\}) = {Base}_{M} \times \{x +_{S} y\}$
87	86	oveq1d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (({Base}_{M} \times \{x\}) {+_{S}}_{f} ({Base}_{M} \times \{y\})) {\cdot_{M}}_{f} z = ({Base}_{M} \times \{x +_{S} y\}) {\cdot_{M}}_{f} z$
88	85 87	eqtr4d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (x +_{S} y) \cdot_{A} z = (({Base}_{M} \times \{x\}) {+_{S}}_{f} ({Base}_{M} \times \{y\})) {\cdot_{M}}_{f} z$
89	51	3adant3r2	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to x \cdot_{A} z \in (M LMHom M)$
90		eleq1w	$⊢ x = y \to (x \in {Base}_{S} \leftrightarrow y \in {Base}_{S})$
91	90	3anbi2d	$⊢ x = y \to (((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land z \in (M LMHom M)) \leftrightarrow ((M \in LMod \land S \in CRing) \land y \in {Base}_{S} \land z \in (M LMHom M)))$
92		oveq1	$⊢ x = y \to x \cdot_{A} z = y \cdot_{A} z$
93	92	eleq1d	$⊢ x = y \to (x \cdot_{A} z \in (M LMHom M) \leftrightarrow y \cdot_{A} z \in (M LMHom M))$
94	91 93	imbi12d	$⊢ x = y \to ((((M \in LMod \land S \in CRing) \land x \in {Base}_{S} \land z \in (M LMHom M)) \to x \cdot_{A} z \in (M LMHom M)) \leftrightarrow (((M \in LMod \land S \in CRing) \land y \in {Base}_{S} \land z \in (M LMHom M)) \to y \cdot_{A} z \in (M LMHom M)))$
95	94 51	chvarvv	$⊢ ((M \in LMod \land S \in CRing) \land y \in {Base}_{S} \land z \in (M LMHom M)) \to y \cdot_{A} z \in (M LMHom M)$
96	95	3adant3r1	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to y \cdot_{A} z \in (M LMHom M)$
97	1 3 30 31	mendplusg	$⊢ (x \cdot_{A} z \in (M LMHom M) \land y \cdot_{A} z \in (M LMHom M)) \to (x \cdot_{A} z) +_{A} (y \cdot_{A} z) = (x \cdot_{A} z) {+_{M}}_{f} (y \cdot_{A} z)$
98	89 96 97	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (x \cdot_{A} z) +_{A} (y \cdot_{A} z) = (x \cdot_{A} z) {+_{M}}_{f} (y \cdot_{A} z)$
99	71 69 42	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to x \cdot_{A} z = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z$
100	1 19 3 2 20 21 22	mendvsca	$⊢ (y \in {Base}_{S} \land z \in (M LMHom M)) \to y \cdot_{A} z = ({Base}_{M} \times \{y\}) {\cdot_{M}}_{f} z$
101	73 69 100	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to y \cdot_{A} z = ({Base}_{M} \times \{y\}) {\cdot_{M}}_{f} z$
102	99 101	oveq12d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (x \cdot_{A} z) {+_{M}}_{f} (y \cdot_{A} z) = (({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z) {+_{M}}_{f} (({Base}_{M} \times \{y\}) {\cdot_{M}}_{f} z)$
103	98 102	eqtrd	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (x \cdot_{A} z) +_{A} (y \cdot_{A} z) = (({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z) {+_{M}}_{f} (({Base}_{M} \times \{y\}) {\cdot_{M}}_{f} z)$
104	80 88 103	3eqtr4d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (x +_{S} y) \cdot_{A} z = (x \cdot_{A} z) +_{A} (y \cdot_{A} z)$
105		ovexd	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \land k \in {Base}_{M}) \to x \cdot_{S} y \in V$
106	70	ffvelcdmda	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \land k \in {Base}_{M}) \to z (k) \in {Base}_{M}$
107		fconstmpt	$⊢ {Base}_{M} \times \{x \cdot_{S} y\} = (k \in {Base}_{M} ⟼ x \cdot_{S} y)$
108	107	a1i	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to {Base}_{M} \times \{x \cdot_{S} y\} = (k \in {Base}_{M} ⟼ x \cdot_{S} y)$
109	70	feqmptd	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to z = (k \in {Base}_{M} ⟼ z (k))$
110	68 105 106 108 109	offval2	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to ({Base}_{M} \times \{x \cdot_{S} y\}) {\cdot_{M}}_{f} z = (k \in {Base}_{M} ⟼ (x \cdot_{S} y) \cdot_{M} z (k))$
111		eqid	$⊢ \cdot_{S} = \cdot_{S}$
112	20 111	ringcl	$⊢ (S \in Ring \land x \in {Base}_{S} \land y \in {Base}_{S}) \to x \cdot_{S} y \in {Base}_{S}$
113	81 71 73 112	syl3anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to x \cdot_{S} y \in {Base}_{S}$
114	1 19 3 2 20 21 22	mendvsca	$⊢ (x \cdot_{S} y \in {Base}_{S} \land z \in (M LMHom M)) \to (x \cdot_{S} y) \cdot_{A} z = ({Base}_{M} \times \{x \cdot_{S} y\}) {\cdot_{M}}_{f} z$
115	113 69 114	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (x \cdot_{S} y) \cdot_{A} z = ({Base}_{M} \times \{x \cdot_{S} y\}) {\cdot_{M}}_{f} z$
116	71	adantr	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \land k \in {Base}_{M}) \to x \in {Base}_{S}$
117		ovexd	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \land k \in {Base}_{M}) \to y \cdot_{M} z (k) \in V$
118		fconstmpt	$⊢ {Base}_{M} \times \{x\} = (k \in {Base}_{M} ⟼ x)$
119	118	a1i	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to {Base}_{M} \times \{x\} = (k \in {Base}_{M} ⟼ x)$
120		simplr2	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \land k \in {Base}_{M}) \to y \in {Base}_{S}$
121		fconstmpt	$⊢ {Base}_{M} \times \{y\} = (k \in {Base}_{M} ⟼ y)$
122	121	a1i	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to {Base}_{M} \times \{y\} = (k \in {Base}_{M} ⟼ y)$
123	68 120 106 122 109	offval2	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to ({Base}_{M} \times \{y\}) {\cdot_{M}}_{f} z = (k \in {Base}_{M} ⟼ y \cdot_{M} z (k))$
124	101 123	eqtrd	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to y \cdot_{A} z = (k \in {Base}_{M} ⟼ y \cdot_{M} z (k))$
125	68 116 117 119 124	offval2	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y \cdot_{A} z) = (k \in {Base}_{M} ⟼ x \cdot_{M} (y \cdot_{M} z (k)))$
126	1 19 3 2 20 21 22	mendvsca	$⊢ (x \in {Base}_{S} \land y \cdot_{A} z \in (M LMHom M)) \to x \cdot_{A} (y \cdot_{A} z) = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y \cdot_{A} z)$
127	71 96 126	syl2anc	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to x \cdot_{A} (y \cdot_{A} z) = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y \cdot_{A} z)$
128	76	adantr	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \land k \in {Base}_{M}) \to M \in LMod$
129	21 2 19 20 111	lmodvsass	$⊢ (M \in LMod \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z (k) \in {Base}_{M})) \to (x \cdot_{S} y) \cdot_{M} z (k) = x \cdot_{M} (y \cdot_{M} z (k))$
130	128 116 120 106 129	syl13anc	$⊢ (((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \land k \in {Base}_{M}) \to (x \cdot_{S} y) \cdot_{M} z (k) = x \cdot_{M} (y \cdot_{M} z (k))$
131	130	mpteq2dva	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (k \in {Base}_{M} ⟼ (x \cdot_{S} y) \cdot_{M} z (k)) = (k \in {Base}_{M} ⟼ x \cdot_{M} (y \cdot_{M} z (k)))$
132	125 127 131	3eqtr4d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to x \cdot_{A} (y \cdot_{A} z) = (k \in {Base}_{M} ⟼ (x \cdot_{S} y) \cdot_{M} z (k))$
133	110 115 132	3eqtr4d	$⊢ ((M \in LMod \land S \in CRing) \land (x \in {Base}_{S} \land y \in {Base}_{S} \land z \in (M LMHom M))) \to (x \cdot_{S} y) \cdot_{A} z = x \cdot_{A} (y \cdot_{A} z)$
134	14	adantr	$⊢ ((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \to S \in Ring$
135		eqid	$⊢ 1_{S} = 1_{S}$
136	20 135	ringidcl	$⊢ S \in Ring \to 1_{S} \in {Base}_{S}$
137	134 136	syl	$⊢ ((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \to 1_{S} \in {Base}_{S}$
138	1 19 3 2 20 21 22	mendvsca	$⊢ (1_{S} \in {Base}_{S} \land x \in (M LMHom M)) \to 1_{S} \cdot_{A} x = ({Base}_{M} \times \{1_{S}\}) {\cdot_{M}}_{f} x$
139	137 138	sylancom	$⊢ ((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \to 1_{S} \cdot_{A} x = ({Base}_{M} \times \{1_{S}\}) {\cdot_{M}}_{f} x$
140		fvexd	$⊢ ((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \to {Base}_{M} \in V$
141	21 21	lmhmf	$⊢ x \in (M LMHom M) \to x : {Base}_{M} ⟶ {Base}_{M}$
142	141	adantl	$⊢ ((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \to x : {Base}_{M} ⟶ {Base}_{M}$
143		simpll	$⊢ ((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \to M \in LMod$
144	21 2 19 135	lmodvs1	$⊢ (M \in LMod \land y \in {Base}_{M}) \to 1_{S} \cdot_{M} y = y$
145	143 144	sylan	$⊢ (((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \land y \in {Base}_{M}) \to 1_{S} \cdot_{M} y = y$
146	140 142 137 145	caofid0l	$⊢ ((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \to ({Base}_{M} \times \{1_{S}\}) {\cdot_{M}}_{f} x = x$
147	139 146	eqtrd	$⊢ ((M \in LMod \land S \in CRing) \land x \in (M LMHom M)) \to 1_{S} \cdot_{A} x = x$
148	4 5 7 8 9 10 11 12 14 18 27 67 104 133 147	islmodd	$⊢ (M \in LMod \land S \in CRing) \to A \in LMod$

Metamath Proof Explorer

Theorem mendlmod

Proof