Metamath Proof Explorer


Theorem erngplus2-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 erngplus2-rN K HL W H U E V E F T U + ˙ V F = 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 erngplus-rN K HL W H U E V E U + ˙ V = f T U f V f
7 6 3adantr3 K HL W H U E V E F T U + ˙ V = f T U f V f
8 fveq2 f = F U f = U F
9 fveq2 f = F V f = V F
10 8 9 coeq12d f = F U f V f = U F V F
11 10 adantl K HL W H U E V E F T f = F U f V f = U F V F
12 simpr3 K HL W H U E V E F T F T
13 fvex U F V
14 fvex V F V
15 13 14 coex U F V F V
16 15 a1i K HL W H U E V E F T U F V F V
17 7 11 12 16 fvmptd K HL W H U E V E F T U + ˙ V F = U F V F