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

Metamath Proof Explorer

Theorem mendassa

Proof