erngfset

Description: The division rings on trace-preserving endomorphisms for a lattice K . (Contributed by NM, 8-Jun-2013)

		Ref	Expression
	Hypothesis	erngset.h	$⊢ H = LHyp (K)$
	Assertion	erngfset	$⊢ K \in V \to EDRing (K) = (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ s \circ t)⟩\})$

Proof

Step	Hyp	Ref	Expression
1		erngset.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 TEndo (k) = TEndo (K)$
6	5	fveq1d	$⊢ k = K \to TEndo (k) (w) = TEndo (K) (w)$
7	6	opeq2d	$⊢ k = K \to ⟨{Base}_{ndx}, TEndo (k) (w)⟩ = ⟨{Base}_{ndx}, TEndo (K) (w)⟩$
8		fveq2	$⊢ k = K \to LTrn (k) = LTrn (K)$
9	8	fveq1d	$⊢ k = K \to LTrn (k) (w) = LTrn (K) (w)$
10	9	mpteq1d	$⊢ k = K \to (f \in LTrn (k) (w) ⟼ s (f) \circ t (f)) = (f \in LTrn (K) (w) ⟼ s (f) \circ t (f))$
11	6 6 10	mpoeq123dv	$⊢ k = K \to (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ (f \in LTrn (k) (w) ⟼ s (f) \circ t (f))) = (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))$
12	11	opeq2d	$⊢ k = K \to ⟨+_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ (f \in LTrn (k) (w) ⟼ s (f) \circ t (f)))⟩ = ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩$
13		eqidd	$⊢ k = K \to s \circ t = s \circ t$
14	6 6 13	mpoeq123dv	$⊢ k = K \to (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ s \circ t) = (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ s \circ t)$
15	14	opeq2d	$⊢ k = K \to ⟨\cdot_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ s \circ t)⟩ = ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ s \circ t)⟩$
16	7 12 15	tpeq123d	$⊢ k = K \to \{⟨{Base}_{ndx}, TEndo (k) (w)⟩, ⟨+_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ (f \in LTrn (k) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ s \circ t)⟩\} = \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ s \circ t)⟩\}$
17	4 16	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, TEndo (k) (w)⟩, ⟨+_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ (f \in LTrn (k) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ s \circ t)⟩\}) = (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ s \circ t)⟩\})$
18		df-edring	$⊢ EDRing = (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, TEndo (k) (w)⟩, ⟨+_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ (f \in LTrn (k) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ s \circ t)⟩\}))$
19	17 18 1	mptfvmpt	$⊢ K \in V \to EDRing (K) = (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ s \circ t)⟩\})$
20	2 19	syl	$⊢ K \in V \to EDRing (K) = (w \in H ⟼ \{⟨{Base}_{ndx}, TEndo (K) (w)⟩, ⟨+_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ (f \in LTrn (K) (w) ⟼ s (f) \circ t (f)))⟩, ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ s \circ t)⟩\})$

Metamath Proof Explorer

Theorem erngfset

Proof