dvaset

Description: The constructed partial vector space A for a lattice K . (Contributed by NM, 8-Oct-2013) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dvaset.h	$⊢ H = LHyp (K)$
	dvaset.t	$⊢ T = LTrn (K) (W)$
	dvaset.e	$⊢ E = TEndo (K) (W)$
	dvaset.d	$⊢ D = EDRing (K) (W)$
	dvaset.u	$⊢ U = DVecA (K) (W)$
Assertion	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), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩\}$

Proof

Step	Hyp	Ref	Expression
1		dvaset.h	$⊢ H = LHyp (K)$
2		dvaset.t	$⊢ T = LTrn (K) (W)$
3		dvaset.e	$⊢ E = TEndo (K) (W)$
4		dvaset.d	$⊢ D = EDRing (K) (W)$
5		dvaset.u	$⊢ U = DVecA (K) (W)$
6	1	dvafset	$⊢ K \in X \to DVecA (K) = (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩\})$
7	6	fveq1d	$⊢ K \in X \to DVecA (K) (W) = (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩\}) (W)$
8		fveq2	$⊢ w = W \to LTrn (K) (w) = LTrn (K) (W)$
9	8 2	eqtr4di	$⊢ w = W \to LTrn (K) (w) = T$
10	9	opeq2d	$⊢ w = W \to ⟨{Base}_{ndx}, LTrn (K) (w)⟩ = ⟨{Base}_{ndx}, T⟩$
11		eqidd	$⊢ w = W \to f \circ g = f \circ g$
12	9 9 11	mpoeq123dv	$⊢ w = W \to (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g) = (f \in T, g \in T ⟼ f \circ g)$
13	12	opeq2d	$⊢ w = W \to ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩ = ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩$
14		fveq2	$⊢ w = W \to EDRing (K) (w) = EDRing (K) (W)$
15	14 4	eqtr4di	$⊢ w = W \to EDRing (K) (w) = D$
16	15	opeq2d	$⊢ w = W \to ⟨Scalar (ndx), EDRing (K) (w)⟩ = ⟨Scalar (ndx), D⟩$
17	10 13 16	tpeq123d	$⊢ w = W \to \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (w)⟩\} = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), D⟩\}$
18		fveq2	$⊢ w = W \to TEndo (K) (w) = TEndo (K) (W)$
19	18 3	eqtr4di	$⊢ w = W \to TEndo (K) (w) = E$
20		eqidd	$⊢ w = W \to s (f) = s (f)$
21	19 9 20	mpoeq123dv	$⊢ w = W \to (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f)) = (s \in E, f \in T ⟼ s (f))$
22	21	opeq2d	$⊢ w = W \to ⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩ = ⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩$
23	22	sneqd	$⊢ w = W \to \{⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩\} = \{⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩\}$
24	17 23	uneq12d	$⊢ w = W \to \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩\} = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩\}$
25		eqid	$⊢ (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩\}) = (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩\})$
26		tpex	$⊢ \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), D⟩\} \in V$
27		snex	$⊢ \{⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩\} \in V$
28	26 27	unex	$⊢ \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩\} \in V$
29	24 25 28	fvmpt	$⊢ W \in H \to (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (w)⟩\} \cup \{⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩\}) (W) = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩\}$
30	7 29	sylan9eq	$⊢ (K \in X \land W \in H) \to DVecA (K) (W) = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩\}$
31	5 30	syl5eq	$⊢ (K \in X \land W \in H) \to U = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in T ⟼ s (f))⟩\}$

Metamath Proof Explorer

Theorem dvaset

Proof