Metamath Proof Explorer


Theorem 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 V EDRing R K = w H Base ndx TEndo K w + ndx s TEndo K w , t TEndo K w f LTrn K w s f t f ndx s TEndo K w , t TEndo K w t s

Proof

Step Hyp Ref Expression
1 erngset.h-r H = LHyp K
2 elex K V K V
3 fveq2 k = K LHyp k = LHyp K
4 3 1 eqtr4di k = K LHyp k = H
5 fveq2 k = K TEndo k = TEndo K
6 5 fveq1d k = K TEndo k w = TEndo K w
7 6 opeq2d k = K Base ndx TEndo k w = Base ndx TEndo K w
8 fveq2 k = K LTrn k = LTrn K
9 8 fveq1d k = K LTrn k w = LTrn K w
10 9 mpteq1d k = K f LTrn k w s f t f = f LTrn K w s f t f
11 6 6 10 mpoeq123dv k = K s TEndo k w , t TEndo k w f LTrn k w s f t f = s TEndo K w , t TEndo K w f LTrn K w s f t f
12 11 opeq2d k = K + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f = + ndx s TEndo K w , t TEndo K w f LTrn K w s f t f
13 eqidd k = K t s = t s
14 6 6 13 mpoeq123dv k = K s TEndo k w , t TEndo k w t s = s TEndo K w , t TEndo K w t s
15 14 opeq2d k = K ndx s TEndo k w , t TEndo k w t s = ndx s TEndo K w , t TEndo K w t s
16 7 12 15 tpeq123d k = K Base ndx TEndo k w + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f ndx s TEndo k w , t TEndo k w t s = Base ndx TEndo K w + ndx s TEndo K w , t TEndo K w f LTrn K w s f t f ndx s TEndo K w , t TEndo K w t s
17 4 16 mpteq12dv k = K w LHyp k Base ndx TEndo k w + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f ndx s TEndo k w , t TEndo k w t s = w H Base ndx TEndo K w + ndx s TEndo K w , t TEndo K w f LTrn K w s f t f ndx s TEndo K w , t TEndo K w t s
18 df-edring-rN EDRing R = k V w LHyp k Base ndx TEndo k w + ndx s TEndo k w , t TEndo k w f LTrn k w s f t f ndx s TEndo k w , t TEndo k w t s
19 17 18 1 mptfvmpt K V EDRing R K = w H Base ndx TEndo K w + ndx s TEndo K w , t TEndo K w f LTrn K w s f t f ndx s TEndo K w , t TEndo K w t s
20 2 19 syl K V EDRing R K = w H Base ndx TEndo K w + ndx s TEndo K w , t TEndo K w f LTrn K w s f t f ndx s TEndo K w , t TEndo K w t s