Metamath Proof Explorer


Theorem erngset

Description: The division ring on trace-preserving endomorphisms for a fiducial co-atom W . (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypotheses erngset.h H = LHyp K
erngset.t T = LTrn K W
erngset.e E = TEndo K W
erngset.d D = EDRing K W
Assertion erngset K V W H D = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t

Proof

Step Hyp Ref Expression
1 erngset.h H = LHyp K
2 erngset.t T = LTrn K W
3 erngset.e E = TEndo K W
4 erngset.d D = EDRing K W
5 1 erngfset K V EDRing 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 s t
6 5 fveq1d K V EDRing K W = 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 s t W
7 4 6 syl5eq K V D = 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 s t W
8 fveq2 w = W TEndo K w = TEndo K W
9 8 opeq2d w = W Base ndx TEndo K w = Base ndx TEndo K W
10 tpeq1 Base ndx TEndo K w = Base ndx TEndo K W 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 s t = 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 s t
11 3 opeq2i Base ndx E = Base ndx TEndo K W
12 tpeq1 Base ndx E = Base ndx TEndo K W Base ndx E + 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 s t = 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 s t
13 11 12 ax-mp Base ndx E + 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 s t = 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 s t
14 10 13 eqtr4di Base ndx TEndo K w = Base ndx TEndo K W 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 s t = Base ndx E + 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 s t
15 9 14 syl w = W 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 s t = Base ndx E + 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 s t
16 8 3 eqtr4di w = W TEndo K w = E
17 fveq2 w = W LTrn K w = LTrn K W
18 17 2 eqtr4di w = W LTrn K w = T
19 eqidd w = W s f t f = s f t f
20 18 19 mpteq12dv w = W f LTrn K w s f t f = f T s f t f
21 16 16 20 mpoeq123dv w = W s TEndo K w , t TEndo K w f LTrn K w s f t f = s E , t E f T s f t f
22 21 opeq2d w = W + ndx s TEndo K w , t TEndo K w f LTrn K w s f t f = + ndx s E , t E f T s f t f
23 22 tpeq2d w = W Base ndx E + 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 s t = Base ndx E + ndx s E , t E f T s f t f ndx s TEndo K w , t TEndo K w s t
24 eqidd w = W s t = s t
25 16 16 24 mpoeq123dv w = W s TEndo K w , t TEndo K w s t = s E , t E s t
26 25 opeq2d w = W ndx s TEndo K w , t TEndo K w s t = ndx s E , t E s t
27 26 tpeq3d w = W Base ndx E + ndx s E , t E f T s f t f ndx s TEndo K w , t TEndo K w s t = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
28 15 23 27 3eqtrd w = W 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 s t = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
29 eqid 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 s t = 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 s t
30 tpex Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t V
31 28 29 30 fvmpt W H 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 s t W = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
32 7 31 sylan9eq K V W H D = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t