mendassa

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

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

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	1 2	mendsca	$⊢ S = Scalar (A)$
6	5	a1i	$⊢ (M \in LMod \land S \in CRing) \to S = Scalar (A)$
7		eqidd	$⊢ (M \in LMod \land S \in CRing) \to {Base}_{S} = {Base}_{S}$
8		eqidd	$⊢ (M \in LMod \land S \in CRing) \to \cdot_{A} = \cdot_{A}$
9		eqidd	$⊢ (M \in LMod \land S \in CRing) \to \cdot_{A} = \cdot_{A}$
10	1 2	mendlmod	$⊢ (M \in LMod \land S \in CRing) \to A \in LMod$
11	1	mendring	$⊢ M \in LMod \to A \in Ring$
12	11	adantr	$⊢ (M \in LMod \land S \in CRing) \to A \in Ring$
13		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)$
14		eqid	$⊢ {Base}_{M} = {Base}_{M}$
15	14 14	lmhmf	$⊢ z \in (M LMHom M) \to z : {Base}_{M} ⟶ {Base}_{M}$
16	13 15	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}$
17	16	ffvelcdmda	$⊢ (((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 v \in {Base}_{M}) \to z (v) \in {Base}_{M}$
18	16	feqmptd	$⊢ ((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 = (v \in {Base}_{M} ⟼ z (v))$
19		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}$
20		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)$
21		eqid	$⊢ \cdot_{M} = \cdot_{M}$
22		eqid	$⊢ {Base}_{S} = {Base}_{S}$
23		eqid	$⊢ \cdot_{A} = \cdot_{A}$
24	1 21 3 2 22 14 23	mendvsca	$⊢ (x \in {Base}_{S} \land y \in (M LMHom M)) \to x \cdot_{A} y = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y$
25	19 20 24	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$
26		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$
27		simplr1	$⊢ (((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}_{M}) \to x \in {Base}_{S}$
28		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))) \land w \in {Base}_{M}) \to y (w) \in V$
29		fconstmpt	$⊢ {Base}_{M} \times \{x\} = (w \in {Base}_{M} ⟼ x)$
30	29	a1i	$⊢ ((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\} = (w \in {Base}_{M} ⟼ x)$
31	14 14	lmhmf	$⊢ y \in (M LMHom M) \to y : {Base}_{M} ⟶ {Base}_{M}$
32	20 31	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}$
33	32	feqmptd	$⊢ ((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 = (w \in {Base}_{M} ⟼ y (w))$
34	26 27 28 30 33	offval2	$⊢ ((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 = (w \in {Base}_{M} ⟼ x \cdot_{M} y (w))$
35	25 34	eqtrd	$⊢ ((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 = (w \in {Base}_{M} ⟼ x \cdot_{M} y (w))$
36		fveq2	$⊢ w = z (v) \to y (w) = y (z (v))$
37	36	oveq2d	$⊢ w = z (v) \to x \cdot_{M} y (w) = x \cdot_{M} y (z (v))$
38	17 18 35 37	fmptco	$⊢ ((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) \circ z = (v \in {Base}_{M} ⟼ x \cdot_{M} y (z (v)))$
39		simplr1	$⊢ (((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 v \in {Base}_{M}) \to x \in {Base}_{S}$
40		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))) \land v \in {Base}_{M}) \to y (z (v)) \in V$
41		fconstmpt	$⊢ {Base}_{M} \times \{x\} = (v \in {Base}_{M} ⟼ x)$
42	41	a1i	$⊢ ((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\} = (v \in {Base}_{M} ⟼ x)$
43		eqid	$⊢ \cdot_{A} = \cdot_{A}$
44	1 3 43	mendmulr	$⊢ (y \in (M LMHom M) \land z \in (M LMHom M)) \to y \cdot_{A} z = y \circ z$
45	20 13 44	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 \cdot_{A} z = y \circ z$
46		fcompt	$⊢ (y : {Base}_{M} ⟶ {Base}_{M} \land z : {Base}_{M} ⟶ {Base}_{M}) \to y \circ z = (v \in {Base}_{M} ⟼ y (z (v)))$
47	32 16 46	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 \circ z = (v \in {Base}_{M} ⟼ y (z (v)))$
48	45 47	eqtrd	$⊢ ((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 \cdot_{A} z = (v \in {Base}_{M} ⟼ y (z (v)))$
49	26 39 40 42 48	offval2	$⊢ ((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 \cdot_{A} z) = (v \in {Base}_{M} ⟼ x \cdot_{M} y (z (v)))$
50	38 49	eqtr4d	$⊢ ((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) \circ z = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y \cdot_{A} z)$
51	10	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 LMod$
52	3 5 23 22	lmodvscl	$⊢ (A \in LMod \land x \in {Base}_{S} \land y \in (M LMHom M)) \to x \cdot_{A} y \in (M LMHom M)$
53	51 19 20 52	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 x \cdot_{A} y \in (M LMHom M)$
54	1 3 43	mendmulr	$⊢ (x \cdot_{A} 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$
55	53 13 54	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) \cdot_{A} z = (x \cdot_{A} y) \circ z$
56	12	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 Ring$
57	3 43	ringcl	$⊢ (A \in Ring \land y \in (M LMHom M) \land z \in (M LMHom M)) \to y \cdot_{A} z \in (M LMHom M)$
58	56 20 13 57	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 \cdot_{A} z \in (M LMHom M)$
59	1 21 3 2 22 14 23	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)$
60	19 58 59	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 \cdot_{A} z) = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y \cdot_{A} z)$
61	50 55 60	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) \cdot_{A} z = x \cdot_{A} (y \cdot_{A} z)$
62		simplr2	$⊢ (((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 v \in {Base}_{M}) \to y \in (M LMHom M)$
63	2 22 14 21 21	lmhmlin	$⊢ (y \in (M LMHom M) \land x \in {Base}_{S} \land z (v) \in {Base}_{M}) \to y (x \cdot_{M} z (v)) = x \cdot_{M} y (z (v))$
64	62 39 17 63	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))) \land v \in {Base}_{M}) \to y (x \cdot_{M} z (v)) = x \cdot_{M} y (z (v))$
65	64	mpteq2dva	$⊢ ((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 (v \in {Base}_{M} ⟼ y (x \cdot_{M} z (v))) = (v \in {Base}_{M} ⟼ x \cdot_{M} y (z (v)))$
66		simplll	$⊢ (((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 v \in {Base}_{M}) \to M \in LMod$
67	14 2 21 22	lmodvscl	$⊢ (M \in LMod \land x \in {Base}_{S} \land z (v) \in {Base}_{M}) \to x \cdot_{M} z (v) \in {Base}_{M}$
68	66 39 17 67	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))) \land v \in {Base}_{M}) \to x \cdot_{M} z (v) \in {Base}_{M}$
69	1 21 3 2 22 14 23	mendvsca	$⊢ (x \in {Base}_{S} \land z \in (M LMHom M)) \to x \cdot_{A} z = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} z$
70	19 13 69	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$
71		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))) \land v \in {Base}_{M}) \to z (v) \in V$
72	26 39 71 42 18	offval2	$⊢ ((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} z = (v \in {Base}_{M} ⟼ x \cdot_{M} z (v))$
73	70 72	eqtrd	$⊢ ((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 = (v \in {Base}_{M} ⟼ x \cdot_{M} z (v))$
74		fveq2	$⊢ w = x \cdot_{M} z (v) \to y (w) = y (x \cdot_{M} z (v))$
75	68 73 33 74	fmptco	$⊢ ((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 \circ (x \cdot_{A} z) = (v \in {Base}_{M} ⟼ y (x \cdot_{M} z (v)))$
76	65 75 49	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 y \circ (x \cdot_{A} z) = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} (y \cdot_{A} z)$
77	3 5 23 22	lmodvscl	$⊢ (A \in LMod \land x \in {Base}_{S} \land z \in (M LMHom M)) \to x \cdot_{A} z \in (M LMHom M)$
78	51 19 13 77	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 x \cdot_{A} z \in (M LMHom M)$
79	1 3 43	mendmulr	$⊢ (y \in (M LMHom M) \land x \cdot_{A} z \in (M LMHom M)) \to y \cdot_{A} (x \cdot_{A} z) = y \circ (x \cdot_{A} z)$
80	20 78 79	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 \cdot_{A} (x \cdot_{A} z) = y \circ (x \cdot_{A} z)$
81	76 80 60	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 y \cdot_{A} (x \cdot_{A} z) = x \cdot_{A} (y \cdot_{A} z)$
82	4 6 7 8 9 10 12 61 81	isassad	$⊢ (M \in LMod \land S \in CRing) \to A \in AssAlg$

Metamath Proof Explorer

Theorem mendassa

Proof