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