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