Metamath Proof Explorer


Theorem erngplus-rN

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

Ref Expression
Hypotheses erngset.h-r H = LHyp K
erngset.t-r T = LTrn K W
erngset.e-r E = TEndo K W
erngset.d-r D = EDRing R K W
erng.p-r + ˙ = + D
Assertion erngplus-rN K HL W H U E V E U + ˙ V = f T U f V f

Proof

Step Hyp Ref Expression
1 erngset.h-r H = LHyp K
2 erngset.t-r T = LTrn K W
3 erngset.e-r E = TEndo K W
4 erngset.d-r D = EDRing R K W
5 erng.p-r + ˙ = + D
6 1 2 3 4 5 erngfplus-rN K HL W H + ˙ = s E , t E g T s g t g
7 6 oveqd K HL W H U + ˙ V = U s E , t E g T s g t g V
8 eqid s E , t E g T s g t g = s E , t E g T s g t g
9 8 2 tendopl U E V E U s E , t E g T s g t g V = f T U f V f
10 7 9 sylan9eq K HL W H U E V E U + ˙ V = f T U f V f