Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Axiomatization of complex pre-Hilbert spaces
Vector operations
hv2times
Next ⟩
hvnegdii
Metamath Proof Explorer
Ascii
Unicode
Theorem
hv2times
Description:
Two times a vector.
(Contributed by
NM
, 22-Jun-2006)
(New usage is discouraged.)
Ref
Expression
Assertion
hv2times
⊢
A
∈
ℋ
→
2
⋅
ℎ
A
=
A
+
ℎ
A
Proof
Step
Hyp
Ref
Expression
1
df-2
⊢
2
=
1
+
1
2
1
oveq1i
⊢
2
⋅
ℎ
A
=
1
+
1
⋅
ℎ
A
3
ax-1cn
⊢
1
∈
ℂ
4
ax-hvdistr2
⊢
1
∈
ℂ
∧
1
∈
ℂ
∧
A
∈
ℋ
→
1
+
1
⋅
ℎ
A
=
1
⋅
ℎ
A
+
ℎ
1
⋅
ℎ
A
5
3
3
4
mp3an12
⊢
A
∈
ℋ
→
1
+
1
⋅
ℎ
A
=
1
⋅
ℎ
A
+
ℎ
1
⋅
ℎ
A
6
2
5
syl5eq
⊢
A
∈
ℋ
→
2
⋅
ℎ
A
=
1
⋅
ℎ
A
+
ℎ
1
⋅
ℎ
A
7
ax-hvdistr1
⊢
1
∈
ℂ
∧
A
∈
ℋ
∧
A
∈
ℋ
→
1
⋅
ℎ
A
+
ℎ
A
=
1
⋅
ℎ
A
+
ℎ
1
⋅
ℎ
A
8
3
7
mp3an1
⊢
A
∈
ℋ
∧
A
∈
ℋ
→
1
⋅
ℎ
A
+
ℎ
A
=
1
⋅
ℎ
A
+
ℎ
1
⋅
ℎ
A
9
8
anidms
⊢
A
∈
ℋ
→
1
⋅
ℎ
A
+
ℎ
A
=
1
⋅
ℎ
A
+
ℎ
1
⋅
ℎ
A
10
hvaddcl
⊢
A
∈
ℋ
∧
A
∈
ℋ
→
A
+
ℎ
A
∈
ℋ
11
10
anidms
⊢
A
∈
ℋ
→
A
+
ℎ
A
∈
ℋ
12
ax-hvmulid
⊢
A
+
ℎ
A
∈
ℋ
→
1
⋅
ℎ
A
+
ℎ
A
=
A
+
ℎ
A
13
11
12
syl
⊢
A
∈
ℋ
→
1
⋅
ℎ
A
+
ℎ
A
=
A
+
ℎ
A
14
6
9
13
3eqtr2d
⊢
A
∈
ℋ
→
2
⋅
ℎ
A
=
A
+
ℎ
A