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=EDRingR⁡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=EDRingR⁡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