P. 212 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21101-21200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	znle2 21101	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → ≤ = ((𝐹 ∘ ≤ ) ∘ ◡𝐹))
Theorem	znleval 21102	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵))))
Theorem	znleval2 21103	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≤ 𝐵 ↔ (◡𝐹‘𝐴) ≤ (◡𝐹‘𝐵)))
Theorem	zntoslem 21104	Lemma for zntos 21105. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)    &   ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))    &   ⊢ ≤ = (le‘𝑌)    &   ⊢ 𝑋 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset)
Theorem	zntos 21105	The ℤ/nℤ structure is a totally ordered set. (The order is not respected by the operations, except in the case 𝑁 = 0 when it coincides with the ordering on ℤ.) (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ Toset)
Theorem	znhash 21106	The ℤ/nℤ structure has 𝑛 elements. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → (♯‘𝐵) = 𝑁)
Theorem	znfi 21107	The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐵 ∈ Fin)
Theorem	znfld 21108	The ℤ/nℤ structure is a finite field when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℙ → 𝑌 ∈ Field)
Theorem	znidomb 21109	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 21110	Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (chr‘𝑌) = 𝑁)
Theorem	znunit 21111	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 21112	The size of the unit group of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.)
⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝑈 = (Unit‘𝑌)    ⇒   ⊢ (𝑁 ∈ ℕ → (♯‘𝑈) = (ϕ‘𝑁))
Theorem	znrrg 21113	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 21114*	Lemma for cygzn 21118. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    ⇒   ⊢ ((𝜑 ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝐿‘𝐾) = (𝐿‘𝑀) ↔ (𝐾 · 𝑋) = (𝑀 · 𝑋)))
Theorem	cygznlem2a 21115*	Lemma for cygzn 21118. (Contributed by Mario Carneiro, 23-Dec-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = if(𝐵 ∈ Fin, (♯‘𝐵), 0)    &   ⊢ 𝑌 = (ℤ/nℤ‘𝑁)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐿 = (ℤRHom‘𝑌)    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵}    &   ⊢ (𝜑 → 𝐺 ∈ CycGrp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐸)    &   ⊢ 𝐹 = ran (𝑚 ∈ ℤ ↦ ⟨(𝐿‘𝑚), (𝑚 · 𝑋)⟩)    ⇒   ⊢ (𝜑 → 𝐹:(Base‘𝑌)⟶𝐵)
Theorem	cygznlem2 21116*	Lemma for cygzn 21118. (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 21117*	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 21118	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 21119*	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 21120	Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐶 = (Base‘𝐻)    ⇒   ⊢ ((𝐺 ∈ CycGrp ∧ 𝐻 ∈ CycGrp) → (𝐺 ≃𝑔 𝐻 ↔ 𝐵 ≈ 𝐶))
Theorem	frgpcyg 21121	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)
10.8.4  Signs as subgroup of the complex numbers
Theorem	cnmsgnsubg 21122	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 21123	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 21124	The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1})    ⇒   ⊢ 𝑈 ∈ Grp
Theorem	psgnghm 21125	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 21126	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 21127	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 21128	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 21129	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 21130	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 21131	Even permutations are permutations. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    ⇒   ⊢ (pmEven‘𝐷) ⊆ 𝑃
Theorem	psgnevpmb 21132	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 21133	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 21134	A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ (pmEven‘𝐷)) → (𝑁‘𝐹) = 1)
Theorem	psgnodpmr 21135	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 21136	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 21137	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 21138	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 21139	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 21140	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 21141*	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 21142	A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑃 = (Base‘𝑆)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑇) → 𝐹 ∈ (𝑃 ∖ (pmEven‘𝐷)))
Theorem	psgnfix1 21143*	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 21144*	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 21145*	Lemma 1 for psgndif 21147. (Contributed by AV, 27-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑍 = (SymGrp‘𝑁)    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊)) → ((𝑈 ∈ Word 𝑅 ∧ (♯‘𝑊) = (♯‘𝑈) ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(((𝑈‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))) → 𝑄 = (𝑍 Σg 𝑈))))
Theorem	psgndiflemA 21146*	Lemma 2 for psgndif 21147. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑆 = (SymGrp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑍 = (SymGrp‘𝑁)    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ 𝑄 ∈ {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}) → ((𝑊 ∈ Word 𝑇 ∧ (𝑄 ↾ (𝑁 ∖ {𝐾})) = (𝑆 Σg 𝑊) ∧ 𝑈 ∈ Word 𝑅) → (𝑄 = ((SymGrp‘𝑁) Σg 𝑈) → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑈)))))
Theorem	psgndif 21147*	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 21148*	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 21149	Extend class notation with the field of real numbers.
class ℝfld
Definition	df-refld 21150	The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ ℝfld = (ℂfld ↾s ℝ)
Theorem	rebase 21151	The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ℝ = (Base‘ℝfld)
Theorem	remulg 21152	The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ ℝ) → (𝑁(.g‘ℝfld)𝐴) = (𝑁 · 𝐴))
Theorem	resubdrg 21153	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 21154	Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ − = (-g‘ℝfld)    ⇒   ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋 − 𝑌) = (𝑋 − 𝑌))
Theorem	replusg 21155	The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ + = (+g‘ℝfld)
Theorem	remulr 21156	The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ · = (.r‘ℝfld)
Theorem	re0g 21157	The zero element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ 0 = (0g‘ℝfld)
Theorem	re1r 21158	The unity element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ 1 = (1r‘ℝfld)
Theorem	rele2 21159	The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ≤ = (le‘ℝfld)
Theorem	relt 21160	The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ < = (lt‘ℝfld)
Theorem	reds 21161	The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.)
⊢ (abs ∘ − ) = (dist‘ℝfld)
Theorem	redvr 21162	The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴(/r‘ℝfld)𝐵) = (𝐴 / 𝐵))
Theorem	retos 21163	The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.)
⊢ ℝfld ∈ Toset
Theorem	refld 21164	The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ℝfld ∈ Field
Theorem	refldcj 21165	The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ ∗ = (*𝑟‘ℝfld)
Theorem	resrng 21166	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 21167*	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 21168	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 21169	Extend class notation with class of all pre-Hilbert spaces.
class PreHil
Syntax	cipf 21170	Extend class notation with inner product function.
class ·if
Definition	df-phl 21171*	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 21172*	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 21196), while ·𝑖 only has closure (ipcl 21178). (Contributed by Mario Carneiro, 12-Aug-2015.)
⊢ ·if = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(·𝑖‘𝑔)𝑦)))
Theorem	isphl 21173*	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 21174	A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LVec)
Theorem	phllmod 21175	A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod)
Theorem	phlsrng 21176	The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ PreHil → 𝐹 ∈ *-Ring)
Theorem	phllmhm 21177*	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 21178	Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴 , 𝐵) ∈ 𝐾)
Theorem	ipcj 21179	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 21180	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 21181	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 21182	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 21183	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 21184	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 21185	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 21186	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 21187	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 21188	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 21189	Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑆 = (-g‘𝐹)    &   ⊢ + = (+g‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))))
Theorem	ipass 21190	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 21191	"Associative" law for second argument of inner product (compare ipass 21190). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝐹)    &   ⊢ ∗ = (*𝑟‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → (𝐴 , (𝐶 · 𝐵)) = ((𝐴 , 𝐵) × ( ∗ ‘𝐶)))
Theorem	ipassr2 21192	"Associative" law for inner product. Conjugate version of ipassr 21191. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ × = (.r‘𝐹)    &   ⊢ ∗ = (*𝑟‘𝐹)    ⇒   ⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝐾)) → ((𝐴 , 𝐵) × 𝐶) = (𝐴 , (( ∗ ‘𝐶) · 𝐵)))
Theorem	ipffval 21193*	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 21194	The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ · = (·if‘𝑊)    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 · 𝑌) = (𝑋 , 𝑌))
Theorem	ipfeq 21195	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 21196	The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·if‘𝑊)    ⇒   ⊢ , Fn (𝑉 × 𝑉)
Theorem	phlipf 21197	The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·if‘𝑊)    &   ⊢ 𝑆 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝑆)    ⇒   ⊢ (𝑊 ∈ PreHil → , :(𝑉 × 𝑉)⟶𝐾)
Theorem	ip2eq 21198*	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 21199*	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 21200*	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))