Metamath Proof Explorer


Theorem erngbase

Description: The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom W ). TODO: the .t hypothesis isn't used. (Also look at others.) (Contributed by NM, 9-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
erng.c C = Base D
Assertion erngbase K V W H C = E

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 erng.c C = Base D
6 1 2 3 4 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
7 6 fveq2d K V W H Base D = Base Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
8 3 fvexi E V
9 eqid Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t = Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
10 9 rngbase E V E = Base Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
11 8 10 ax-mp E = Base Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
12 7 5 11 3eqtr4g K V W H C = E