Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
dvhvaddcbv
Next ⟩
dvhvaddval
Metamath Proof Explorer
Ascii
Unicode
Theorem
dvhvaddcbv
Description:
Change bound variables to isolate them later.
(Contributed by
NM
, 3-Nov-2013)
Ref
Expression
Hypothesis
dvhvaddval.a
⊢
+
˙
=
f
∈
T
×
E
,
g
∈
T
×
E
⟼
1
st
⁡
f
∘
1
st
⁡
g
2
nd
⁡
f
⨣
˙
2
nd
⁡
g
Assertion
dvhvaddcbv
⊢
+
˙
=
h
∈
T
×
E
,
i
∈
T
×
E
⟼
1
st
⁡
h
∘
1
st
⁡
i
2
nd
⁡
h
⨣
˙
2
nd
⁡
i
Proof
Step
Hyp
Ref
Expression
1
dvhvaddval.a
⊢
+
˙
=
f
∈
T
×
E
,
g
∈
T
×
E
⟼
1
st
⁡
f
∘
1
st
⁡
g
2
nd
⁡
f
⨣
˙
2
nd
⁡
g
2
fveq2
⊢
f
=
h
→
1
st
⁡
f
=
1
st
⁡
h
3
2
coeq1d
⊢
f
=
h
→
1
st
⁡
f
∘
1
st
⁡
g
=
1
st
⁡
h
∘
1
st
⁡
g
4
fveq2
⊢
f
=
h
→
2
nd
⁡
f
=
2
nd
⁡
h
5
4
oveq1d
⊢
f
=
h
→
2
nd
⁡
f
⨣
˙
2
nd
⁡
g
=
2
nd
⁡
h
⨣
˙
2
nd
⁡
g
6
3
5
opeq12d
⊢
f
=
h
→
1
st
⁡
f
∘
1
st
⁡
g
2
nd
⁡
f
⨣
˙
2
nd
⁡
g
=
1
st
⁡
h
∘
1
st
⁡
g
2
nd
⁡
h
⨣
˙
2
nd
⁡
g
7
fveq2
⊢
g
=
i
→
1
st
⁡
g
=
1
st
⁡
i
8
7
coeq2d
⊢
g
=
i
→
1
st
⁡
h
∘
1
st
⁡
g
=
1
st
⁡
h
∘
1
st
⁡
i
9
fveq2
⊢
g
=
i
→
2
nd
⁡
g
=
2
nd
⁡
i
10
9
oveq2d
⊢
g
=
i
→
2
nd
⁡
h
⨣
˙
2
nd
⁡
g
=
2
nd
⁡
h
⨣
˙
2
nd
⁡
i
11
8
10
opeq12d
⊢
g
=
i
→
1
st
⁡
h
∘
1
st
⁡
g
2
nd
⁡
h
⨣
˙
2
nd
⁡
g
=
1
st
⁡
h
∘
1
st
⁡
i
2
nd
⁡
h
⨣
˙
2
nd
⁡
i
12
6
11
cbvmpov
⊢
f
∈
T
×
E
,
g
∈
T
×
E
⟼
1
st
⁡
f
∘
1
st
⁡
g
2
nd
⁡
f
⨣
˙
2
nd
⁡
g
=
h
∈
T
×
E
,
i
∈
T
×
E
⟼
1
st
⁡
h
∘
1
st
⁡
i
2
nd
⁡
h
⨣
˙
2
nd
⁡
i
13
1
12
eqtri
⊢
+
˙
=
h
∈
T
×
E
,
i
∈
T
×
E
⟼
1
st
⁡
h
∘
1
st
⁡
i
2
nd
⁡
h
⨣
˙
2
nd
⁡
i