dvaabl

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

	Ref	Expression
Hypotheses	dvalvec.h	$⊢ H = LHyp (K)$
	dvalvec.v	$⊢ U = DVecA (K) (W)$
Assertion	dvaabl	$⊢ (K \in HL \land W \in H) \to U \in Abel$

Proof

Step	Hyp	Ref	Expression
1		dvalvec.h	$⊢ H = LHyp (K)$
2		dvalvec.v	$⊢ U = DVecA (K) (W)$
3		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
4		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
5		eqid	$⊢ EDRing (K) (W) = EDRing (K) (W)$
6	1 3 4 5 2	dvaset	$⊢ (K \in HL \land W \in H) \to U = \{⟨{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		eqid	$⊢ TGrp (K) (W) = TGrp (K) (W)$
8	1 3 7	tgrpset	$⊢ (K \in HL \land W \in H) \to TGrp (K) (W) = \{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}$
9	1 7	tgrpabl	$⊢ (K \in HL \land W \in H) \to TGrp (K) (W) \in Abel$
10	8 9	eqeltrrd	$⊢ (K \in HL \land W \in H) \to \{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\} \in Abel$
11		fvex	$⊢ LTrn (K) (W) \in V$
12		eqid	$⊢ \{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\} = \{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}$
13	12	grpbase	$⊢ LTrn (K) (W) \in V \to LTrn (K) (W) = {Base}_{\{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}}$
14		eqid	$⊢ \{⟨{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))⟩\}$
15	14	lmodbase	$⊢ LTrn (K) (W) \in V \to LTrn (K) (W) = {Base}_{(\{⟨{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))⟩\})}$
16	13 15	eqtr3d	$⊢ LTrn (K) (W) \in V \to {Base}_{\{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}} = {Base}_{(\{⟨{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))⟩\})}$
17	11 16	ax-mp	$⊢ {Base}_{\{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}} = {Base}_{(\{⟨{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))⟩\})}$
18	11 11	mpoex	$⊢ (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g) \in V$
19	12	grpplusg	$⊢ (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g) \in V \to (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g) = +_{\{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}}$
20	14	lmodplusg	$⊢ (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g) \in V \to (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g) = +_{(\{⟨{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))⟩\})}$
21	19 20	eqtr3d	$⊢ (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g) \in V \to +_{\{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}} = +_{(\{⟨{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	18 21	ax-mp	$⊢ +_{\{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}} = +_{(\{⟨{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	17 22	ablprop	$⊢ \{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\} \in Abel \leftrightarrow \{⟨{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))⟩\} \in Abel$
24	10 23	sylib	$⊢ (K \in HL \land W \in H) \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))⟩\} \in Abel$
25	6 24	eqeltrd	$⊢ (K \in HL \land W \in H) \to U \in Abel$

Metamath Proof Explorer

Theorem dvaabl

Proof