mendsca

Description: The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 31-Oct-2024)

	Ref	Expression
Hypotheses	mendsca.a	$⊢ A = MEndo (M)$
	mendsca.s	$⊢ S = Scalar (M)$
Assertion	mendsca	$⊢ S = Scalar (A)$

Proof

Step	Hyp	Ref	Expression
1		mendsca.a	$⊢ A = MEndo (M)$
2		mendsca.s	$⊢ S = Scalar (M)$
3		fvex	$⊢ Scalar (M) \in V$
4		eqid	$⊢ \{⟨{Base}_{ndx}, M LMHom M⟩, ⟨+_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), Scalar (M)⟩, ⟨\cdot_{ndx}, (x \in {Base}_{Scalar (M)}, y \in (M LMHom M) ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y)⟩\} = \{⟨{Base}_{ndx}, M LMHom M⟩, ⟨+_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), Scalar (M)⟩, ⟨\cdot_{ndx}, (x \in {Base}_{Scalar (M)}, y \in (M LMHom M) ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y)⟩\}$
5	4	algsca	$⊢ Scalar (M) \in V \to Scalar (M) = Scalar (\{⟨{Base}_{ndx}, M LMHom M⟩, ⟨+_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), Scalar (M)⟩, ⟨\cdot_{ndx}, (x \in {Base}_{Scalar (M)}, y \in (M LMHom M) ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y)⟩\})$
6	3 5	mp1i	$⊢ M \in V \to Scalar (M) = Scalar (\{⟨{Base}_{ndx}, M LMHom M⟩, ⟨+_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), Scalar (M)⟩, ⟨\cdot_{ndx}, (x \in {Base}_{Scalar (M)}, y \in (M LMHom M) ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y)⟩\})$
7		eqid	$⊢ M LMHom M = M LMHom M$
8		eqid	$⊢ (x \in (M LMHom M), y \in (M LMHom M) ⟼ x {+_{M}}_{f} y) = (x \in (M LMHom M), y \in (M LMHom M) ⟼ x {+_{M}}_{f} y)$
9		eqid	$⊢ (x \in (M LMHom M), y \in (M LMHom M) ⟼ x \circ y) = (x \in (M LMHom M), y \in (M LMHom M) ⟼ x \circ y)$
10		eqid	$⊢ Scalar (M) = Scalar (M)$
11		eqid	$⊢ (x \in {Base}_{Scalar (M)}, y \in (M LMHom M) ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y) = (x \in {Base}_{Scalar (M)}, y \in (M LMHom M) ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y)$
12	7 8 9 10 11	mendval	$⊢ M \in V \to MEndo (M) = \{⟨{Base}_{ndx}, M LMHom M⟩, ⟨+_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), Scalar (M)⟩, ⟨\cdot_{ndx}, (x \in {Base}_{Scalar (M)}, y \in (M LMHom M) ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y)⟩\}$
13	12	fveq2d	$⊢ M \in V \to Scalar (MEndo (M)) = Scalar (\{⟨{Base}_{ndx}, M LMHom M⟩, ⟨+_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x {+_{M}}_{f} y)⟩, ⟨\cdot_{ndx}, (x \in (M LMHom M), y \in (M LMHom M) ⟼ x \circ y)⟩\} \cup \{⟨Scalar (ndx), Scalar (M)⟩, ⟨\cdot_{ndx}, (x \in {Base}_{Scalar (M)}, y \in (M LMHom M) ⟼ ({Base}_{M} \times \{x\}) {\cdot_{M}}_{f} y)⟩\})$
14	6 13	eqtr4d	$⊢ M \in V \to Scalar (M) = Scalar (MEndo (M))$
15		scaid	$⊢ Scalar = Slot Scalar (ndx)$
16	15	str0	$⊢ \emptyset = Scalar (\emptyset)$
17	16	eqcomi	$⊢ Scalar (\emptyset) = \emptyset$
18		eqid	$⊢ MEndo (M) = MEndo (M)$
19	17 18	fveqprc	$⊢ \neg M \in V \to Scalar (M) = Scalar (MEndo (M))$
20	14 19	pm2.61i	$⊢ Scalar (M) = Scalar (MEndo (M))$
21	1	fveq2i	$⊢ Scalar (A) = Scalar (MEndo (M))$
22	20 2 21	3eqtr4i	$⊢ S = Scalar (A)$

Metamath Proof Explorer

Theorem mendsca

Proof