dvafset

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
	Hypothesis	dvaset.h	$⊢ H = LHyp (K)$
	Assertion	dvafset	$⊢ K \in V \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))⟩\})$

Proof

Step	Hyp	Ref	Expression
1		dvaset.h	$⊢ H = LHyp (K)$
2		elex	$⊢ K \in V \to K \in V$
3		fveq2	$⊢ k = K \to LHyp (k) = LHyp (K)$
4	3 1	eqtr4di	$⊢ k = K \to LHyp (k) = H$
5		fveq2	$⊢ k = K \to LTrn (k) = LTrn (K)$
6	5	fveq1d	$⊢ k = K \to LTrn (k) (w) = LTrn (K) (w)$
7	6	opeq2d	$⊢ k = K \to ⟨{Base}_{ndx}, LTrn (k) (w)⟩ = ⟨{Base}_{ndx}, LTrn (K) (w)⟩$
8		eqidd	$⊢ k = K \to f \circ g = f \circ g$
9	6 6 8	mpoeq123dv	$⊢ k = K \to (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g) = (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)$
10	9	opeq2d	$⊢ k = K \to ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩ = ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩$
11		fveq2	$⊢ k = K \to EDRing (k) = EDRing (K)$
12	11	fveq1d	$⊢ k = K \to EDRing (k) (w) = EDRing (K) (w)$
13	12	opeq2d	$⊢ k = K \to ⟨Scalar (ndx), EDRing (k) (w)⟩ = ⟨Scalar (ndx), EDRing (K) (w)⟩$
14	7 10 13	tpeq123d	$⊢ k = K \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}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩, ⟨Scalar (ndx), EDRing (K) (w)⟩\}$
15		fveq2	$⊢ k = K \to TEndo (k) = TEndo (K)$
16	15	fveq1d	$⊢ k = K \to TEndo (k) (w) = TEndo (K) (w)$
17		eqidd	$⊢ k = K \to s (f) = s (f)$
18	16 6 17	mpoeq123dv	$⊢ k = K \to (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f)) = (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))$
19	18	opeq2d	$⊢ k = K \to ⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩ = ⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩$
20	19	sneqd	$⊢ k = K \to \{⟨\cdot_{ndx}, (s \in TEndo (k) (w), f \in LTrn (k) (w) ⟼ s (f))⟩\} = \{⟨\cdot_{ndx}, (s \in TEndo (K) (w), f \in LTrn (K) (w) ⟼ s (f))⟩\}$
21	14 20	uneq12d	$⊢ k = K \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}, 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))⟩\}$
22	4 21	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ \{⟨{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))⟩\})$
23		df-dveca	$⊢ DVecA = (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{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))⟩\}))$
24	22 23 1	mptfvmpt	$⊢ K \in V \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))⟩\})$
25	2 24	syl	$⊢ K \in V \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))⟩\})$

Metamath Proof Explorer

Theorem dvafset

Proof