Metamath Proof Explorer

Theorem dvhsca

Description: The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014)

		Ref	Expression
	Hypotheses	dvhsca.h	$⊢ H = LHyp (K)$
		dvhsca.d	$⊢ D = EDRing (K) (W)$
		dvhsca.u	$⊢ U = DVecH (K) (W)$
		dvhsca.f	$⊢ F = Scalar (U)$
	Assertion	dvhsca	$⊢ (K \in X \land W \in H) \to F = D$

Proof

Step	Hyp	Ref	Expression
1		dvhsca.h	$⊢ H = LHyp (K)$
2		dvhsca.d	$⊢ D = EDRing (K) (W)$
3		dvhsca.u	$⊢ U = DVecH (K) (W)$
4		dvhsca.f	$⊢ F = Scalar (U)$
5		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
6		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
7	1 5 6 2 3	dvhset	$⊢ (K \in X \land W \in H) \to U = \{⟨{Base}_{ndx}, LTrn (K) (W) \times TEndo (K) (W)⟩, ⟨+_{ndx}, (f \in (LTrn (K) (W) \times TEndo (K) (W)), g \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (K) (W) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}$
8	7	fveq2d	$⊢ (K \in X \land W \in H) \to Scalar (U) = Scalar (\{⟨{Base}_{ndx}, LTrn (K) (W) \times TEndo (K) (W)⟩, ⟨+_{ndx}, (f \in (LTrn (K) (W) \times TEndo (K) (W)), g \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (K) (W) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})$
9	2	fvexi	$⊢ D \in V$
10		eqid	$⊢ \{⟨{Base}_{ndx}, LTrn (K) (W) \times TEndo (K) (W)⟩, ⟨+_{ndx}, (f \in (LTrn (K) (W) \times TEndo (K) (W)), g \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (K) (W) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\} = \{⟨{Base}_{ndx}, LTrn (K) (W) \times TEndo (K) (W)⟩, ⟨+_{ndx}, (f \in (LTrn (K) (W) \times TEndo (K) (W)), g \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (K) (W) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}$
11	10	lmodsca	$⊢ D \in V \to D = Scalar (\{⟨{Base}_{ndx}, LTrn (K) (W) \times TEndo (K) (W)⟩, ⟨+_{ndx}, (f \in (LTrn (K) (W) \times TEndo (K) (W)), g \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (K) (W) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})$
12	9 11	ax-mp	$⊢ D = Scalar (\{⟨{Base}_{ndx}, LTrn (K) (W) \times TEndo (K) (W)⟩, ⟨+_{ndx}, (f \in (LTrn (K) (W) \times TEndo (K) (W)), g \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in LTrn (K) (W) ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in (LTrn (K) (W) \times TEndo (K) (W)) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\})$
13	8 4 12	3eqtr4g	$⊢ (K \in X \land W \in H) \to F = D$