Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
erngfmul
Next ⟩
erngmul
Metamath Proof Explorer
Ascii
Unicode
Theorem
erngfmul
Description:
Ring multiplication 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.m
⊢
·
˙
=
⋅
D
Assertion
erngfmul
⊢
K
∈
V
∧
W
∈
H
→
·
˙
=
s
∈
E
,
t
∈
E
⟼
s
∘
t
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.m
⊢
·
˙
=
⋅
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
⟼
s
∘
t
∈
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
rngmulr
⊢
s
∈
E
,
t
∈
E
⟼
s
∘
t
∈
V
→
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
12
9
11
ax-mp
⊢
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
13
7
5
12
3eqtr4g
⊢
K
∈
V
∧
W
∈
H
→
·
˙
=
s
∈
E
,
t
∈
E
⟼
s
∘
t