mendbas

Description: Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015)

		Ref	Expression
	Hypothesis	mendbas.a	$⊢ A = MEndo (M)$
	Assertion	mendbas	$⊢ M LMHom M = {Base}_{A}$

Proof

Step	Hyp	Ref	Expression
1		mendbas.a	$⊢ A = MEndo (M)$
2		ovex	$⊢ M LMHom M \in V$
3		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)⟩\}$
4	3	algbase	$⊢ M LMHom M \in V \to M LMHom M = {Base}_{(\{⟨{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	2 4	mp1i	$⊢ M \in V \to M LMHom M = {Base}_{(\{⟨{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		eqid	$⊢ M LMHom M = M LMHom M$
7		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)$
8		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)$
9		eqid	$⊢ Scalar (M) = Scalar (M)$
10		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)$
11	6 7 8 9 10	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)⟩\}$
12	1 11	syl5eq	$⊢ M \in V \to A = \{⟨{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 {Base}_{A} = {Base}_{(\{⟨{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	5 13	eqtr4d	$⊢ M \in V \to M LMHom M = {Base}_{A}$
15		base0	$⊢ \emptyset = {Base}_{\emptyset}$
16		reldmlmhm	$⊢ Rel dom LMHom$
17	16	ovprc1	$⊢ \neg M \in V \to M LMHom M = \emptyset$
18		fvprc	$⊢ \neg M \in V \to MEndo (M) = \emptyset$
19	1 18	syl5eq	$⊢ \neg M \in V \to A = \emptyset$
20	19	fveq2d	$⊢ \neg M \in V \to {Base}_{A} = {Base}_{\emptyset}$
21	15 17 20	3eqtr4a	$⊢ \neg M \in V \to M LMHom M = {Base}_{A}$
22	14 21	pm2.61i	$⊢ M LMHom M = {Base}_{A}$

Metamath Proof Explorer

Theorem mendbas

Proof