HomeTheorem List (p. 286 of 445)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 286 of 445) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-28386) |
Hilbert Space Explorer
(28387-29909) |
Users' Mathboxes
(29910-44411) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hvaddsubval 28501 | Value of vector addition in terms of vector subtraction. (Contributed by NM, 10-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ 𝐵) = (𝐴 −ℎ (-1 ·ℎ 𝐵))) | ||
| Theorem | hvadd32 28502 | Commutative/associative law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵)) | ||
| Theorem | hvadd12 28503 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶))) | ||
| Theorem | hvadd4 28504 | Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷))) | ||
| Theorem | hvsub4 28505 | Hilbert vector space addition/subtraction law. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) −ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) +ℎ (𝐵 −ℎ 𝐷))) | ||
| Theorem | hvaddsub12 28506 | Commutative/associative law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐶)) = (𝐵 +ℎ (𝐴 −ℎ 𝐶))) | ||
| Theorem | hvpncan 28507 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐵) = 𝐴) | ||
| Theorem | hvpncan2 28508 | Addition/subtraction cancellation law for vectors in Hilbert space. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐴) = 𝐵) | ||
| Theorem | hvaddsubass 28509 | Associativity of sum and difference of Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) −ℎ 𝐶) = (𝐴 +ℎ (𝐵 −ℎ 𝐶))) | ||
| Theorem | hvpncan3 28510 | Subtraction and addition of equal Hilbert space vectors. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℎ (𝐵 −ℎ 𝐴)) = 𝐵) | ||
| Theorem | hvmulcom 28511 | Scalar multiplication commutative law. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶))) | ||
| Theorem | hvsubass 28512 | Hilbert vector space associative law for subtraction. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = (𝐴 −ℎ (𝐵 +ℎ 𝐶))) | ||
| Theorem | hvsub32 28513 | Hilbert vector space commutative/associative law. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) −ℎ 𝐶) = ((𝐴 −ℎ 𝐶) −ℎ 𝐵)) | ||
| Theorem | hvmulassi 28514 | Scalar multiplication associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 · 𝐵) ·ℎ 𝐶) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
| Theorem | hvmulcomi 28515 | Scalar multiplication commutative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) = (𝐵 ·ℎ (𝐴 ·ℎ 𝐶)) | ||
| Theorem | hvmul2negi 28516 | Double negative in scalar multiplication. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (-𝐴 ·ℎ (-𝐵 ·ℎ 𝐶)) = (𝐴 ·ℎ (𝐵 ·ℎ 𝐶)) | ||
| Theorem | hvsubdistr1 28517 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶))) | ||
| Theorem | hvsubdistr2 28518 | Scalar multiplication distributive law for subtraction. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℋ) → ((𝐴 − 𝐵) ·ℎ 𝐶) = ((𝐴 ·ℎ 𝐶) −ℎ (𝐵 ·ℎ 𝐶))) | ||
| Theorem | hvdistr1i 28519 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 +ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) +ℎ (𝐴 ·ℎ 𝐶)) | ||
| Theorem | hvsubdistr1i 28520 | Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 ·ℎ (𝐵 −ℎ 𝐶)) = ((𝐴 ·ℎ 𝐵) −ℎ (𝐴 ·ℎ 𝐶)) | ||
| Theorem | hvassi 28521 | Hilbert vector space associative law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)) | ||
| Theorem | hvadd32i 28522 | Hilbert vector space commutative/associative law. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = ((𝐴 +ℎ 𝐶) +ℎ 𝐵) | ||
| Theorem | hvsubassi 28523 | 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 28524 | 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 28525 | Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ (𝐴 +ℎ (𝐵 +ℎ 𝐶)) = (𝐵 +ℎ (𝐴 +ℎ 𝐶)) | ||
| Theorem | hvadd4i 28526 | Hilbert vector space addition law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐶 +ℎ 𝐷)) = ((𝐴 +ℎ 𝐶) +ℎ (𝐵 +ℎ 𝐷)) | ||
| Theorem | hvsubsub4i 28527 | Hilbert vector space addition law. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷)) | ||
| Theorem | hvsubsub4 28528 | Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 −ℎ 𝐵) −ℎ (𝐶 −ℎ 𝐷)) = ((𝐴 −ℎ 𝐶) −ℎ (𝐵 −ℎ 𝐷))) | ||
| Theorem | hv2times 28529 | Two times a vector. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (2 ·ℎ 𝐴) = (𝐴 +ℎ 𝐴)) | ||
| Theorem | hvnegdii 28530 | Distribution of negative over subtraction. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴) | ||
| Theorem | hvsubeq0i 28531 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵) | ||
| Theorem | hvsubcan2i 28532 | Vector cancellation law. (Contributed by NM, 3-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐴 −ℎ 𝐵)) = (2 ·ℎ 𝐴) | ||
| Theorem | hvaddcani 28533 | Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶) | ||
| Theorem | hvsubaddi 28534 | Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) = 𝐶 ↔ (𝐵 +ℎ 𝐶) = 𝐴) | ||
| Theorem | hvnegdi 28535 | Distribution of negative over subtraction. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (-1 ·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴)) | ||
| Theorem | hvsubeq0 28536 | If the difference between two vectors is zero, they are equal. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = 0ℎ ↔ 𝐴 = 𝐵)) | ||
| Theorem | hvaddeq0 28537 | 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 28538 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) = (𝐴 +ℎ 𝐶) ↔ 𝐵 = 𝐶)) | ||
| Theorem | hvaddcan2 28539 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐶) = (𝐵 +ℎ 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | hvmulcan 28540 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) = (𝐴 ·ℎ 𝐶) ↔ 𝐵 = 𝐶)) | ||
| Theorem | hvmulcan2 28541 | Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℋ ∧ 𝐶 ≠ 0ℎ)) → ((𝐴 ·ℎ 𝐶) = (𝐵 ·ℎ 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | hvsubcan 28542 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = (𝐴 −ℎ 𝐶) ↔ 𝐵 = 𝐶)) | ||
| Theorem | hvsubcan2 28543 | Cancellation law for vector addition. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐶) = (𝐵 −ℎ 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | hvsub0 28544 | Subtraction of a zero vector. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐴 −ℎ 0ℎ) = 𝐴) | ||
| Theorem | hvsubadd 28545 | Relationship between vector subtraction and addition. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) = 𝐶 ↔ (𝐵 +ℎ 𝐶) = 𝐴)) | ||
| Theorem | hvaddsub4 28546 | Hilbert vector space addition/subtraction law. (Contributed by NM, 18-May-2005.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 +ℎ 𝐵) = (𝐶 +ℎ 𝐷) ↔ (𝐴 −ℎ 𝐶) = (𝐷 −ℎ 𝐵))) | ||
| Axiom | ax-hfi 28547 | Inner product maps pairs from ℋ to ℂ. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ ·ih :( ℋ × ℋ)⟶ℂ | ||
| Theorem | hicl 28548 | Closure of inner product. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) ∈ ℂ) | ||
| Theorem | hicli 28549 | Closure inference for inner product. (Contributed by NM, 1-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ·ih 𝐵) ∈ ℂ | ||
| Axiom | ax-his1 28550 | Conjugate law for inner product. Postulate (S1) of [Beran] p. 95. Note that ∗‘𝑥 is the complex conjugate cjval 14295 of 𝑥. In the literature, the inner product of 𝐴 and 𝐵 is usually written ⟨𝐴, 𝐵⟩, but our operation notation co 7016 allows us to use existing theorems about operations and also avoids a clash with the definition of an ordered pair df-op 4479. Physicists use ⟨𝐵 ∣ 𝐴⟩, called Dirac bra-ket notation, to represent this operation; see comments in df-bra 29318. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ·ih 𝐵) = (∗‘(𝐵 ·ih 𝐴))) | ||
| Axiom | ax-his2 28551 | 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 28552 | 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 29318 for why the physics definition is swapped. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ·ℎ 𝐵) ·ih 𝐶) = (𝐴 · (𝐵 ·ih 𝐶))) | ||
| Axiom | ax-his4 28553 | Identity law for inner product. Postulate (S4) of [Beran] p. 95. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → 0 < (𝐴 ·ih 𝐴)) | ||
| Theorem | his5 28554 | 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 28555 | Associative law for inner product. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐵 ·ih ((∗‘𝐴) ·ℎ 𝐶)) = (𝐴 · (𝐵 ·ih 𝐶))) | ||
| Theorem | his35 28556 | Move scalar multiplication to outside of inner product. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ)) → ((𝐴 ·ℎ 𝐶) ·ih (𝐵 ·ℎ 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 ·ih 𝐷))) | ||
| Theorem | his35i 28557 | 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 28558 | 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 28559 | 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 28560 | Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 −ℎ 𝐵) ·ih 𝐶) = ((𝐴 ·ih 𝐶) − (𝐵 ·ih 𝐶))) | ||
| Theorem | his2sub2 28561 | Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → (𝐴 ·ih (𝐵 −ℎ 𝐶)) = ((𝐴 ·ih 𝐵) − (𝐴 ·ih 𝐶))) | ||
| Theorem | hire 28562 | 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 28563 | Real closure of inner product with self. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐴 ·ih 𝐴) ∈ ℝ) | ||
| Theorem | hi01 28564 | Inner product with the 0 vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (0ℎ ·ih 𝐴) = 0) | ||
| Theorem | hi02 28565 | Inner product with the 0 vector. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐴 ·ih 0ℎ) = 0) | ||
| Theorem | hiidge0 28566 | Inner product with self is not negative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → 0 ≤ (𝐴 ·ih 𝐴)) | ||
| Theorem | his6 28567 | 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 28568 | 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 28569 | Commuted inner products have the same absolute values. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (abs‘(𝐴 ·ih 𝐵)) = (abs‘(𝐵 ·ih 𝐴))) | ||
| Theorem | hial0 28570* | 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 28571* | 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 28572 | Two vector subtractions simultaneously commute in an inner product. (Contributed by NM, 1-Jul-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) ·ih (𝐶 −ℎ 𝐷)) = ((𝐵 −ℎ 𝐴) ·ih (𝐷 −ℎ 𝐶)) | ||
| Theorem | hi2eq 28573 | Lemma used to prove equality of vectors. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih (𝐴 −ℎ 𝐵)) = (𝐵 ·ih (𝐴 −ℎ 𝐵)) ↔ 𝐴 = 𝐵)) | ||
| Theorem | hial2eq 28574* | Two vectors whose inner product is always equal are equal. (Contributed by NM, 16-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ (𝐴 ·ih 𝑥) = (𝐵 ·ih 𝑥) ↔ 𝐴 = 𝐵)) | ||
| Theorem | hial2eq2 28575* | Two vectors whose inner product is always equal are equal. (Contributed by NM, 28-Jan-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (∀𝑥 ∈ ℋ (𝑥 ·ih 𝐴) = (𝑥 ·ih 𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | orthcom 28576 | Orthogonality commutes. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 ·ih 𝐵) = 0 ↔ (𝐵 ·ih 𝐴) = 0)) | ||
| Theorem | normlem0 28577 | 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 28578 | 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 28579 | 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 28580 | 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 28581 | 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 28582 | 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 28583 | 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 28584 | 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 28585 | Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 +ℎ 𝐵) ·ih (𝐶 +ℎ 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) + ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶))) | ||
| Theorem | normlem9 28586 | Lemma used to derive properties of norm. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐶 ∈ ℋ & ⊢ 𝐷 ∈ ℋ ⇒ ⊢ ((𝐴 −ℎ 𝐵) ·ih (𝐶 −ℎ 𝐷)) = (((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐷)) − ((𝐴 ·ih 𝐷) + (𝐵 ·ih 𝐶))) | ||
| Theorem | normlem7tALT 28587 | 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 𝐴))))) | ||
| Theorem | bcseqi 28588 | Equality case of Bunjakovaskij-Cauchy-Schwarz inequality. Specifically, in the equality case the two vectors are collinear. Compare bcsiHIL 28648. (Contributed by NM, 16-Jul-2001.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (((𝐴 ·ih 𝐵) · (𝐵 ·ih 𝐴)) = ((𝐴 ·ih 𝐴) · (𝐵 ·ih 𝐵)) ↔ ((𝐵 ·ih 𝐵) ·ℎ 𝐴) = ((𝐴 ·ih 𝐵) ·ℎ 𝐵)) | ||
| Theorem | normlem9at 28589 | Lemma used to derive properties of norm. Part of Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 10-May-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 −ℎ 𝐵) ·ih (𝐴 −ℎ 𝐵)) = (((𝐴 ·ih 𝐴) + (𝐵 ·ih 𝐵)) − ((𝐴 ·ih 𝐵) + (𝐵 ·ih 𝐴)))) | ||
| Theorem | dfhnorm2 28590 | Alternate definition of the norm of a vector of Hilbert space. Definition of norm in [Beran] p. 96. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ normℎ = (𝑥 ∈ ℋ ↦ (√‘(𝑥 ·ih 𝑥))) | ||
| Theorem | normf 28591 | The norm function maps from Hilbert space to reals. (Contributed by NM, 6-Sep-2007.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ normℎ: ℋ⟶ℝ | ||
| Theorem | normval 28592 | The value of the norm of a vector in Hilbert space. Definition of norm in [Beran] p. 96. In the literature, the norm of 𝐴 is usually written as "|| 𝐴 ||", but we use function value notation to take advantage of our existing theorems about functions. (Contributed by NM, 29-May-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normℎ‘𝐴) = (√‘(𝐴 ·ih 𝐴))) | ||
| Theorem | normcl 28593 | Real closure of the norm of a vector. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (normℎ‘𝐴) ∈ ℝ) | ||
| Theorem | normge0 28594 | The norm of a vector is nonnegative. (Contributed by NM, 29-May-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → 0 ≤ (normℎ‘𝐴)) | ||
| Theorem | normgt0 28595 | The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐴 ≠ 0ℎ ↔ 0 < (normℎ‘𝐴))) | ||
| Theorem | norm0 28596 | The norm of a zero vector. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| ⊢ (normℎ‘0ℎ) = 0 | ||
| Theorem | norm-i 28597 | Theorem 3.3(i) of [Beran] p. 97. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴) = 0 ↔ 𝐴 = 0ℎ)) | ||
| Theorem | normne0 28598 | A norm is nonzero iff its argument is a nonzero vector. (Contributed by NM, 11-Mar-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ((normℎ‘𝐴) ≠ 0 ↔ 𝐴 ≠ 0ℎ)) | ||
| Theorem | normcli 28599 | Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (normℎ‘𝐴) ∈ ℝ | ||
| Theorem | normsqi 28600 | The square of a norm. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((normℎ‘𝐴)↑2) = (𝐴 ·ih 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |