This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED) Complex vector spaces Examples of complex vector spaces cncvcOLD
Description: Obsolete version of cncvs . The set of complex numbers is a complex
vector space. The vector operation is + , and the scalar product is
x. . (Contributed by NM , 5-Nov-2006) (New usage is discouraged.)
(Proof modification is discouraged.)
Ref
Expression
Assertion
cncvcOLD ⊢ ⟨ + , · ⟩ ∈ CVecOLD
Proof
Step
Hyp
Ref
Expression
1
cnaddabloOLD ⊢ + ∈ AbelOp
2
ax-addf ⊢ + : ( ℂ × ℂ ) ⟶ ℂ
3
2
fdmi ⊢ dom + = ( ℂ × ℂ )
4
ax-mulf ⊢ · : ( ℂ × ℂ ) ⟶ ℂ
5
mullid ⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
6
adddi ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 · ( 𝑥 + 𝑧 ) ) = ( ( 𝑦 · 𝑥 ) + ( 𝑦 · 𝑧 ) ) )
7
adddir ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 + 𝑧 ) · 𝑥 ) = ( ( 𝑦 · 𝑥 ) + ( 𝑧 · 𝑥 ) ) )
8
mulass ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑦 · 𝑧 ) · 𝑥 ) = ( 𝑦 · ( 𝑧 · 𝑥 ) ) )
9
eqid ⊢ ⟨ + , · ⟩ = ⟨ + , · ⟩
10
1 3 4 5 6 7 8 9
isvciOLD ⊢ ⟨ + , · ⟩ ∈ CVecOLD