Metamath Proof Explorer


Theorem erngplus

Description: Ring addition operation. (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses erngset.h H=LHypK
erngset.t T=LTrnKW
erngset.e E=TEndoKW
erngset.d D=EDRingKW
erng.p +˙=+D
Assertion erngplus KHLWHUEVEU+˙V=fTUfVf

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 erng.p +˙=+D
6 1 2 3 4 5 erngfplus KHLWH+˙=sE,tEgTsgtg
7 6 oveqd KHLWHU+˙V=UsE,tEgTsgtgV
8 eqid sE,tEgTsgtg=sE,tEgTsgtg
9 8 2 tendopl UEVEUsE,tEgTsgtgV=fTUfVf
10 7 9 sylan9eq KHLWHUEVEU+˙V=fTUfVf