nyuuzyou/wikis huggingface dataset:
Self-Distributive Law for Conditional/Forward Implication/Formulation 2/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
As can be seen by inspection, the truth value under the main connective is true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccccc|}
\hline
(p & \implies & (q & \implies & r)) & \implies & ((p & \implies & q) & \implies & (p & \implies & r)) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \T & \T & \F & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \F & \T & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \T & \F & \T & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
== Sources ==
* : $\S 1$: Informal statement calculus: $\S 1.2$: Truth functions and truth tables: Exercises $3 \ \text{(h)}$
Category:Self-Distributive Law for Conditional
Self-Distributive Law for Conditional/Reverse Implication/Formulation 2

== Theorem ==
:$\vdash \paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }$
== Proof ==
== Sources ==
* : $\text{I}$: 'NOT' and 'IF': $\S 5$: Theorem $\text{T7}$
Category:Self-Distributive Law for Conditional
Self-Distributive Quasigroup is Idempotent

== Theorem ==
Let $\struct {S, \odot}$ be a self-distributive quasigroup.
Then $\odot$ is an idempotent operation.
== Proof ==
Because $S$ is a quasigroup:
:$\forall a, b \in S: \exists ! x \in S: x \odot a = b$
:$\forall a, b \in S: \exists ! y \in S: a \odot y = b$
In particular:
:$\exists ! x \in S: x \circ \paren {a \odot b} = y$
for arbitrary $a, b \in S$.
Let $y = a \odot \paren {a \odot b}$.
Because $\struct {S, \odot}$ is self-distributive:
:$y = \paren {a \odot a} \odot \paren {a \odot b}$
Because $S$ is a quasigroup, we have that:
:$a = a \odot a$
As $a$ is arbitrary, the result follows.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 16$: The Natural Numbers: Exercise $16.21 \ \text{(c)}$
Category:Self-Distributive Operations
Category:Quasigroups
Category:Idempotence
Self-Distributive Quasigroup with at least Two Elements has no Identity

== Theorem ==
Let $\struct {S, \odot}$ be a self-distributive quasigroup.
Let $S$ have at least $2$ elements.
Then $\struct {S, \odot}$ has no identity element.
== Proof ==
 $S$ has an identity element $e$ and another element $a$ such that $a \ne e$.
Recall the definition of quasigroup:
:$\forall a, b \in S: \exists ! x \in S: x \circ a = b$
That is:
We have:
That is, there are two $x \in S$ such that $x \circ a = a$.
This contradicts our assertion that $\struct {S, \odot}$ is a quasigroup.
Hence there can be no such element.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 16$: The Natural Numbers: Exercise $16.21 \ \text{(d)}$
Category:Self-Distributive Operations
Category:Quasigroups
Category:Identity Elements
Self-Distributive Quasigroup with at least Two Elements is not Associative

== Theorem ==
Let $\struct {S, \odot}$ be a self-distributive quasigroup.
Let $S$ have at least $2$ elements.
Then $\odot$ is not an associative operation.
== Proof ==
 $\odot$ is associative operation.
Let $a, b \in S$ such that $a \ne b$.
Then:
which contradicts our supposition that $a \ne b$.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 16$: The Natural Numbers: Exercise $16.21 \ \text{(d)}$
Category:Self-Distributive Operations
Category:Quasigroups
Category:Associativity
Self-Distributive Structure/Examples/Arithmetic Mean

== Example of Self-Distributive Structure ==
Let $\Q$ denote the set of rational numbers.
Let $\circ$ be the operation defined on $\Q$ as:
:$\forall x, y \in \Q: x \circ y := \dfrac {x + y} 2$
That is, $x \circ y$ is the arithmetic mean of $x$ and $y$ in $\Q$.
Then the algebraic structure $\struct {\Q, \circ}$ so formed is a self-distributive quasigroup.
== Proof ==
As Rational Addition is Commutative, it follows immediately from Left Distributive and Commutative implies Distributive that:
:$\forall a, b, c \in \Q: \paren {a \circ b} \circ c = \paren {a \circ c} \circ \paren {b \circ c}$
To demonstrate that $\struct {\Q, \circ}$ is a quasigroup, it remains to be shown that:
:$\forall a, b \in \Q: \exists ! x \in \Q: x \circ a = b$
:$\forall a, b \in \Q: \exists ! y \in \Q: a \circ y = b$
We have:
and similarly:
Hence both $x$ and $y$ are determined uniquely by $a$ and $b$.
Hence by definition $\struct {\Q, \circ}$ is a quasigroup.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 16$: The Natural Numbers: Exercise $16.21 \ \text{(a)}$
Category:Examples of Self-Distributive Structures
Category:Examples of Quasigroups
Self-Inverse Element of Integral Domain is Unity or its Negative

== Theorem ==
Let $\struct {D, +, \circ}$ be an integral domain whose zero is $0_D$ and whose unity is $1_D$.
Let $x \in D$ such that $x^2 = 1_D$.
Then either $x = 1_D$ or $x = -1_D$.
== Proof ==
== Sources ==
* : Chapter $9$: Rings: Exercise $12$
Category:Integral Domains
Self-Inverse Elements Commute iff Product is Self-Inverse

== Theorem ==
Let $\struct {G, \circ}$ be a group.
Let $x, y \in \struct {G, \circ}$, such that $x$ and $y$ are self-inverse.
Then $x$ and $y$ commute $x \circ y$ is also self-inverse.
== Proof ==
Let the identity element of $\struct {G, \circ}$ be $e_G$.
=== Necessary Condition ===
Let $x$ and $y$ commute.
Then:
Thus $\paren {x \circ y} \circ \paren {x \circ y} = e_G$, proving that $x \circ y$ is self-inverse.
=== Sufficient Condition ===
Now, suppose that $x \circ y$ is self-inverse.
We already have that $x$ and $y$ are self-inverse.
Thus:
:$\paren {x \circ x} \circ \paren {y \circ y} = e_G \circ e_G = e_G$
Because $x \circ y$ is self-inverse, we have:
:$\paren {x \circ y} \circ \paren {x \circ y} = e_G$
Thus:
So $x$ and $y$ commute.
== Sources ==
* : Chapter $\text {I}$: The Group Concept: Examples: $(4)$
* : Chapter $4$. Groups: Exercise $14$
Category:Group Theory
Category:Commutativity
Self-Locating Number in Pi/Sequence

== Theorem ==
The sequence of self-locating numbers in $\pi$ starts:
:$1, 16 \, 470, 44 \, 899, 79 \, 873 \, 884, 711 \, 939 \, 213, 36 \, 541 \, 622 \, 473, 45 \, 677 \, 255 \, 610, 62 \, 644 \, 957 \, 128, 656 \, 430 \, 109 \, 694$
== Sources ==
* : Cool Numbers: Self-location and $\pi$
Category:Self-Locating Numbers in Pi
Self-Product of Standard Ordered Basis Element equals 1

== Theorem ==
Let $\tuple {\mathbf i, \mathbf j, \mathbf k}$ be the standard ordered basis of Cartesian $3$-space $S$.
Then:
:$\mathbf i^2 = \mathbf j^2 = \mathbf k^2 = 1$
where $\mathbf i^2$ and so on denotes the square of a vector quantity:
:$\mathbf i^2 := \mathbf i \cdot \mathbf i$
== Proof ==
By definition, the Cartesian $3$-space is a frame of reference consisting of a rectangular coordinate system.
By definition of Component of Vector in $3$-space, the vectors $\mathbf i$, $\mathbf j$ and $\mathbf k$ are the unit vectors in the direction of the $x$-axis, $y$-axis and $z$-axis respectively.
Hence $\mathbf i^2$ is the square of a unit vector:
:$\mathbf i^2 = \norm {\mathbf i}^2 = 1^2 = 1$
and the same for $\mathbf j^2$ and $\mathbf k^2$.
== Also see ==
* Dot Product of Elements of Standard Ordered Basis
== Sources ==
* : Chapter $\text {II}$: The Products of Vectors: $2$. The Scalar Product: $(2.6)$
* : Chapter $\text I$: Vector Algebra: $\S 2$. $(3)$
* : Chapter $1$ Vector Analysis $1.3$ Scalar or Dot Product: $(1.22 a)$
Category:Dot Product
Category:Standard Ordered Bases
Semantic Consequence Union Negation

== Theorem ==
Let $U$ be a set of propositional formulas.
Let $P$ be a propositional formula.
Let $U \models P$ denote that $U$ is a semantic consequence $P$.
Then:
:$U \models P$
iff:
:$U \cup \set {\neg P}$ has no models.
== Proof ==
=== Sufficient Condition ===
 $U \models P$.
Let $\MM$ be a model such that:
:$\MM \models U \cup \set {\neg P}$
Then by definition of $\MM$ being a model, we have that:
:$\MM \models U$
and by definition of semantic consequence:
:$\MM \models P$
So we have that $\MM \models P$ and $\MM \models \neg P$
By definition of contradiction, it follows that there can be no such model.
So $U \models P$ is a sufficient condition for $U \cup \set {\neg P}$ to have no models.
=== Necessary Condition ===
Suppose that $U \cup \set {\neg P}$ has no models.
There are the following possibilities:
$(1): \quad \neg P$ has no models, in which case it is itself a contradiction.
Hence from Tautology and Contradiction, $P$ is a tautology.
Hence $P$ is true under every model.
Hence whatever $U$ may be, every model of $U$ is also a model of $P$:
:$U \models P$
$(2): \quad U$ has no models, in which case every model of $U$ is also a model of $P$ vacuously, and so:
:$U \models P$
$(3): \quad$ There exists at least one model of $U$, but each one does not model $\neg P$.
Let $\MM$ be such a model.
We have that:
:$\MM \not \models \neg P$
so by definition of negation:
:$\MM \models P$
Thus $\MM \models U$ implies that $\MM \models P$.
Hence by definition:
:$U \models P$
In all cases $U \models P$.
So $U \models P$ is a necessary condition for $U \cup \set {\neg P}$ to have no models.
== Sources ==
* : $\S 1.7$:
::Evidently $\mathbf A$ is a semantic consequence of $\mathbf H$ the set $\mathbf H \cup \set {\neg \mathbf A}$ has no models.
Category:Propositional Logic
Semantic Consequence as Tautological Conditional

== Theorem ==
Let $\FF$ be a finite set of WFFs of propositional logic.
Let $\mathbf A$ be another WFF.
Then the following are equivalent:
that is, $\mathbf A$ is a semantic consequence of $\FF$ $\ds \bigwedge \FF \implies \mathbf A$ is a tautology.
Here, $\ds \bigwedge \FF$ is the conjunction of $\FF$.
== Proof ==
=== Necessary Condition ===
let:
:$\FF \models_{\mathrm {BI} } \mathbf A$
 $\ds \bigwedge \FF \implies \mathbf A$ were not a tautology.
Then there exists a boolean interpretation $v$ such that:
:$\map v {\ds \bigwedge \FF} = \T$
:$\map v {\mathbf A} = \F$
by definition of the boolean interpretation of $\implies$.
It now follows from the boolean interpretation of conjunction that:
:$\map v {\mathbf B} = \T$
for every $\mathbf B \in \FF$.
Hence, by definition of model:
:$v \models_{\mathrm {BI} } \FF$
It now follows from our assumption that:
:$\map v {\mathbf A} = \T$
This is a contradiction, hence $\ds \bigwedge \FF \implies \mathbf A$ is a tautology.
=== Sufficient Condition ===
Let $\ds \bigwedge \FF \implies \mathbf A$ be a tautology.
Let $v$ be an arbitrary model of $\FF$.
Then:
:$\map v {\mathbf B} = \T$
for every $\mathbf B \in \FF$, whence by the boolean interpretation of conjunction:
:$\map v \FF = \T$
Since $\ds \bigwedge \FF \implies \mathbf A$ is a tautology, it must be the case that:
:$\map v {\mathbf A} = \T$
Hence, since $v$ was arbitrary:
:$\FF \models_{\mathrm {BI} } \mathbf A$
== Sources ==
* : $\S 2.5.3$: Theorem $2.50$
* : $\S 2.10$: Exercise $2.16$
Category:Boolean Interpretations
Semantic Consequence is Transitive

== Theorem ==
Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF, \GG$ and $\HH$ be sets of $\LL$-formulas.
Suppose that:
Then $\FF \models_{\mathscr M} \HH$.
== Proof ==
Let $\MM$ be an $\mathscr M$-structure.
By assumption, if $\MM$ is a model of $\FF$, it is one of $\GG$ as well.
But any model of $\GG$ is also a model of $\HH$.
In conclusion, any model of $\FF$ is also a model of $\HH$.
Hence the result, by definition of semantic consequence.
Category:Formal Semantics
Semantic Consequence of Set Union Formula

== Theorem ==
Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be a set of logical formulas from $\LL$.
Let $\phi$ be an $\mathscr M$-semantic consequence of $\FF$.
Let $\psi$ be another logical formula.
Then:
:$\FF \cup \set \psi \models_{\mathscr M} \phi$
that is, $\phi$ is also a semantic consequence of $\FF \cup \set \psi$.
== Proof ==
This is an immediate consequence of Semantic Consequence of Superset.
== Also see ==
* Semantic Consequence of Superset
== Sources ==
* : $\S 2.5.3$: Theorem $2.53$
* : $\S 2.10$: Exercise $2.16$
Category:Formal Semantics
Semantic Consequence of Set minus Tautology

== Theorem ==
Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be a set of logical formulas from $\LL$.
Let $\phi$ be an $\mathscr M$-semantic consequence of $\FF$.
Let $\psi \in \FF$ be a tautology.
Then:
:$\FF \setminus \set \psi \models_{\mathscr M} \phi$
that is, $\phi$ is also a semantic consequence of $\FF \setminus \set \psi$.
== Proof ==
Let $\MM$ be a model of $\FF \setminus \set \psi$.
Since $\psi$ is a tautology, it follows that:
:$\MM \models_{\mathscr M} \psi$
Hence:
:$\MM \models \FF$
which, , entails:
:$\MM \models \phi$
Since $\MM$ was arbitrary, it follows by definition of semantic consequence that:
:$\FF \setminus \set \psi \models_{\mathscr M} \phi$
== Sources ==
* : $\S 2.5.3$: Theorem $2.54$
* : $\S 2.10$: Exercise $2.16$
Category:Formal Semantics
Semantic Consequence of Superset

== Theorem ==
Let $\LL$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\LL$.
Let $\FF$ be a set of logical formulas from $\LL$.
Let $\phi$ be an $\mathscr M$-semantic consequence of $\FF$.
Let $\FF'$ be another set of logical formulas.
Then:
:$\FF \cup \FF' \models_{\mathscr M} \phi$
that is, $\phi$ is also a semantic consequence of $\FF \cup \FF'$.
== Proof ==
Any model of $\FF \cup \FF'$ is a fortiori also a model of $\FF$.
By definition of semantic consequence all models of $\FF$ are models of $\phi$.
Therefore all models of $\FF \cup \FF'$ are also models of $\phi$.
Hence:
:$\FF \cup \FF' \models_{\mathscr M} \phi$
as desired.
Category:Formal Semantics
Semantic Consequence preserved in Supersignature

== Theorem ==
Let $\LL, \LL'$ be signatures for the language of predicate logic.
Let $\LL'$ be a supersignature of $\LL$.
Let $\mathbf A$ be an $\LL$-sentence.
Let $\Sigma$ be a set of $\LL$-sentences.
Then the following are equivalent:
:$\AA \models_{\mathrm{PL} } \mathbf A$ for all $\LL$-structures $\AA$ for which $\AA \models_{\mathrm{PL} } \Sigma$
:$\AA' \models_{\mathrm{PL} } \mathbf A$ for all $\LL'$-structures $\AA'$ for which $\AA' \models_{\mathrm{PL} } \Sigma$
where $\models_{\mathrm{PL} }$ denotes the models relation.
That is to say, the notion of semantic consequence is preserved in passing to a supersignature.
== Proof ==
== Sources ==
* : $\text{II}.8$ Further Semantic Notions: Lemma $\text{II}.8.15$
Category:Model Theory for Predicate Logic
Semantic Tableau Algorithm

== Algorithm ==
Let $\mathbf A$ be a WFF of propositional logic.
The purpose of this algorithm is to create a completed semantic tableau $T$ for $\mathbf A$.
:Step 1: Start with a labeled tree $T$ comprising only a root node labeled with the singleton $\set {\mathbf A}$.
:Step 2: Choose a leaf node $t$ of $T$ that has not yet been marked. Let $\map U t$ be the set that labels $t$.
:Step 3: If $\map U t$ is a set of literals, mark $t$ as follows:
::a): If $\map U t$ contains a complementary pair, mark it closed, $\times$, and go to Step 2.
::b): Otherwise, mark it open, $\odot$, and go to Step 2.
:Step 4: Choose a formula $\mathbf B \in \map U t$ that is not a literal. Classify $\mathbf B$ as an $\alpha$-formula or a $\beta$-formula, and determine $\mathbf B_1, \mathbf B_2$ accordingly.
::a): If $\mathbf B$ is an $\alpha$-formula, add a child $t'$ to $t$, labeled $\map U {t'} = \paren {\map U t \setminus \set {\mathbf B} } \cup \set {\mathbf B_1, \mathbf B_2}$.
::b): If $\mathbf B$ is a $\beta$-formula, add two children $t', t' '$ to $t$ with labels:
::::$\map U {t'} = \paren {\map U t \setminus \set {\mathbf B} } \cup \set {\mathbf B_1}$
::::$\map U {t' '} = \paren {\map U t \setminus \set {\mathbf B} } \cup \set {\mathbf B_2}$
:Step 5: Go to Step 2 if there remain leaves that are not marked. Otherwise, stop.
=== Finiteness ===
The finiteness of this algorithm is demonstrated on Semantic Tableau Algorithm Terminates.
=== Heuristics ===
== Sources ==
* : $\S 2.6.2$: Algorithm $2.64$
Category:Propositional Logic
Semantic Tableau Algorithm/Heuristics

== Algorithm ==
The Semantic Tableau Algorithm can be made more efficient by using the following heuristic adaptations.
Firstly, the addition of a Step 2.5:
:Step 2.5: If $\map U t$ contains a complementary pair of formulas, mark $t$ closed and go to Step 2.
Secondly, the following modification to the initial part of Step 4:
:Step 4: If possible, choose an $\alpha$-formula $\mathbf B \in \map U t$; otherwise, choose a $\beta$-formula $\mathbf B$. Determine $\mathbf B_1, \mathbf B_2$ corresponding to $\mathbf B$ being an $\alpha$-formula or a $\beta$-formula.
== Also see ==
* Correctness of Heuristics for Semantic Tableau Algorithm
== Sources ==
* : $\S 2.6.4$
Category:Propositional Logic
Semantic Tableau Algorithm is Decision Procedure for Tautologies

== Theorem ==
The Semantic Tableau Algorithm is a decision procedure for tautologies.
== Proof ==
Let $\mathbf A$ be a WFF of propositional logic.
The Semantic Tableau Algorithm applied to $\neg \mathbf A$ yields a completed tableau for $\neg \mathbf A$.
By , this completed tableau decides if $\mathbf A$ is a tautology.
== Sources ==
* : $\S 2.7$: Corollary $2.70$
Category:Propositional Logic
Semantically Equivalent Terms are Equal

== Theorem ==
Let $\tau_1, \tau_2$ be terms.
Suppose that they are semantically equivalent with respect to the empty set.
Then $\tau_1 = \tau_2$.
== Proof ==
== Sources ==
* : $\mathrm{II}.8$ Further Semantic Notions: Exercise $\mathrm{II.8.5}$
Category:Predicate Logic
Semi-Eulerian Graph/Examples/Arbitrary Example 1

== Example of Semi-Eulerian Graph ==
The following is a semi-Eulerian graph:
:
An example of an Eulerian trail is:
:$A \to B \to C \to D \to E \to B \to D \to A \to E$
== Sources ==
* 
* 
Category:Examples of Semi-Eulerian Graphs
Semi-Inner Product/Examples/Sequences with Finite Support

== Example of Semi-Inner Product ==
Let $\GF$ be a subfield of $\C$.
Let $V$ be the vector space of sequences with finite support over $\GF$.
Let $\innerprod \cdot \cdot: V \times V \to \GF$ be the mapping defined by:
:$\ds \innerprod {\sequence {a_n} } {\sequence {b_n} } = \sum_{n \mathop = 1}^\infty a_{2 n} \overline {b_{2 n} }$
Then $\innerprod \cdot \cdot$ is a semi-inner product on $V$ but not an inner product on $V$.
== Proof ==
First of all, note that $V$ contains only the sequences with finite support.
Therefore, for each $\sequence {a_n}, \sequence{b_n}$ there exists $N \in \N$ such that:
:$\forall n \ge N: a_n = b_n = 0$
and hence:
:$\ds \innerprod {\sequence {a_n} } {\sequence {b_n} } = \sum_{n \mathop = 1}^\infty a_{2 n} \overline {b_{2 n} } = \sum_{n \mathop = 1}^{N / 2} a_{2 n} \overline {b_{2 n} }$
so that $\innerprod \cdot \cdot: V \times V \to \GF$ is indeed defined.
Now checking the axioms for a semi-inner product in turn:
=== $(1)$ Conjugate Symmetry ===
=== $(2)$ Sesquilinearity ===
=== $(3)$ Non-Negative Definiteness ===
Hence $\innerprod \cdot \cdot$ is a semi-inner product.
Because any sequence $\sequence{a_n}$ such that $a_{2n} = 0$ for all $n \in \N$ will have:
:$\innerprod {\sequence{a_n} } {\sequence{a_n} } = 0$
it follows that $\innerprod \cdot \cdot$ is not an inner product.
== Sources ==
* : $\text{I}$ Hilbert Spaces: $\S 1.$ Elementary Properties and Examples: Example $1.2$
Category:Examples of Semi-Inner Products
Semi-Inner Product induces Inner Product on Quotient

== Theorem ==
Let $\GF \in \set {\R, \C}$. 
Let $\struct {V, \innerprod \cdot \cdot}$ be a semi-inner product space over $\GF$.
Let:
:$N = \set {x \in V : \innerprod x x = 0}$
Let $X/N$ be the quotient vector space of $X$ modulo $N$. 
Define:
:$\innerprod {x + N} {y + N}_{X/N} = \innerprod x y$
for each $x, y \in X$. 
Then $\innerprod \cdot \cdot_{X/N}$ is an inner product on $X/N$.
== Proof ==
First note that Zero Set of Semi-Inner Product is Vector Subspace shows that $N$ is a vector subspace and hence $X/N$ is well-defined.
We show that $\innerprod \cdot \cdot_{X/N}$ is well-defined. 
We need to show that if $x, y, x', y' \in X$ are such that $x - x' \in N$ and $y - y' \in N$, then $\innerprod x y = \innerprod {x'} {y'}$. 
We have:
From Cauchy-Bunyakovsky-Schwarz Inequality: Inner Product Spaces, we have:
:$\cmod {\innerprod {x - x'} {y - y'} }^2 \le \innerprod {x - x'} {x - x'} \innerprod {y - y'} {y - y'} = 0$
since $x - x' \in N$ and $y - y' \in N$.
We also have:
:$\cmod {\innerprod {x - x'} {y'} }^2 \le \innerprod {x - x'} {x - x'} \innerprod {y'} {y'} = 0$
since $x - x' \in N$.
Finally:
:$\cmod {\innerprod {x'} {y - y'} }^2 \le \innerprod {x'} {x'} \innerprod {y - y'} {y - y'} = 0$ 
since $y - y' \in N$. 
So we have $\innerprod {x - x'} {y - y'} + \innerprod {x - x'} {y'} + \innerprod {x'} {y - y'} = 0$ and we obtain:
:$\innerprod x y = \innerprod {x'} {y'}$
Hence $\innerprod \cdot \cdot_{X/N}$ is well-defined.
We just need to verify that $\innerprod \cdot \cdot_{X/N}$ is an inner product on $X/N$.
=== Proof of conjugate symmetry ===
Let $x, y \in X$.
We have:
=== Proof of linearity in first argument ===
Let $x, y, z \in X$, we have:
=== Proof of non-negative definiteness ===
Let $x \in X$.
We have:
:$\innerprod {x + N} {x + N}_{X/N} = \innerprod x x \in \R_{\ge 0}$
From non-negative definiteness of $\innerprod \cdot \cdot$ .
=== Proof of positiveness ===
Let $x \in X$.
Again we have:
:$\innerprod {x + N} {x + N}_{X/N} = \innerprod x x$
So $\innerprod {x + N} {x + N}_{X/N} = 0$ $\innerprod x x = 0$ $x \in N$.
This is, $x + N = {\mathbf 0}_{X/N}$.
Category:Semi-Inner Product Spaces
Category:Quotient Vector Spaces
Semi-Inner Product with Zero Vector

== Theorem ==
Let $\struct {V, \innerprod \cdot \cdot}$ be a semi-inner product space.
Let $\mathbf 0_V$ be the zero vector of $V$.
Then for all $v \in V$:
:$\innerprod {\mathbf 0_V} v = \innerprod v {\mathbf 0_V} = 0$
== Proof ==
== Also see ==
* Inner Product with Zero Vector
== Sources ==
* : $\text{I}$ Hilbert Spaces: $\S 1.$ Elementary Properties and Examples: Definition $1.1$
Category:Semi-Inner Product Spaces
Semidirect Product is Abelian iff Components are Abelian and Action is Trivial

== Theorem ==
Let $N$ and $H$ be groups.
Let $H$ act by automorphisms on $N$ via $\phi$.
Let $N \rtimes_\phi H$ be the corresponding semidirect product.
Then the following are equivalent:
:$(1): \quad N \rtimes_\phi H$ is abelian
:$(2): \quad N$ and $H$ are abelian and $H$ acts trivially
== Proof ==
=== $(1)$ implies $(2)$ ===
Let $n \in N$, $h \in H$.
From $\tuple {n, e} \tuple {e, h} = \tuple {e,h} \tuple {n, e}$ we have $n \map {\phi_e} e = e \map {\phi_h} n$.
Thus $H$ acts trivially.
By Semidirect Product with Trivial Action is Direct Product, $N \rtimes_\phi H = N \times H$.
By External Direct Product of Abelian Groups is Abelian Group, $N$ and $H$ are abelian.
=== $(2)$ implies $(1)$ ===
By Semidirect Product with Trivial Action is Direct Product, $N \rtimes_\phi H = N \times H$.
By External Direct Product of Abelian Groups is Abelian Group, $N \rtimes_\phi H$ is abelian.
Category:Semidirect Products