P. 217 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21601-21700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	znfi 21601	The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
Theorem	znfld 21602	The ℤ/nℤ structure is a finite field when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Field)
Theorem	znidomb 21603	The ℤ/nℤ structure is a domain (and hence a field) precisely when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑌 ∈ IDomn ↔ 𝑁 ∈ ℙ))
Theorem	znchr 21604	Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (chr‘𝑌) = 𝑁)
Theorem	znunit 21605	The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑌)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℤ) → ((𝐿‘𝐴) ∈ 𝑈 ↔ (𝐴 gcd 𝑁) = 1))
Theorem	znunithash 21606	The size of the unit group of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → (♯‘𝑈) = (ϕ‘𝑁))
Theorem	znrrg 21607	The regular elements of ℤ/nℤ are exactly the units. (This theorem fails for 𝑁 = 0, where all nonzero integers are regular, but only ±1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑌)    &   ⊢ 𝐸 = (RLReg‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐸 = 𝑈)
Theorem	cygznlem1 21608*	Lemma for cygzn 21612. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    ⇒   ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋)))
Theorem	cygznlem2a 21609*	Lemma for cygzn 21612. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ ⟨(𝐿‘𝑚), (𝑚 · 𝑋)⟩)    ⇒   ⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵)
Theorem	cygznlem2 21610*	Lemma for cygzn 21612. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ ⟨(𝐿‘𝑚), (𝑚 · 𝑋)⟩)    ⇒   ⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝐹‘(𝐿‘𝑀)) = (𝑀 · 𝑋))
Theorem	cygznlem3 21611*	A cyclic group with 𝑛 elements is isomorphic to ℤ / 𝑛ℤ. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ ⟨(𝐿‘𝑚), (𝑚 · 𝑋)⟩)    ⇒   ⊢ (𝜑 → 𝐺 ≃𝑔 𝑌)
Theorem	cygzn 21612	A cyclic group with 𝑛 elements is isomorphic to ℤ / 𝑛ℤ, and an infinite cyclic group is isomorphic to ℤ / 0ℤ ≈ ℤ. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝐺 ∈ CycGrp → 𝐺 ≃𝑔 𝑌)
Theorem	cygth 21613*	The "fundamental theorem of cyclic groups". Cyclic groups are exactly the additive groups ℤ / 𝑛ℤ, for 0 ≤ 𝑛 (where 𝑛 = 0 is the infinite cyclic group ℤ), up to isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ (𝐺 ∈ CycGrp ↔ ∃𝑛 ∈ ℕ0 𝐺 ≃𝑔 (ℤ/nℤ‘𝑛))
Theorem	cyggic 21614	Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = (Base‘𝐻)    ⇒   ⊢ ((𝐺 ∈ CycGrp ∧ 𝐻 ∈ CycGrp) → (𝐺 ≃𝑔 𝐻 ↔ 𝐵 ≈ 𝐶))
Theorem	frgpcyg 21615	A free group is cyclic iff it has zero or one generator. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 18-Apr-2021.)
⊢ 𝐺 = (freeGrp‘𝐼)    ⇒   ⊢ (𝐼 ≼ 1o ↔ 𝐺 ∈ CycGrp)
Theorem	freshmansdream 21616	For a prime number 𝑃, if 𝑋 and 𝑌 are members of a commutative ring 𝑅 of characteristic 𝑃, then ((𝑋 + 𝑌)↑𝑃) = ((𝑋↑𝑃) + (𝑌↑𝑃)). This theorem is sometimes referred to as "the freshman's dream" . (Contributed by Thierry Arnoux, 18-Sep-2023.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝑃 = (chr‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑃 ↑ (𝑋 + 𝑌)) = ((𝑃 ↑ 𝑋) + (𝑃 ↑ 𝑌)))
Theorem	frobrhm 21617*	In a commutative ring with prime characteristic, the Frobenius function 𝐹 is a ring endomorphism, thus named the Frobenius endomorphism. (Contributed by Thierry Arnoux, 31-May-2024.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝑃 = (chr‘𝑅)    &   ⊢ ↑ = (.g‘(mulGrp‘𝑅))    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑃 ↑ 𝑥))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑅))
10.8.4  Signs as subgroup of the complex numbers
Theorem	cnmsgnsubg 21618	The signs form a multiplicative subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑀 = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))    ⇒   ⊢ {1, -1} ∈ (SubGrp‘𝑀)
Theorem	cnmsgnbas 21619	The base set of the sign subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1})    ⇒   ⊢ {1, -1} = (Base‘𝑈)
Theorem	cnmsgngrp 21620	The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1})    ⇒   ⊢ 𝑈 ∈ Grp
Theorem	psgnghm 21621	The sign is a homomorphism from the finitary permutation group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝐹 = (𝑆 ↾s dom 𝑁)    &   ⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1})    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝑁 ∈ (𝐹 GrpHom 𝑈))
Theorem	psgnghm2 21622	The sign is a homomorphism from the finite symmetric group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1})    ⇒   ⊢ (𝐷 ∈ Fin → 𝑁 ∈ (𝑆 GrpHom 𝑈))
Theorem	psgninv 21623	The sign of a permutation equals the sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘◡𝐹) = (𝑁‘𝐹))
Theorem	psgnco 21624	Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃) → (𝑁‘(𝐹 ∘ 𝐺)) = ((𝑁‘𝐹) · (𝑁‘𝐺)))
10.8.5  Embedding of permutation signs into a ring
Theorem	zrhpsgnmhm 21625	Embedding of permutation signs into an arbitrary ring is a homomorphism. (Contributed by SO, 9-Jul-2018.)
⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ Fin) → ((ℤRHom‘𝑅) ∘ (pmSgn‘𝐴)) ∈ ((SymGrp‘𝐴) MndHom (mulGrp‘𝑅)))
Theorem	zrhpsgninv 21626	The embedded sign of a permutation equals the embedded sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ 𝑃) → ((𝑌 ∘ 𝑆)‘◡𝐹) = ((𝑌 ∘ 𝑆)‘𝐹))
Theorem	evpmss 21627	Even permutations are permutations. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    ⇒   ⊢ (pmEven‘𝐷) ⊆ 𝑃
Theorem	psgnevpmb 21628	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 21629	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 21630	A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝐷)) → (𝑁‘𝐹) = 1)
Theorem	psgnodpmr 21631	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 21632	The sign of an even permutation embedded into a ring is the unity element of the ring. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝑁)) → ((𝑌 ∘ 𝑆)‘𝐹) = 1 )
Theorem	zrhpsgnodpm 21633	The sign of an odd permutation embedded into a ring is the additive inverse of the unity element of the ring. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑌 = (ℤRHom‘𝑅)    &   ⊢ 𝑆 = (pmSgn‘𝑁)    &   ⊢ 1 = (1r‘𝑅)    &   ⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝐹 ∈ (𝑃 ∖ (pmEven‘𝑁))) → ((𝑌 ∘ 𝑆)‘𝐹) = (𝐼‘ 1 ))
Theorem	cofipsgn 21634	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 21635	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 21636	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 21637*	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 21638	A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷)))
Theorem	psgnfix1 21639*	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 21640*	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 21641*	Lemma 1 for psgndif 21643. (Contributed by AV, 27-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑍 = (SymGrp‘𝑁)    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊)) → ((𝑈 ∈ Word 𝑅 ∧ (♯‘𝑊) = (♯‘𝑈) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑄 = (𝑍 Σg 𝑈))))
Theorem	psgndiflemA 21642*	Lemma 2 for psgndif 21643. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑍 = (SymGrp‘𝑁)    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊) ∧ 𝑈 ∈ Word 𝑅) → (𝑄 = ((SymGrp‘𝑁) Σg 𝑈) → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑈)))))
Theorem	psgndif 21643*	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 21644*	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 21645	Extend class notation with the field of real numbers.
class ℝfld
Definition	df-refld 21646	The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ ℝfld = (ℂfld ↾s ℝ)
Theorem	rebase 21647	The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ℝ = (Base‘ℝfld)
Theorem	remulg 21648	The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑁(.g‘ℝfld)𝐴) = (𝑁 · 𝐴))
Theorem	resubdrg 21649	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 21650	Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ − = (-g‘ℝfld)    ⇒   ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	replusg 21651	The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ + = (+g‘ℝfld)
Theorem	remulr 21652	The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ · = (.r‘ℝfld)
Theorem	re0g 21653	The zero element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ 0 = (0g‘ℝfld)
Theorem	re1r 21654	The unity element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ 1 = (1r‘ℝfld)
Theorem	rele2 21655	The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ≤ = (le‘ℝfld)
Theorem	relt 21656	The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ < = (lt‘ℝfld)
Theorem	reds 21657	The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.)
⊢ (abs ∘ − ) = (dist‘ℝfld)
Theorem	redvr 21658	The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴(/r‘ℝfld)𝐵) = (𝐴 / 𝐵))
Theorem	retos 21659	The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ℝfld ∈ Toset
Theorem	refld 21660	The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ℝfld ∈ Field
Theorem	refldcj 21661	The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ ∗ = (*𝑟‘ℝfld)
Theorem	resrng 21662	The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019.) (Proof shortened by Thierry Arnoux, 11-Jan-2025.)
⊢ ℝfld ∈ *-Ring
Theorem	regsumsupp 21663*	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 21664	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 21665	Extend class notation with class of all pre-Hilbert spaces.
class PreHil
Syntax	cipf 21666	Extend class notation with inner product function.
class ·if
Definition	df-phl 21667*	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 21668*	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 21692), while ·𝑖 only has closure (ipcl 21674). (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦)))
Theorem	isphl 21669*	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 21670	A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec)
Theorem	phllmod 21671	A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod)
Theorem	phlsrng 21672	The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ PreHil → 𝐹 ∈ *-Ring)
Theorem	phllmhm 21673*	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 21674	Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ 𝐾)
Theorem	ipcj 21675	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 21676	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 21677	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 21678	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 21679	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 21680	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 21681	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 21682	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 21683	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 21684	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 21685	Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑆 = (-g‘𝐹)    &   ⊢ + = (+g‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))))
Theorem	ipass 21686	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 21687	"Associative" law for second argument of inner product (compare ipass 21686). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝐹)    &   ⊢ ∗ = (*𝑟‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → (𝐴 , (𝐶 · 𝐵)) = ((𝐴 , 𝐵) × ( ∗ ‘𝐶)))
Theorem	ipassr2 21688	"Associative" law for inner product. Conjugate version of ipassr 21687. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝐹)    &   ⊢ ∗ = (*𝑟‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝐴 , 𝐵) × 𝐶) = (𝐴 , (( ∗ ‘𝐶) · 𝐵)))
Theorem	ipffval 21689*	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 21690	The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ · = (·if‘𝑊)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) = (𝑋 , 𝑌))
Theorem	ipfeq 21691	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 21692	The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·if‘𝑊)    ⇒   ⊢ , Fn (𝑉 × 𝑉)
Theorem	phlipf 21693	The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·if‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑊 ∈ PreHil → , :(𝑉 × 𝑉)⟶𝐾)
Theorem	ip2eq 21694*	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 21695*	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 21696*	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 21697	The inner product on a subspace equals the inner product on the parent space. (Contributed by AV, 19-Oct-2021.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑃 = (·𝑖‘𝑋)    ⇒   ⊢ (𝑈 ∈ 𝑆 → 𝑃 = , )
Theorem	phssipval 21698	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 21699	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 21700	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)