Metamath Proof Explorer

Theorem dvavbase

Description: The vectors (vector base set) of the constructed partial vector space A are all translations (for a fiducial co-atom W ). (Contributed by NM, 9-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

		Ref	Expression
	Hypotheses	dvavbase.h	$⊢ H = LHyp (K)$
		dvavbase.t	$⊢ T = LTrn (K) (W)$
		dvavbase.u	$⊢ U = DVecA (K) (W)$
		dvavbase.v	$⊢ V = {Base}_{U}$
	Assertion	dvavbase	$⊢ (K \in X \land W \in H) \to V = T$

Proof

Step	Hyp	Ref	Expression
1		dvavbase.h	$⊢ H = LHyp (K)$
2		dvavbase.t	$⊢ T = LTrn (K) (W)$
3		dvavbase.u	$⊢ U = DVecA (K) (W)$
4		dvavbase.v	$⊢ V = {Base}_{U}$
5		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
6		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
7	1 2 5 6 3	dvaset	$⊢ (K \in X \land W \in H) \to U = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in T ⟼ s (f))⟩\}$
8	7	fveq2d	$⊢ (K \in X \land W \in H) \to {Base}_{U} = {Base}_{(\{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in T ⟼ s (f))⟩\})}$
9	2	fvexi	$⊢ T \in V$
10		eqid	$⊢ \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in T ⟼ s (f))⟩\} = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in T ⟼ s (f))⟩\}$
11	10	lmodbase	$⊢ T \in V \to T = {Base}_{(\{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in T ⟼ s (f))⟩\})}$
12	9 11	ax-mp	$⊢ T = {Base}_{(\{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (W)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (W), f \in T ⟼ s (f))⟩\})}$
13	8 4 12	3eqtr4g	$⊢ (K \in X \land W \in H) \to V = T$