P. 316 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 31501-31600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hvsubvali 31501	Value of vector subtraction definition. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 −ℎ 𝐵) = (𝐴 +ℎ (-1 ·ℎ 𝐵))
Theorem	hvsubcli 31502	Closure of vector subtraction. (Contributed by NM, 2-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 −ℎ 𝐵) ∈ ℋ
Theorem	ifhvhv0 31503	Prove if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ. (Contributed by David A. Wheeler, 7-Dec-2018.) (New usage is discouraged.)
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈ ℋ
Theorem	hvaddlid 31504	Addition with the zero vector. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0ℎ +ℎ 𝐴) = 𝐴)
Theorem	hvmul0 31505	Scalar multiplication with the zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℂ → (𝐴 ·ℎ 0ℎ) = 0ℎ)
Theorem	hvmul0or 31506	If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) = 0ℎ ↔ (𝐴 = 0 ∨ 𝐵 = 0ℎ)))
Theorem	hvsubid 31507	Subtraction of a vector from itself. (Contributed by NM, 30-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 𝐴) = 0ℎ)
Theorem	hvnegid 31508	Addition of negative of a vector to itself. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ)
Theorem	hv2neg 31509	Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴))
Theorem	hvaddlidi 31510	Addition with the zero vector. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (0ℎ +ℎ 𝐴) = 𝐴
Theorem	hvnegidi 31511	Addition of negative of a vector to itself. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ (-1 ·ℎ 𝐴)) = 0ℎ
Theorem	hv2negi 31512	Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    ⇒   ⊢ (0ℎ −ℎ 𝐴) = (-1 ·ℎ 𝐴)
Theorem	hvm1neg 31513	Convert minus one times a scalar product to the negative of the scalar. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (-1 ·ℎ (𝐴 ·ℎ 𝐵)) = (-𝐴 ·ℎ 𝐵))
Theorem	hvaddsubval 31514	Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐴 −ℎ (-1 ·ℎ 𝐵)))
Theorem	hvadd32 31515	Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵))
Theorem	hvadd12 31516	Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶)))
Theorem	hvadd4 31517	Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷)))
Theorem	hvsub4 31518	Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ 𝐷)))
Theorem	hvaddsub12 31519	Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐶)) = (𝐵 +ℎ (𝐴 −ℎ 𝐶)))
Theorem	hvpncan 31520	Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐵) = 𝐴)
Theorem	hvpncan2 31521	Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐴) = 𝐵)
Theorem	hvaddsubass 31522	Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐶) = (𝐴 +ℎ (𝐵 −ℎ 𝐶)))
Theorem	hvpncan3 31523	Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐴)) = 𝐵)
Theorem	hvmulcom 31524	Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶)))
Theorem	hvsubass 31525	Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = (𝐴 −ℎ (𝐵 +ℎ 𝐶)))
Theorem	hvsub32 31526	Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = ((𝐴 −ℎ 𝐶) −ℎ 𝐵))
Theorem	hvmulassi 31527	Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
Theorem	hvmulcomi 31528	Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶))
Theorem	hvmul2negi 31529	Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (-𝐴 ·ℎ (-𝐵 ·ℎ 𝐶)) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶))
Theorem	hvsubdistr1 31530	Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶)))
Theorem	hvsubdistr2 31531	Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 − 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) −ℎ (𝐵 ·ℎ 𝐶)))
Theorem	hvdistr1i 31532	Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶))
Theorem	hvsubdistr1i 31533	Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶))
Theorem	hvassi 31534	Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))
Theorem	hvadd32i 31535	Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵)
Theorem	hvsubassi 31536	Hilbert vector space associative law for subtraction. (Contributed by NM, 7-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = (𝐴 −ℎ (𝐵 +ℎ 𝐶))
Theorem	hvsub32i 31537	Hilbert vector space commutative/associative law. (Contributed by NM, 7-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = ((𝐴 −ℎ 𝐶) −ℎ 𝐵)
Theorem	hvadd12i 31538	Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶))
Theorem	hvadd4i 31539	Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷))
Theorem	hvsubsub4i 31540	Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷))
Theorem	hvsubsub4 31541	Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷)))
Theorem	hv2times 31542	Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (2 ·ℎ 𝐴) = (𝐴 +ℎ 𝐴))
Theorem	hvnegdii 31543	Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴)
Theorem	hvsubeq0i 31544	If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵)
Theorem	hvsubcan2i 31545	Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐴 −ℎ 𝐵)) = (2 ·ℎ 𝐴)
Theorem	hvaddcani 31546	Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶)
Theorem	hvsubaddi 31547	Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) = 𝐶 ↔ (𝐵 +ℎ 𝐶) = 𝐴)
Theorem	hvnegdi 31548	Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴))
Theorem	hvsubeq0 31549	If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵))
Theorem	hvaddeq0 31550	If the sum of two vectors is zero, one is the negative of the other. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) = 0ℎ ↔ 𝐴 = (-1 ·ℎ 𝐵)))
Theorem	hvaddcan 31551	Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶))
Theorem	hvaddcan2 31552	Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐶) = (𝐵 +ℎ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	hvmulcan 31553	Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) = (𝐴 ·ℎ 𝐶) ↔ 𝐵 = 𝐶))
Theorem	hvmulcan2 31554	Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℋ ∧ 𝐶 ≠ 0ℎ)) → ((𝐴 ·ℎ 𝐶) = (𝐵 ·ℎ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	hvsubcan 31555	Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = (𝐴 −ℎ 𝐶) ↔ 𝐵 = 𝐶))
Theorem	hvsubcan2 31556	Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐶) = (𝐵 −ℎ 𝐶) ↔ 𝐴 = 𝐵))
Theorem	hvsub0 31557	Subtraction of a zero vector. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 0ℎ) = 𝐴)
Theorem	hvsubadd 31558	Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = 𝐶 ↔ (𝐵 +ℎ 𝐶) = 𝐴))
Theorem	hvaddsub4 31559	Hilbert vector space addition/subtraction law. (Contributed by NM, 18-May-2005.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) = (𝐶 +ℎ 𝐷) ↔ (𝐴 −ℎ 𝐶) = (𝐷 −ℎ 𝐵)))
20.1.6  Inner product postulates for a Hilbert space
Axiom	ax-hfi 31560	Inner product maps pairs from ℋ to ℂ. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ ·ih :( ℋ × ℋ)⟶ℂ
Theorem	hicl 31561	Closure of inner product. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) ∈ ℂ)
Theorem	hicli 31562	Closure inference for inner product. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ·ih 𝐵) ∈ ℂ
Axiom	ax-his1 31563	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that ∗‘𝑥 is the complex conjugate cjval 15189 of 𝑥. In the literature, the inner product of 𝐴 and 𝐵 is usually written ⟨𝐴, 𝐵⟩, but our operation notation co 7413 allows to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4591. Physicists use ⟨𝐵 ∣ 𝐴⟩, called Dirac bra-ket notation, to represent this operation; see comments in df-bra 32331. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴)))
Axiom	ax-his2 31564	Distributive law for inner product. Postulate (S2) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐶)))
Axiom	ax-his3 31565	Associative law for inner product. Postulate (S3) of [Beran] p. 95. Warning: Mathematics textbooks usually use our version of the axiom. Physics textbooks, on the other hand, usually replace the left-hand side with (𝐵 ·ih (𝐴 ·ℎ 𝐶)) (e.g., Equation 1.21b of [Hughes] p. 44; Definition (iii) of [ReedSimon] p. 36). See the comments in df-bra 32331 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶)))
Axiom	ax-his4 31566	Identity law for inner product. Postulate (S4) of [Beran] p. 95. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → 0 < (𝐴 ·ih 𝐴))
20.2  Inner product and norms
20.2.1  Inner product
Theorem	his5 31567	Associative law for inner product. Lemma 3.1(S5) of [Beran] p. 95. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ·ih (𝐴 ·ℎ 𝐶)) = ((∗‘𝐴) · (𝐵 ·ih 𝐶)))
Theorem	his52 31568	Associative law for inner product. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ·ih ((∗‘𝐴) ·ℎ 𝐶)) = (𝐴 · (𝐵 ·ih 𝐶)))
Theorem	his35 31569	Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ·ℎ 𝐶) ·ih (𝐵 ·ℎ 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 ·ih 𝐷)))
Theorem	his35i 31570	Move scalar multiplication to outside of inner product. (Contributed by NM, 1-Jul-2005.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 ·ℎ 𝐶) ·ih (𝐵 ·ℎ 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 ·ih 𝐷))
Theorem	his7 31571	Distributive law for inner product. Lemma 3.1(S7) of [Beran] p. 95. (Contributed by NM, 31-Jul-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ih (𝐵 +ℎ 𝐶)) = ((𝐴 ·ih 𝐵) + (𝐴 ·ih 𝐶)))
Theorem	hiassdi 31572	Distributive/associative law for inner product, useful for linearity proofs. (Contributed by NM, 10-May-2005.) (New usage is discouraged.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → (((𝐴 ·ℎ 𝐵) +ℎ 𝐶) ·ih 𝐷) = ((𝐴 · (𝐵 ·ih 𝐷)) + (𝐶 ·ih 𝐷)))
Theorem	his2sub 31573	Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) − (𝐵 ·ih 𝐶)))
Theorem	his2sub2 31574	Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ih (𝐵 −ℎ 𝐶)) = ((𝐴 ·ih 𝐵) − (𝐴 ·ih 𝐶)))
Theorem	hire 31575	A necessary and sufficient condition for an inner product to be real. (Contributed by NM, 2-Jul-2005.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) ∈ ℝ ↔ (𝐴 ·ih 𝐵) = (𝐵 ·ih 𝐴)))
Theorem	hiidrcl 31576	Real closure of inner product with self. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 ·ih 𝐴) ∈ ℝ)
Theorem	hi01 31577	Inner product with the 0 vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (0ℎ ·ih 𝐴) = 0)
Theorem	hi02 31578	Inner product with the 0 vector. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (𝐴 ·ih 0ℎ) = 0)
Theorem	hiidge0 31579	Inner product with self is not negative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·ih 𝐴))
Theorem	his6 31580	Zero inner product with self means vector is zero. Lemma 3.1(S6) of [Beran] p. 95. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → ((𝐴 ·ih 𝐴) = 0 ↔ 𝐴 = 0ℎ))
Theorem	his1i 31581	Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. (Contributed by NM, 15-May-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴))
Theorem	abshicom 31582	Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) = (abs‘(𝐵 ·ih 𝐴)))
Theorem	hial0 31583*	A vector whose inner product is always zero is zero. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (∀𝑥 ∈ ℋ (𝐴 ·ih 𝑥) = 0 ↔ 𝐴 = 0ℎ))
Theorem	hial02 31584*	A vector whose inner product is always zero is zero. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
⊢ (𝐴 ∈ ℋ → (∀𝑥 ∈ ℋ (𝑥 ·ih 𝐴) = 0 ↔ 𝐴 = 0ℎ))
Theorem	hisubcomi 31585	Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) ·ih (𝐶 −ℎ 𝐷)) = ((𝐵 −ℎ 𝐴) ·ih (𝐷 −ℎ 𝐶))
Theorem	hi2eq 31586	Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih (𝐴 −ℎ 𝐵)) = (𝐵 ·ih (𝐴 −ℎ 𝐵)) ↔ 𝐴 = 𝐵))
Theorem	hial2eq 31587*	Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ (𝐴 ·ih 𝑥) = (𝐵 ·ih 𝑥) ↔ 𝐴 = 𝐵))
Theorem	hial2eq2 31588*	Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ (𝑥 ·ih 𝐴) = (𝑥 ·ih 𝐵) ↔ 𝐴 = 𝐵))
Theorem	orthcom 31589	Orthogonality commutes. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 ↔ (𝐵 ·ih 𝐴) = 0))
Theorem	normlem0 31590	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 7-Oct-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    ⇒   ⊢ ((𝐹 −ℎ (𝑆 ·ℎ 𝐺)) ·ih (𝐹 −ℎ (𝑆 ·ℎ 𝐺))) = (((𝐹 ·ih 𝐹) + (-(∗‘𝑆) · (𝐹 ·ih 𝐺))) + ((-𝑆 · (𝐺 ·ih 𝐹)) + ((𝑆 · (∗‘𝑆)) · (𝐺 ·ih 𝐺))))
Theorem	normlem1 31591	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 22-Aug-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ ((𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺)) ·ih (𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺))) = (((𝐹 ·ih 𝐹) + (((∗‘𝑆) · -𝑅) · (𝐹 ·ih 𝐺))) + (((𝑆 · -𝑅) · (𝐺 ·ih 𝐹)) + ((𝑅↑2) · (𝐺 ·ih 𝐺))))
Theorem	normlem2 31592	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 27-Jul-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    ⇒   ⊢ 𝐵 ∈ ℝ
Theorem	normlem3 31593	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    &   ⊢ 𝐴 = (𝐺 ·ih 𝐺)    &   ⊢ 𝐶 = (𝐹 ·ih 𝐹)    &   ⊢ 𝑅 ∈ ℝ    ⇒   ⊢ (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶) = (((𝐹 ·ih 𝐹) + (((∗‘𝑆) · -𝑅) · (𝐹 ·ih 𝐺))) + (((𝑆 · -𝑅) · (𝐺 ·ih 𝐹)) + ((𝑅↑2) · (𝐺 ·ih 𝐺))))
Theorem	normlem4 31594	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    &   ⊢ 𝐴 = (𝐺 ·ih 𝐺)    &   ⊢ 𝐶 = (𝐹 ·ih 𝐹)    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ ((𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺)) ·ih (𝐹 −ℎ ((𝑆 · 𝑅) ·ℎ 𝐺))) = (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶)
Theorem	normlem5 31595	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 10-Aug-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    &   ⊢ 𝐴 = (𝐺 ·ih 𝐺)    &   ⊢ 𝐶 = (𝐹 ·ih 𝐹)    &   ⊢ 𝑅 ∈ ℝ    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ 0 ≤ (((𝐴 · (𝑅↑2)) + (𝐵 · 𝑅)) + 𝐶)
Theorem	normlem6 31596	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 2-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ 𝐵 = -(((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹)))    &   ⊢ 𝐴 = (𝐺 ·ih 𝐺)    &   ⊢ 𝐶 = (𝐹 ·ih 𝐹)    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ (abs‘𝐵) ≤ (2 · ((√‘𝐴) · (√‘𝐶)))
Theorem	normlem7 31597	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Aug-1999.) (New usage is discouraged.)
⊢ 𝑆 ∈ ℂ    &   ⊢ 𝐹 ∈ ℋ    &   ⊢ 𝐺 ∈ ℋ    &   ⊢ (abs‘𝑆) = 1    ⇒   ⊢ (((∗‘𝑆) · (𝐹 ·ih 𝐺)) + (𝑆 · (𝐺 ·ih 𝐹))) ≤ (2 · ((√‘(𝐺 ·ih 𝐺)) · (√‘(𝐹 ·ih 𝐹))))
Theorem	normlem8 31598	Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 +ℎ 𝐵) ·ih (𝐶 +ℎ 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) + ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))
Theorem	normlem9 31599	Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    &   ⊢ 𝐶 ∈ ℋ    &   ⊢ 𝐷 ∈ ℋ    ⇒   ⊢ ((𝐴 −ℎ 𝐵) ·ih (𝐶 −ℎ 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) − ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶)))
Theorem	normlem7tALT 31600	Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of [Beran] p. 97. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℋ    &   ⊢ 𝐵 ∈ ℋ    ⇒   ⊢ ((𝑆 ∈ ℂ ∧ (abs‘𝑆) = 1) → (((∗‘𝑆) · (𝐴 ·ih 𝐵)) + (𝑆 · (𝐵 ·ih 𝐴))) ≤ (2 · ((√‘(𝐵 ·ih 𝐵)) · (√‘(𝐴 ·ih 𝐴)))))