dvhfset

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

		Ref	Expression
	Hypothesis	dvhset.h	$⊢ H = LHyp (K)$
	Assertion	dvhfset	$⊢ K \in V \to DVecH (K) = (w \in H ⟼ \{⟨{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), EDRing (K) (w)⟩\} \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)⟩)⟩\})$

Proof

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

Metamath Proof Explorer

Theorem dvhfset

Proof