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 | |
|
erngset.t | |
||
erngset.e | |
||
erngset.d | |
||
Assertion | erngset | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | erngset.h | |
|
2 | erngset.t | |
|
3 | erngset.e | |
|
4 | erngset.d | |
|
5 | 1 | erngfset | |
6 | 5 | fveq1d | |
7 | 4 6 | eqtrid | |
8 | fveq2 | |
|
9 | 8 | opeq2d | |
10 | tpeq1 | |
|
11 | 3 | opeq2i | |
12 | tpeq1 | |
|
13 | 11 12 | ax-mp | |
14 | 10 13 | eqtr4di | |
15 | 9 14 | syl | |
16 | 8 3 | eqtr4di | |
17 | fveq2 | |
|
18 | 17 2 | eqtr4di | |
19 | eqidd | |
|
20 | 18 19 | mpteq12dv | |
21 | 16 16 20 | mpoeq123dv | |
22 | 21 | opeq2d | |
23 | 22 | tpeq2d | |
24 | eqidd | |
|
25 | 16 16 24 | mpoeq123dv | |
26 | 25 | opeq2d | |
27 | 26 | tpeq3d | |
28 | 15 23 27 | 3eqtrd | |
29 | eqid | |
|
30 | tpex | |
|
31 | 28 29 30 | fvmpt | |
32 | 7 31 | sylan9eq | |