mendvscafval

Description: Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-2024)

	Ref	Expression
Hypotheses	mendvscafval.a	$⊢ A = MEndo (M)$
	mendvscafval.v	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	mendvscafval.b	$⊢ B = {Base}_{A}$
	mendvscafval.s	$⊢ S = Scalar (M)$
	mendvscafval.k	$⊢ K = {Base}_{S}$
	mendvscafval.e	$⊢ E = {Base}_{M}$
Assertion	mendvscafval	$⊢ \cdot_{A} = (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)$

Proof

Step	Hyp	Ref	Expression
1		mendvscafval.a	$⊢ A = MEndo (M)$
2		mendvscafval.v	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
3		mendvscafval.b	$⊢ B = {Base}_{A}$
4		mendvscafval.s	$⊢ S = Scalar (M)$
5		mendvscafval.k	$⊢ K = {Base}_{S}$
6		mendvscafval.e	$⊢ E = {Base}_{M}$
7	1	fveq2i	$⊢ \cdot_{A} = \cdot_{MEndo (M)}$
8	1	mendbas	$⊢ M LMHom M = {Base}_{A}$
9	3 8	eqtr4i	$⊢ B = M LMHom M$
10		eqid	$⊢ (x \in B, y \in B ⟼ x {+_{M}}_{f} y) = (x \in B, y \in B ⟼ x {+_{M}}_{f} y)$
11		eqid	$⊢ (x \in B, y \in B ⟼ x \circ y) = (x \in B, y \in B ⟼ x \circ y)$
12		eqid	$⊢ B = B$
13	6	xpeq1i	$⊢ E \times \{x\} = {Base}_{M} \times \{x\}$
14		eqid	$⊢ y = y$
15		ofeq	$⊢ \underset{˙}{\cdot} = \cdot_{M} \to \circ_{f} \underset{˙}{\cdot} = \circ_{f} \cdot_{M}$
16	2 15	ax-mp	$⊢ \circ_{f} \underset{˙}{\cdot} = \circ_{f} \cdot_{M}$
17	13 14 16	oveq123i	$⊢ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y = ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y$
18	5 12 17	mpoeq123i	$⊢ (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y) = (x \in {Base}_{S}, y \in B ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y)$
19	9 10 11 4 18	mendval	$⊢ M \in V \to MEndo (M) = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (x \in B, y \in B ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)⟩\}$
20	19	fveq2d	$⊢ M \in V \to \cdot_{MEndo (M)} = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (x \in B, y \in B ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)⟩\})}$
21	5	fvexi	$⊢ K \in V$
22	3	fvexi	$⊢ B \in V$
23	21 22	mpoex	$⊢ (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y) \in V$
24		eqid	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (x \in B, y \in B ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)⟩\} = \{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (x \in B, y \in B ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)⟩\}$
25	24	algvsca	$⊢ (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y) \in V \to (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y) = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (x \in B, y \in B ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)⟩\})}$
26	23 25	mp1i	$⊢ M \in V \to (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y) = \cdot_{(\{⟨{Base}_{ndx}, B⟩, ⟨+_{ndx}, (x \in B, y \in B ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in B, y \in B ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), S⟩, ⟨\cdot_{ndx}, (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)⟩\})}$
27	20 26	eqtr4d	$⊢ M \in V \to \cdot_{MEndo (M)} = (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)$
28		fvprc	$⊢ \neg M \in V \to MEndo (M) = \emptyset$
29	28	fveq2d	$⊢ \neg M \in V \to \cdot_{MEndo (M)} = \cdot_{\emptyset}$
30		vscaid	$⊢ \cdot_{𝑠} = Slot \cdot_{ndx}$
31	30	str0	$⊢ \emptyset = \cdot_{\emptyset}$
32	29 31	eqtr4di	$⊢ \neg M \in V \to \cdot_{MEndo (M)} = \emptyset$
33		fvprc	$⊢ \neg M \in V \to Scalar (M) = \emptyset$
34	4 33	syl5eq	$⊢ \neg M \in V \to S = \emptyset$
35	34	fveq2d	$⊢ \neg M \in V \to {Base}_{S} = {Base}_{\emptyset}$
36		base0	$⊢ \emptyset = {Base}_{\emptyset}$
37	35 5 36	3eqtr4g	$⊢ \neg M \in V \to K = \emptyset$
38	37	orcd	$⊢ \neg M \in V \to (K = \emptyset \lor B = \emptyset)$
39		0mpo0	$⊢ (K = \emptyset \lor B = \emptyset) \to (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y) = \emptyset$
40	38 39	syl	$⊢ \neg M \in V \to (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y) = \emptyset$
41	32 40	eqtr4d	$⊢ \neg M \in V \to \cdot_{MEndo (M)} = (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)$
42	27 41	pm2.61i	$⊢ \cdot_{MEndo (M)} = (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)$
43	7 42	eqtri	$⊢ \cdot_{A} = (x \in K, y \in B ⟼ (E \times \{x\}) {\underset{˙}{\cdot}}_{f} y)$

Metamath Proof Explorer

Theorem mendvscafval

Proof