P. 209 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	psgnevpmb 20801	A class is an even permutation if it is a permutation with sign 1. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → (𝐹 ∈ (pmEven‘𝐷) ↔ (𝐹 ∈ 𝑃 ∧ (𝑁‘𝐹) = 1)))
Theorem	psgnodpm 20802	A permutation which is odd (i.e. not even) has sign -1. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷))) → (𝑁‘𝐹) = -1)
Theorem	psgnevpm 20803	A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝐷)) → (𝑁‘𝐹) = 1)
Theorem	psgnodpmr 20804	If a permutation has sign -1 it is odd (not even). (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ (𝑁‘𝐹) = -1) → 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷)))
Theorem	zrhpsgnevpm 20805	The sign of an even permutation embedded into a ring is the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝑁)) → ((𝑌 ∘ 𝑆)‘𝐹) = 1 )
Theorem	zrhpsgnodpm 20806	The sign of an odd permutation embedded into a ring is the additive inverse of the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ (𝑃 ∖ (pmEven‘𝑁))) → ((𝑌 ∘ 𝑆)‘𝐹) = (𝐼‘ 1 ))
Theorem	cofipsgn 20807	Composition of any class 𝑌 and the sign function for a finite permutation. (Contributed by AV, 27-Dec-2018.) (Revised by AV, 3-Jul-2022.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘𝑄) = (𝑌‘(𝑆‘𝑄)))
Theorem	zrhpsgnelbas 20808	Embedding of permutation signs into a ring results in an element of the ring. (Contributed by AV, 1-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → (𝑌‘(𝑆‘𝑄)) ∈ (Base‘𝑅))
Theorem	zrhcopsgnelbas 20809	Embedding of permutation signs into a ring results in an element of the ring. (Contributed by AV, 1-Jan-2019.) (Proof shortened by AV, 3-Jul-2022.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘𝑄) ∈ (Base‘𝑅))
Theorem	evpmodpmf1o 20810*	The function for performing an even permutation after a fixed odd permutation is one to one onto all odd permutations. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷))) → (𝑓 ∈ (pmEven‘𝐷) ↦ (𝐹(+g‘𝑆)𝑓)):(pmEven‘𝐷)–1-1-onto→(𝑃 ∖ (pmEven‘𝐷)))
Theorem	pmtrodpm 20811	A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷)))
Theorem	psgnfix1 20812*	A permutation of a finite set fixing one element is generated by transpositions not involving the fixed element. (Contributed by AV, 13-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾}))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → ∃𝑤 ∈ Word 𝑇(𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑤)))
Theorem	psgnfix2 20813*	A permutation of a finite set fixing one element is generated by transpositions not involving the fixed element. (Contributed by AV, 17-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑍 = (SymGrp‘𝑁)    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → ∃𝑤 ∈ Word 𝑅𝑄 = (𝑍 Σg 𝑤)))
Theorem	psgndiflemB 20814*	Lemma 1 for psgndif 20816. (Contributed by AV, 27-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑍 = (SymGrp‘𝑁)    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊)) → ((𝑈 ∈ Word 𝑅 ∧ (♯‘𝑊) = (♯‘𝑈) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑄 = (𝑍 Σg 𝑈))))
Theorem	psgndiflemA 20815*	Lemma 2 for psgndif 20816. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑍 = (SymGrp‘𝑁)    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊) ∧ 𝑈 ∈ Word 𝑅) → (𝑄 = ((SymGrp‘𝑁) Σg 𝑈) → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑈)))))
Theorem	psgndif 20816*	Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾}))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → (𝑍‘(𝑄 ↾ (𝑁 ∖ {𝐾}))) = (𝑆‘𝑄)))
Theorem	copsgndif 20817*	Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019.) (Revised by AV, 5-Jul-2022.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 𝑍 = (pmSgn‘(𝑁 ∖ {𝐾}))    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) → (𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} → ((𝑌 ∘ 𝑍)‘(𝑄 ↾ (𝑁 ∖ {𝐾}))) = ((𝑌 ∘ 𝑆)‘𝑄)))
10.8.6  The ordered field of real numbers
Syntax	crefld 20818	Extend class notation with the field of real numbers.
class ℝfld
Definition	df-refld 20819	The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ ℝfld = (ℂfld ↾s ℝ)
Theorem	rebase 20820	The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ℝ = (Base‘ℝfld)
Theorem	remulg 20821	The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑁(.g‘ℝfld)𝐴) = (𝑁 · 𝐴))
Theorem	resubdrg 20822	The real numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) (Revised by Thierry Arnoux, 30-Jun-2019.)
⊢ (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
Theorem	resubgval 20823	Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ − = (-g‘ℝfld)    ⇒   ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	replusg 20824	The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ + = (+g‘ℝfld)
Theorem	remulr 20825	The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ · = (.r‘ℝfld)
Theorem	re0g 20826	The neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ 0 = (0g‘ℝfld)
Theorem	re1r 20827	The multiplicative neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ 1 = (1r‘ℝfld)
Theorem	rele2 20828	The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ≤ = (le‘ℝfld)
Theorem	relt 20829	The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ < = (lt‘ℝfld)
Theorem	reds 20830	The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.)
⊢ (abs ∘ − ) = (dist‘ℝfld)
Theorem	redvr 20831	The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴(/r‘ℝfld)𝐵) = (𝐴 / 𝐵))
Theorem	retos 20832	The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ℝfld ∈ Toset
Theorem	refld 20833	The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ℝfld ∈ Field
Theorem	refldcj 20834	The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ ∗ = (*𝑟‘ℝfld)
Theorem	recrng 20835	The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019.)
⊢ ℝfld ∈ *-Ring
Theorem	regsumsupp 20836*	The group sum over the real numbers, expressed as a finite sum. (Contributed by Thierry Arnoux, 22-Jun-2019.) (Proof shortened by AV, 19-Jul-2019.)
⊢ ((𝐹:𝐼⟶ℝ ∧ 𝐹 finSupp 0 ∧ 𝐼 ∈ 𝑉) → (ℝfld Σg 𝐹) = Σ𝑥 ∈ (𝐹 supp 0)(𝐹‘𝑥))
Theorem	rzgrp 20837	The quotient group ℝ / ℤ is a group. (Contributed by Thierry Arnoux, 26-Jan-2020.)
⊢ 𝑅 = (ℝfld /s (ℝfld ~QG ℤ))    ⇒   ⊢ 𝑅 ∈ Grp
10.9  Generalized pre-Hilbert and Hilbert spaces
10.9.1  Definition and basic properties
Syntax	cphl 20838	Extend class notation with class of all pre-Hilbert spaces.
class PreHil
Syntax	cipf 20839	Extend class notation with inner product function.
class ·if
Definition	df-phl 20840*	Define the class of all pre-Hilbert spaces (inner product spaces) over arbitrary fields with involution. (Some textbook definitions are more restrictive and require the field of scalars to be the field of real or complex numbers). (Contributed by NM, 22-Sep-2011.)
⊢ PreHil = {𝑔 ∈ LVec ∣ [(Base‘𝑔) / 𝑣][(·𝑖‘𝑔) / ℎ][(Scalar‘𝑔) / 𝑓](𝑓 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑣 ((𝑦 ∈ 𝑣 ↦ (𝑦ℎ𝑥)) ∈ (𝑔 LMHom (ringLMod‘𝑓)) ∧ ((𝑥ℎ𝑥) = (0g‘𝑓) → 𝑥 = (0g‘𝑔)) ∧ ∀𝑦 ∈ 𝑣 ((*𝑟‘𝑓)‘(𝑥ℎ𝑦)) = (𝑦ℎ𝑥)))}
Definition	df-ipf 20841*	Define the inner product function. Usually we will use ·𝑖 directly instead of ·if, and they have the same behavior in most cases. The main advantage of ·if is that it is a guaranteed function (ipffn 20865), while ·𝑖 only has closure (ipcl 20847). (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦)))
Theorem	isphl 20842*	The predicate "is a generalized pre-Hilbert (inner product) space". (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ ∗ = (*𝑟‘𝐹)    &   ⊢ 𝑍 = (0g‘𝐹)    ⇒   ⊢ (𝑊 ∈ PreHil ↔ (𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀𝑥 ∈ 𝑉 ((𝑦 ∈ 𝑉 ↦ (𝑦 , 𝑥)) ∈ (𝑊 LMHom (ringLMod‘𝐹)) ∧ ((𝑥 , 𝑥) = 𝑍 → 𝑥 = 0 ) ∧ ∀𝑦 ∈ 𝑉 ( ∗ ‘(𝑥 , 𝑦)) = (𝑦 , 𝑥))))
Theorem	phllvec 20843	A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec)
Theorem	phllmod 20844	A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod)
Theorem	phlsrng 20845	The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ PreHil → 𝐹 ∈ *-Ring)
Theorem	phllmhm 20846*	The inner product of a pre-Hilbert space is linear in its left argument. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (𝑥 , 𝐴))    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉) → 𝐺 ∈ (𝑊 LMHom (ringLMod‘𝐹)))
Theorem	ipcl 20847	Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ 𝐾)
Theorem	ipcj 20848	Conjugate of an inner product in a pre-Hilbert space. Equation I1 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ∗ = (*𝑟‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ( ∗ ‘(𝐴 , 𝐵)) = (𝐵 , 𝐴))
Theorem	iporthcom 20849	Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑍 = (0g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 , 𝐵) = 𝑍 ↔ (𝐵 , 𝐴) = 𝑍))
Theorem	ip0l 20850	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑍 = (0g‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉) → ( 0 , 𝐴) = 𝑍)
Theorem	ip0r 20851	Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑍 = (0g‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉) → (𝐴 , 0 ) = 𝑍)
Theorem	ipeq0 20852	The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. (Contributed by NM, 24-Jan-2008.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑍 = (0g‘𝐹)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉) → ((𝐴 , 𝐴) = 𝑍 ↔ 𝐴 = 0 ))
Theorem	ipdir 20853	Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ ⨣ = (+g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 + 𝐵) , 𝐶) = ((𝐴 , 𝐶) ⨣ (𝐵 , 𝐶)))
Theorem	ipdi 20854	Distributive law for inner product (left-distributivity). (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ ⨣ = (+g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 + 𝐶)) = ((𝐴 , 𝐵) ⨣ (𝐴 , 𝐶)))
Theorem	ip2di 20855	Distributive law for inner product. (Contributed by NM, 17-Apr-2008.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ ⨣ = (+g‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) , (𝐶 + 𝐷)) = (((𝐴 , 𝐶) ⨣ (𝐵 , 𝐷)) ⨣ ((𝐴 , 𝐷) ⨣ (𝐵 , 𝐶))))
Theorem	ipsubdir 20856	Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑆 = (-g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) , 𝐶) = ((𝐴 , 𝐶)𝑆(𝐵 , 𝐶)))
Theorem	ipsubdi 20857	Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑆 = (-g‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 − 𝐶)) = ((𝐴 , 𝐵)𝑆(𝐴 , 𝐶)))
Theorem	ip2subdi 20858	Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑆 = (-g‘𝐹)    &   ⊢ + = (+g‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))))
Theorem	ipass 20859	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 · 𝐵) , 𝐶) = (𝐴 × (𝐵 , 𝐶)))
Theorem	ipassr 20860	"Associative" law for second argument of inner product (compare ipass 20859). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝐹)    &   ⊢ ∗ = (*𝑟‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → (𝐴 , (𝐶 · 𝐵)) = ((𝐴 , 𝐵) × ( ∗ ‘𝐶)))
Theorem	ipassr2 20861	"Associative" law for inner product. Conjugate version of ipassr 20860. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝐹)    &   ⊢ ∗ = (*𝑟‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝐴 , 𝐵) × 𝐶) = (𝐴 , (( ∗ ‘𝐶) · 𝐵)))
Theorem	ipffval 20862*	The inner product operation as a function. (Contributed by Mario Carneiro, 12-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ · = (·if‘𝑊)    ⇒   ⊢ · = (𝑥 ∈ 𝑉, 𝑦 ∈ 𝑉 ↦ (𝑥 , 𝑦))
Theorem	ipfval 20863	The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ · = (·if‘𝑊)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) = (𝑋 , 𝑌))
Theorem	ipfeq 20864	If the inner product operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ · = (·if‘𝑊)    ⇒   ⊢ ( , Fn (𝑉 × 𝑉) → · = , )
Theorem	ipffn 20865	The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·if‘𝑊)    ⇒   ⊢ , Fn (𝑉 × 𝑉)
Theorem	phlipf 20866	The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·if‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑊 ∈ PreHil → , :(𝑉 × 𝑉)⟶𝐾)
Theorem	ip2eq 20867*	Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ 𝑉 (𝑥 , 𝐴) = (𝑥 , 𝐵)))
Theorem	isphld 20868*	Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ (𝜑 → 𝑉 = (Base‘𝑊))    &   ⊢ (𝜑 → + = (+g‘𝑊))    &   ⊢ (𝜑 → · = ( ·𝑠 ‘𝑊))    &   ⊢ (𝜑 → 𝐼 = (·𝑖‘𝑊))    &   ⊢ (𝜑 → 0 = (0g‘𝑊))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝑊))    &   ⊢ (𝜑 → 𝐾 = (Base‘𝐹))    &   ⊢ (𝜑 → ⨣ = (+g‘𝐹))    &   ⊢ (𝜑 → × = (.r‘𝐹))    &   ⊢ (𝜑 → ∗ = (*𝑟‘𝐹))    &   ⊢ (𝜑 → 𝑂 = (0g‘𝐹))    &   ⊢ (𝜑 → 𝑊 ∈ LVec)    &   ⊢ (𝜑 → 𝐹 ∈ *-Ring)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥𝐼𝑦) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐾 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝑞 · 𝑥) + 𝑦)𝐼𝑧) = ((𝑞 × (𝑥𝐼𝑧)) ⨣ (𝑦𝐼𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑥𝐼𝑥) = 𝑂) → 𝑥 = 0 )    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ( ∗ ‘(𝑥𝐼𝑦)) = (𝑦𝐼𝑥))    ⇒   ⊢ (𝜑 → 𝑊 ∈ PreHil)
Theorem	phlpropd 20869*	If two structures have the same components (properties), one is a pre-Hilbert space iff the other one is. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐾))    &   ⊢ (𝜑 → 𝐹 = (Scalar‘𝐿))    &   ⊢ 𝑃 = (Base‘𝐹)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑃 ∧ 𝑦 ∈ 𝐵)) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(·𝑖‘𝐾)𝑦) = (𝑥(·𝑖‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ PreHil ↔ 𝐿 ∈ PreHil))
Theorem	ssipeq 20870	The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑃 = (·𝑖‘𝑋)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝑃 = , )
Theorem	phssipval 20871	The inner product on a subspace in terms of the inner product on the parent space. (Contributed by NM, 28-Jan-2008.) (Revised by AV, 19-Oct-2021.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑃 = (·𝑖‘𝑋)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈)) → (𝐴𝑃𝐵) = (𝐴 , 𝐵))
Theorem	phssip 20872	The inner product (as a function) on a subspace is a restriction of the inner product (as a function) on the parent space. (Contributed by NM, 28-Jan-2008.) (Revised by AV, 19-Oct-2021.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ · = (·if‘𝑊)    &   ⊢ 𝑃 = (·if‘𝑋)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆) → 𝑃 = ( · ↾ (𝑈 × 𝑈)))
Theorem	phlssphl 20873	A subspace of an inner product space (pre-Hilbert space) is an inner product space. (Contributed by AV, 25-Sep-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ PreHil)
10.9.2  Orthocomplements and closed subspaces
Syntax	cocv 20874	Extend class notation with orthocomplement of a subset.
class ocv
Syntax	ccss 20875	Extend class notation with set of closed subspaces.
class ClSubSp
Syntax	cthl 20876	Extend class notation with the Hilbert lattice.
class toHL
Definition	df-ocv 20877*	Define the orthocomplement function in a given set (which usually is a pre-Hilbert space): it associates with a subset its orthogonal subset (which in the case of a closed linear subspace is its orthocomplement). (Contributed by NM, 7-Oct-2011.)
⊢ ocv = (ℎ ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘ℎ) ↦ {𝑥 ∈ (Base‘ℎ) ∣ ∀𝑦 ∈ 𝑠 (𝑥(·𝑖‘ℎ)𝑦) = (0g‘(Scalar‘ℎ))}))
Definition	df-css 20878*	Define the set of closed (linear) subspaces of a given pre-Hilbert space. (Contributed by NM, 7-Oct-2011.)
⊢ ClSubSp = (ℎ ∈ V ↦ {𝑠 ∣ 𝑠 = ((ocv‘ℎ)‘((ocv‘ℎ)‘𝑠))})
Definition	df-thl 20879	Define the Hilbert lattice of closed subspaces of a given pre-Hilbert space. (Contributed by Mario Carneiro, 25-Oct-2015.)
⊢ toHL = (ℎ ∈ V ↦ ((toInc‘(ClSubSp‘ℎ)) sSet ⟨(oc‘ndx), (ocv‘ℎ)⟩))
Theorem	ocvfval 20880*	The orthocomplement operation. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → ⊥ = (𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 }))
Theorem	ocvval 20881*	Value of the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ (𝑆 ⊆ 𝑉 → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 })
Theorem	elocv 20882*	Elementhood in the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ (𝐴 ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (𝐴 , 𝑥) = 0 ))
Theorem	ocvi 20883	Property of a member of the orthocomplement of a subset. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 0 = (0g‘𝐹)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ ((𝐴 ∈ ( ⊥ ‘𝑆) ∧ 𝐵 ∈ 𝑆) → (𝐴 , 𝐵) = 0 )
Theorem	ocvss 20884	The orthocomplement of a subset is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ ( ⊥ ‘𝑆) ⊆ 𝑉
Theorem	ocvocv 20885	A set is contained in its double orthocomplement. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → 𝑆 ⊆ ( ⊥ ‘( ⊥ ‘𝑆)))
Theorem	ocvlss 20886	The orthocomplement of a subset is a linear subspace of the pre-Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘𝑆) ∈ 𝐿)
Theorem	ocv2ss 20887	Orthocomplements reverse subset inclusion. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ (𝑇 ⊆ 𝑆 → ( ⊥ ‘𝑆) ⊆ ( ⊥ ‘𝑇))
Theorem	ocvin 20888	An orthocomplement has trivial intersection with the original subspace. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ∈ 𝐿) → (𝑆 ∩ ( ⊥ ‘𝑆)) = { 0 })
Theorem	ocvsscon 20889	Two ways to say that 𝑆 and 𝑇 are orthogonal subspaces. (Contributed by Mario Carneiro, 23-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑉) → (𝑆 ⊆ ( ⊥ ‘𝑇) ↔ 𝑇 ⊆ ( ⊥ ‘𝑆)))
Theorem	ocvlsp 20890	The orthocomplement of a linear span. (Contributed by Mario Carneiro, 23-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 𝑁 = (LSpan‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → ( ⊥ ‘(𝑁‘𝑆)) = ( ⊥ ‘𝑆))
Theorem	ocv0 20891	The orthocomplement of the empty set. (Contributed by Mario Carneiro, 23-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ ( ⊥ ‘∅) = 𝑉
Theorem	ocvz 20892	The orthocomplement of the zero subspace. (Contributed by Mario Carneiro, 23-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ (𝑊 ∈ PreHil → ( ⊥ ‘{ 0 }) = 𝑉)
Theorem	ocv1 20893	The orthocomplement of the base set. (Contributed by Mario Carneiro, 23-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ (𝑊 ∈ PreHil → ( ⊥ ‘𝑉) = { 0 })
Theorem	unocv 20894	The orthocomplement of a union. (Contributed by Mario Carneiro, 23-Oct-2015.)
⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ ( ⊥ ‘(𝐴 ∪ 𝐵)) = (( ⊥ ‘𝐴) ∩ ( ⊥ ‘𝐵))
Theorem	iunocv 20895*	The orthocomplement of an indexed union. (Contributed by Mario Carneiro, 23-Oct-2015.)
⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ ( ⊥ ‘∪ 𝑥 ∈ 𝐴 𝐵) = (𝑉 ∩ ∩ 𝑥 ∈ 𝐴 ( ⊥ ‘𝐵))
Theorem	cssval 20896*	The set of closed subspaces of a pre-Hilbert space. (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.)
⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → 𝐶 = {𝑠 ∣ 𝑠 = ( ⊥ ‘( ⊥ ‘𝑠))})
Theorem	iscss 20897	The predicate "is a closed subspace" (of a pre-Hilbert space). (Contributed by NM, 7-Oct-2011.) (Revised by Mario Carneiro, 13-Oct-2015.)
⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑋 → (𝑆 ∈ 𝐶 ↔ 𝑆 = ( ⊥ ‘( ⊥ ‘𝑆))))
Theorem	cssi 20898	Property of a closed subspace (of a pre-Hilbert space). (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ⊥ = (ocv‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑆 ∈ 𝐶 → 𝑆 = ( ⊥ ‘( ⊥ ‘𝑆)))
Theorem	cssss 20899	A closed subspace is a subset of the base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑆 ∈ 𝐶 → 𝑆 ⊆ 𝑉)
Theorem	iscss2 20900	It is sufficient to prove that the double orthocomplement is a subset of the target set to show that the set is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    &   ⊢ ⊥ = (ocv‘𝑊)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉) → (𝑆 ∈ 𝐶 ↔ ( ⊥ ‘( ⊥ ‘𝑆)) ⊆ 𝑆))