Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Construction of a vector space from a Hilbert lattice
dvhvscacbv
Next ⟩
dvhvscaval
Metamath Proof Explorer
Ascii
Unicode
Theorem
dvhvscacbv
Description:
Change bound variables to isolate them later.
(Contributed by
NM
, 20-Nov-2013)
Ref
Expression
Hypothesis
dvhvscaval.s
⊢
·
˙
=
s
∈
E
,
f
∈
T
×
E
⟼
s
⁡
1
st
⁡
f
s
∘
2
nd
⁡
f
Assertion
dvhvscacbv
⊢
·
˙
=
t
∈
E
,
g
∈
T
×
E
⟼
t
⁡
1
st
⁡
g
t
∘
2
nd
⁡
g
Proof
Step
Hyp
Ref
Expression
1
dvhvscaval.s
⊢
·
˙
=
s
∈
E
,
f
∈
T
×
E
⟼
s
⁡
1
st
⁡
f
s
∘
2
nd
⁡
f
2
fveq1
⊢
s
=
t
→
s
⁡
1
st
⁡
f
=
t
⁡
1
st
⁡
f
3
coeq1
⊢
s
=
t
→
s
∘
2
nd
⁡
f
=
t
∘
2
nd
⁡
f
4
2
3
opeq12d
⊢
s
=
t
→
s
⁡
1
st
⁡
f
s
∘
2
nd
⁡
f
=
t
⁡
1
st
⁡
f
t
∘
2
nd
⁡
f
5
2fveq3
⊢
f
=
g
→
t
⁡
1
st
⁡
f
=
t
⁡
1
st
⁡
g
6
fveq2
⊢
f
=
g
→
2
nd
⁡
f
=
2
nd
⁡
g
7
6
coeq2d
⊢
f
=
g
→
t
∘
2
nd
⁡
f
=
t
∘
2
nd
⁡
g
8
5
7
opeq12d
⊢
f
=
g
→
t
⁡
1
st
⁡
f
t
∘
2
nd
⁡
f
=
t
⁡
1
st
⁡
g
t
∘
2
nd
⁡
g
9
4
8
cbvmpov
⊢
s
∈
E
,
f
∈
T
×
E
⟼
s
⁡
1
st
⁡
f
s
∘
2
nd
⁡
f
=
t
∈
E
,
g
∈
T
×
E
⟼
t
⁡
1
st
⁡
g
t
∘
2
nd
⁡
g
10
1
9
eqtri
⊢
·
˙
=
t
∈
E
,
g
∈
T
×
E
⟼
t
⁡
1
st
⁡
g
t
∘
2
nd
⁡
g