Metamath Proof Explorer


Theorem erngplus2

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 erngplus2 KHLWHUEVEFTU+˙VF=UFVF

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 erngplus KHLWHUEVEU+˙V=fTUfVf
7 6 3adantr3 KHLWHUEVEFTU+˙V=fTUfVf
8 fveq2 f=FUf=UF
9 fveq2 f=FVf=VF
10 8 9 coeq12d f=FUfVf=UFVF
11 10 adantl KHLWHUEVEFTf=FUfVf=UFVF
12 simpr3 KHLWHUEVEFTFT
13 fvex UFV
14 fvex VFV
15 13 14 coex UFVFV
16 15 a1i KHLWHUEVEFTUFVFV
17 7 11 12 16 fvmptd KHLWHUEVEFTU+˙VF=UFVF