Metamath Proof Explorer


Theorem erngfplus

Description: Ring addition operation. (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.p + ˙ = + D
Assertion erngfplus K V W H + ˙ = s E , t E f T s f t f

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.p + ˙ = + 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 + D = + 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 8 8 mpoex s E , t E f T s f t f V
10 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
11 10 rngplusg s E , t E f T s f t f V s E , t E f T s f t f = + Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
12 9 11 ax-mp s E , t E f T s f t f = + Base ndx E + ndx s E , t E f T s f t f ndx s E , t E s t
13 7 5 12 3eqtr4g K V W H + ˙ = s E , t E f T s f t f