erngfset-rN

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

		Ref	Expression
	Hypothesis	erngset.h-r	$⊢ H = LHyp (K)$
	Assertion	erngfset-rN	$⊢ K \in V \to {EDRing}_{R} (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) ⟼ t \circ s)⟩\})$

Proof

Step	Hyp	Ref	Expression
1		erngset.h-r	$⊢ 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 t \circ s = t \circ s$
14	6 6 13	mpoeq123dv	$⊢ k = K \to (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ t \circ s) = (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)$
15	14	opeq2d	$⊢ k = K \to ⟨\cdot_{ndx}, (s \in TEndo (k) (w), t \in TEndo (k) (w) ⟼ t \circ s)⟩ = ⟨\cdot_{ndx}, (s \in TEndo (K) (w), t \in TEndo (K) (w) ⟼ t \circ s)⟩$
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) ⟼ t \circ s)⟩\} = \{⟨{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) ⟼ t \circ s)⟩\}$
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) ⟼ t \circ s)⟩\}) = (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) ⟼ t \circ s)⟩\})$
18		df-edring-rN	$⊢ {EDRing}_{R} = (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) ⟼ t \circ s)⟩\}))$
19	17 18 1	mptfvmpt	$⊢ K \in V \to {EDRing}_{R} (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) ⟼ t \circ s)⟩\})$
20	2 19	syl	$⊢ K \in V \to {EDRing}_{R} (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) ⟼ t \circ s)⟩\})$

Metamath Proof Explorer

Theorem erngfset-rN

Proof