Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
erngplus-rN
Next ⟩
erngplus2-rN
Metamath Proof Explorer
Ascii
Unicode
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