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=LHypK
erngset.t T=LTrnKW
erngset.e E=TEndoKW
erngset.d D=EDRingKW
Assertion erngset KVWHD=BasendxE+ndxsE,tEfTsftfndxsE,tEst

Proof

Step Hyp Ref Expression
1 erngset.h H=LHypK
2 erngset.t T=LTrnKW
3 erngset.e E=TEndoKW
4 erngset.d D=EDRingKW
5 1 erngfset KVEDRingK=wHBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst
6 5 fveq1d KVEDRingKW=wHBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwstW
7 4 6 eqtrid KVD=wHBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwstW
8 fveq2 w=WTEndoKw=TEndoKW
9 8 opeq2d w=WBasendxTEndoKw=BasendxTEndoKW
10 tpeq1 BasendxTEndoKw=BasendxTEndoKWBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst=BasendxTEndoKW+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst
11 3 opeq2i BasendxE=BasendxTEndoKW
12 tpeq1 BasendxE=BasendxTEndoKWBasendxE+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst=BasendxTEndoKW+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst
13 11 12 ax-mp BasendxE+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst=BasendxTEndoKW+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst
14 10 13 eqtr4di BasendxTEndoKw=BasendxTEndoKWBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst=BasendxE+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst
15 9 14 syl w=WBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst=BasendxE+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst
16 8 3 eqtr4di w=WTEndoKw=E
17 fveq2 w=WLTrnKw=LTrnKW
18 17 2 eqtr4di w=WLTrnKw=T
19 eqidd w=Wsftf=sftf
20 18 19 mpteq12dv w=WfLTrnKwsftf=fTsftf
21 16 16 20 mpoeq123dv w=WsTEndoKw,tTEndoKwfLTrnKwsftf=sE,tEfTsftf
22 21 opeq2d w=W+ndxsTEndoKw,tTEndoKwfLTrnKwsftf=+ndxsE,tEfTsftf
23 22 tpeq2d w=WBasendxE+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst=BasendxE+ndxsE,tEfTsftfndxsTEndoKw,tTEndoKwst
24 eqidd w=Wst=st
25 16 16 24 mpoeq123dv w=WsTEndoKw,tTEndoKwst=sE,tEst
26 25 opeq2d w=WndxsTEndoKw,tTEndoKwst=ndxsE,tEst
27 26 tpeq3d w=WBasendxE+ndxsE,tEfTsftfndxsTEndoKw,tTEndoKwst=BasendxE+ndxsE,tEfTsftfndxsE,tEst
28 15 23 27 3eqtrd w=WBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst=BasendxE+ndxsE,tEfTsftfndxsE,tEst
29 eqid wHBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst=wHBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwst
30 tpex BasendxE+ndxsE,tEfTsftfndxsE,tEstV
31 28 29 30 fvmpt WHwHBasendxTEndoKw+ndxsTEndoKw,tTEndoKwfLTrnKwsftfndxsTEndoKw,tTEndoKwstW=BasendxE+ndxsE,tEfTsftfndxsE,tEst
32 7 31 sylan9eq KVWHD=BasendxE+ndxsE,tEfTsftfndxsE,tEst