dvhset

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
Hypotheses	dvhset.h	$⊢ H = LHyp (K)$
	dvhset.t	$⊢ T = LTrn (K) (W)$
	dvhset.e	$⊢ E = TEndo (K) (W)$
	dvhset.d	$⊢ D = EDRing (K) (W)$
	dvhset.u	$⊢ U = DVecH (K) (W)$
Assertion	dvhset	$⊢ (K \in X \land W \in H) \to U = \{⟨{Base}_{ndx}, T \times E⟩, ⟨+_{ndx}, (f \in (T \times E), g \in (T \times E) ⟼ ⟨1^{st} (f) \circ 1^{st} (g), (h \in T ⟼ 2^{nd} (f) (h) \circ 2^{nd} (g) (h))⟩)⟩, ⟨Scalar (ndx), D⟩\} \cup \{⟨\cdot_{ndx}, (s \in E, f \in (T \times E) ⟼ ⟨s (1^{st} (f)), s \circ 2^{nd} (f)⟩)⟩\}$

Proof

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

Metamath Proof Explorer

Theorem dvhset

Proof