avewright/proofwiki-math huggingface dataset:
Theorem: Vector Magnitude is Invariant Under Rotation

Let $\mathbf v$ be an arbitrary vector in the Cartesian plane $\CC$.
Let the coordinate system then be rotated in the anticlockwise direction by an arbitrary angle $\theta$.
Then:
the magnitude of $\mathbf v$ is unchanged in the new coordinate system.

Proof:
We offer three equivalent statements:
By definition, rotation of the coordinate system affects the coordinates and not the vector.
{{tidy}}
Rotation is a rigid transformation.  It does not change side lengths or angles.  
The equations of rotation of coordinates are linear transformations.
{{qed}}
Theorem: Vector Sum of Rotated Triangle is Zero

Let $T = \triangle ABC$ be embedded in the Cartesian plane $\CC$.
Let the sides of $T$ be directed line segments, that is, vectors.
Let $\CC$ be rotated anticlockwise about the origin by an angle $\theta$.
Let the triangle $T$, as defined in the rotated coordinates, be T'.
Let $\mathbf{0}$ be the zero vector.
Let $+$ be the vector sum.
Then:
:$T' = \mathbf{AB}' + \mathbf{BC}' + \mathbf{CA}' = \mathbf{0}$

Proof:
Let $\mathbf{AB}$ have the same magnitude as  $AB$ and direction from $A$ to $B$.
Let similar definitions hold for $\mathbf{BC}$ and $\mathbf{CA}$.
By definition of vectors:
:$\mathbf{AB} = \paren { B_x - A_x, B_y - A_y }$
Let $\mathbf{AB}$ in the rotated coordinates be designated $\mathbf{AB}'$.
By definition of vectors:
:$\mathbf{AB}' = \paren { B_x' - A_x', B_y' - A_y' }$
By Equations defining Plane Rotation the $x$-component of $\mathbf{AB}'$ is:
:$\paren { B_x \cos \theta - B_y \sin \theta - A_x \cos \theta + A_y \sin \theta }$
By Vector Magnitude is Invariant Under Rotation the above expression is equal to:
:$\paren { B_x - A_x }$
and the y-component of $\mathbf{AB}'$ is:
:$\paren { B_x \sin \theta + B_y \cos \theta - A_x \sin \theta - A_y \cos \theta }$
By Vector Magnitude is Invariant Under Rotation the above expression is equal to:
:$\paren { B_y - A_y }$
That is, the sides of $T$ are equal to the sides of $T'$:
:$\norm {AB} = \norm {AB'}$
:$\norm {BC} = \norm {BC'}$
:$\norm {CA} = \norm {CA'}$
By Triangle Side-Side-Side Congruence:
:$T \cong T'$
$T'$ consists of the vectors $\mathbf{AB}' + \mathbf{BC}' + \mathbf{CA}'$.
By definition, the terminal point of $\mathbf{CA}$ is the initial point of $\mathbf{AB}$.
It follows that:
$T = \mathbf{AB} + \mathbf{BC} + \mathbf{CA} = \mathbf{0}$
By definition, the terminal point of $\mathbf{CA}'$ is the initial point of $\mathbf{AB}'$.
It follows that:
$T' = \mathbf{AB}' + \mathbf{BC}' + \mathbf{CA}' = \mathbf{0}$
{{qed}}
Category:Vectors
Category:Triangles
mrmbce6oba2aerfepul1o8njxciu6f2
Theorem: Combination Theorem for Bounded Real-Valued Functions/Sum Rule

:$f + g$ is a bounded real-valued function

Proof:
By definition of bounded real-valued function
:$\exists M_f \in \R_{\ge 0} : \forall s \in S : \size{\map f s} \le M_f$
and
:$\exists M_g \in \R_{\ge 0} : \forall s \in S : \size{\map g s} \le M_g$
Let $M = M_f + M_g$.
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \size{\map {\paren{f + g} } s}
      | r = \size{\map f s + \map g s}
      | c = {{Defof|Pointwise Addition of Real-Valued Functions}}
}}
{{eqn | o = \le
      | r = \size{\map f s} + \size{\map g s}
      | c = Triangle Inequality for Real Numbers
}}
{{eqn | o = \le
      | r = M_f + M_g
      | c = {{Defof|Bounded Real-Valued Function}}
}}
{{eqn | r = M
      | c = Definition of $M$
}}
{{end-eqn}}
It follows that $f + g$ is a bounded real-valued function by definition.
{{qed}}
Category:Combination Theorem for Bounded Real-Valued Functions
sc7hw2cwewr0n3cmuw9h3wu15kobg2u
Theorem: Combination Theorem for Bounded Real-Valued Functions/Negation Rule

:$-f$ is a bounded real-valued function

Proof:
By definition of bounded real-valued function
:$\exists M \in \R_{\ge 0} : \forall s \in S : \size{\map f s} \le M$
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \size{\map {\paren{-f} } s}
      | r = \size{-\map f s}
      | c = {{Defof|Absolute Value of Real-Valued Function}}
}}
{{eqn | r = \size{\map f s}
      | c = Absolute Value of Negative
}}
{{eqn | o = \le
      | r = M
      | c = {{Defof|Bounded Real-Valued Function}}
}}
{{end-eqn}}
It follows that $-f$ is a bounded real-valued function by definition.
{{qed}}
Category:Combination Theorem for Bounded Real-Valued Functions
2pz41nl5d6kfbvpbkfhrp566awe5iy4
Theorem: Combination Theorem for Bounded Real-Valued Functions/Product Rule

:$f g$ is a bounded real-valued function

Proof:
By definition of bounded real-valued function
:$\exists M_f \in \R_{\ge 0} : \forall s \in S : \size{\map f s} \le M_f$
and
:$\exists M_g \in \R_{\ge 0} : \forall s \in S : \size{\map g s} \le M_g$
Let $M = M_f M_g$.
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \size{\map {\paren{f g} } s}
      | r = \size{\map f s \map g s}
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions|Pointwise Product}}
}}
{{eqn | r = \size{\map f s} \size{\map g s}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | o = \le
      | r = M_f M_g
      | c = {{Defof|Bounded Real-Valued Function}}
}}
{{eqn | r = M
      | c = Definition of $M$
}}
{{end-eqn}}
It follows that $f g$ is a bounded real-valued function by definition.
{{qed}}
Category:Combination Theorem for Bounded Real-Valued Functions
gg2c75o83onev30ewpenkhfx0qfxtt4
Theorem: Combination Theorem for Bounded Real-Valued Functions/Absolute Value Rule

:$\size f$ is a bounded real-valued function

Proof:
By definition of bounded real-valued function
:$\exists M \in \R_{\ge 0} : \forall s \in S : \size{\map f s} \le M$
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \bigsize{\map {\size f} s}
      | r = \bigsize{\size{\map f s} }
      | c = Definition of $\size f$
}}
{{eqn | r = \size{\map f s}
      | c = {{Defof|Absolute Value}}
}}
{{eqn | o = \le
      | r = M
      | c = {{Defof|Bounded Real-Valued Function}}
}}
{{end-eqn}}
It follows that $\size f$ is a bounded real-valued function by definition.
{{qed}}
Category:Combination Theorem for Bounded Real-Valued Functions
glykhq1jvbdm2t5ein7o6cmb5r9kvds
Theorem: Combination Theorem for Bounded Real-Valued Functions/Maximum Rule

:$f \vee g$ is a bounded real-valued function

Proof:
By definition of bounded real-valued function
:$\exists M_f \in \R_{\ge 0} : \forall s \in S : \size{\map f s} \le M_f$
and
:$\exists M_g \in \R_{\ge 0} : \forall s \in S : \size{\map g s} \le M_g$
From Negative of Absolute Value:
:$\forall s \in S : \map f s \le \size{\map f s}$
and
:$\forall s \in S : \map g s \le \size{\map g s}$
Let $M = \max \set{M_f, M_g}$.
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \bigsize{\map {\paren{f \vee g} } s}
      | r = \bigsize{\max\set {\map f s, \map g s} }
      | c = {{Defof|Pointwise Maximum of Real-Valued Functions}}
}}
{{eqn | r = \bigsize{\max\set {\size{\map f s}, \size{\map g s} } }
      | c = Max Operation Preserves Total Ordering
}}
{{eqn | o = \le
      | r = \bigsize{\max\set {M_f, M_g} }
      | c = Max Operation Preserves Total Ordering
}}
{{eqn | r = \bigsize M
      | c = Definition of $M$
}}
{{eqn | r = M
      | c = as $M \ge 0$
}}
{{end-eqn}}
It follows that $f \vee g$ is a bounded real-valued function by definition.
{{qed}}
Category:Combination Theorem for Bounded Real-Valued Functions
hoi62ytmjzr4hu1wnwq8dadm1f3azv0
Theorem: Combination Theorem for Bounded Real-Valued Functions/Minimum Rule

:$f \wedge g$ is a bounded real-valued function

Proof:
By definition of bounded real-valued function
:$\exists M_f \in \R_{\ge 0} : \forall s \in S : \size{\map f s} \le M_f$
and
:$\exists M_g \in \R_{\ge 0} : \forall s \in S : \size{\map g s} \le M_g$
From Negative of Absolute Value:
:$\forall s \in S : \map f s \le \size{\map f s}$
and
:$\forall s \in S : \map g s \le \size{\map g s}$
Let $M = \min \set{M_f, M_g}$.
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \bigsize{\map {\paren{f \wedge g} } s}
      | r = \bigsize{\min\set {\map f s, \map g s} }
      | c = {{Defof|Pointwise Minimum of Real-Valued Functions}}
}}
{{eqn | r = \bigsize{\min\set {\size{\map f s}, \size{\map g s} } }
      | c = Min Operation Preserves Total Ordering
}}
{{eqn | o = \le
      | r = \bigsize{\min\set {M_f, M_g} }
      | c = Min Operation Preserves Total Ordering
}}
{{eqn | r = \bigsize M
      | c = Definition of $M$
}}
{{eqn | r = M
      | c = as $M \ge 0$
}}
{{end-eqn}}
It follows that $f \wedge g$ is a bounded real-valued function by definition.
{{qed}}
Category:Combination Theorem for Bounded Real-Valued Functions
n5u88d0rx0xqg3ppvl792yb3vuglfiy
Theorem: Combination Theorem for Continuous Real-Valued Functions/Sum Rule

:$f + g$ is a coninuous real-valued function

Proof:
Follows from:
:Real Numbers form Valued Field
:By definition a valued field is a normed division ring
:Sum Rule for Continuous Mappings into Normed Division Ring
{{qed}}
Category:Combination Theorem for Continuous Real-Valued Functions
gw5n2d3n1xgh3w7j5xzw1r2uopx5130
Theorem: Combination Theorem for Continuous Real-Valued Functions/Negation Rule

:$-f$ is a continuous real-valued function

Proof:
Follows from:
:Real Numbers form Valued Field
:By definition a valued field is a normed division ring
:Negation Rule for Continuous Mappings into Normed Division Ring
{{qed}}
Category:Combination Theorem for Continuous Real-Valued Functions
61huilxlqhgymhb81wpyfoi5z301sc2
Theorem: Combination Theorem for Continuous Real-Valued Functions/Product Rule

:$f g$ is a continuous real-valued function

Proof:
Follows from:
:Real Numbers form Valued Field
:By definition a valued field is a normed division ring
:Product Rule for Continuous Mappings into Normed Division Ring
{{qed}}
Category:Combination Theorem for Continuous Real-Valued Functions
ctgqh8g2eo5tsr62ctxwcwg4nizg8y4
Theorem: Combination Theorem for Continuous Real-Valued Functions/Absolute Value Rule

:$\size f$ is a continuous real-valued function

Proof:
From Absolute Value of Function is Composite with Absolute Value Function:
:$\size{f} = \size{\,\cdot\,} \circ f$
where:
:$\size{\,\cdot\,}$ denotes the absolute value function $\size{\,\cdot\,} : \R \to \R$
:$\size{\,\cdot\,} \circ f$ denotes the composite mapping of $\size{\,\cdot\,}$ with $f$
From Absolute Value Function is Continuous:
:$\size{\,\cdot\,} : \R \to \R$ is continuous
From Composite of Continuous Mappings is Continuous:
:$\size{\,\cdot\,} \circ f$ is continuous
The result follows.
{{qed}}
Category:Combination Theorem for Continuous Real-Valued Functions
mk7txoyuaftjzp9joskw0de9bl5oe48
Theorem: Combination Theorem for Continuous Real-Valued Functions/Maximum Rule

:$f \vee g$ is a continuous real-valued function

Proof:
From Characterization of Pointwise Maximum of Real-Valued Functions:
::$f \vee g = \dfrac 1 2 \paren{f + g + \size{f - g}}$
We have:
{{begin-eqn}}
{{eqn | o = 
      | r = f, g \text{ are continuous real-valued functions} 
}}
{{eqn | o = \leadsto
      | r = f -g \text{ is a continuous real-valued function} 
      | c = Difference Rule for Continuous Real-Valued Functions
}}
{{eqn | o = \leadsto
      | r = \size{f - g} \text{ is a continuous real-valued function} 
      | c = Absolute Value Rule for Continuous Real-Valued Function
}}
{{eqn | o = \leadsto
      | r = f + g + \size{f - g} \text{ is a continuous real-valued function} 
      | c = Sum Rule for Continuous Real-Valued Functions
}}
{{eqn | o = \leadsto
      | r = \dfrac 1 2 \paren{f + g + \size{f - g} } \text{ is a continuous real-valued function} 
      | c = Multiple Rule for Continuous Real-Valued Function
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Combination Theorem for Continuous Real-Valued Functions
0j13cgkp92rag29tee3m75npo6n2h4b
Theorem: Combination Theorem for Continuous Real-Valued Functions/Minimum Rule

:$f \wedge g$ is a continuous real-valued function

Proof:
From Characterization of Pointwise Minimum of Real-Valued Functions:
::$f \vee g = \dfrac 1 2 \paren{f + g - \size{f - g}}$
We have:
{{begin-eqn}}
{{eqn | o = 
      | r = f, g \text{ are continuous real-valued functions} 
}}
{{eqn | o = \leadsto
      | r = f -g \text{ is a continuous real-valued function} 
      | c = Difference Rule for Continuous Real-Valued Functions
}}
{{eqn | o = \leadsto
      | r = \size{f - g} \text{ is a continuous real-valued function} 
      | c = Absolute Value Rule for Continuous Real-Valued Function
}}
{{eqn | o = \leadsto
      | r = g - \size{f - g} \text{ is a continuous real-valued function} 
      | c = Difference Rule for Continuous Real-Valued Functions
}}
{{eqn | o = \leadsto
      | r = f + g - \size{f - g} \text{ is a continuous real-valued function} 
      | c = Sum Rule for Continuous Real-Valued Functions
}}
{{eqn | o = \leadsto
      | r = \dfrac 1 2 \paren{f + g - \size{f - g} } \text{ is a continuous real-valued function} 
      | c = Multiple Rule for Continuous Real-Valued Function
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Combination Theorem for Continuous Real-Valued Functions
azcf96zun2dqd34n0a0jekqyyupna2a
Theorem: Combination Theorem for Bounded Continuous Real-Valued Functions/Sum Rule

:$f + g$ is a bounded coninuous real-valued function

Proof:
Follows from:
* Sum Rule for Bounded Real-Valued Functions
* Sum Rule for Continuous Real-Valued Functions
{{qed}}
Category:Combination Theorem for Bounded Continuous Real-Valued Functions
1eui55ymtva40xaz7z7q4mzo739y4q8
Theorem: Combination Theorem for Bounded Continuous Real-Valued Functions/Negation Rule

:$-f$ is a bounded continuous real-valued function

Proof:
Follows from:
* Negation Rule for Bounded Real-Valued Function
* Negation Rule for Continuous Real-Valued Function
{{qed}}
Category:Combination Theorem for Bounded Continuous Real-Valued Functions
3ib54dvxzda1tpxkfrhqf23skc37upi
Theorem: Combination Theorem for Bounded Continuous Real-Valued Functions/Product Rule

:$f g$ is a bounded continuous real-valued function

Proof:
Follows from:
* Product Rule for Bounded Real-Valued Functions
* Product Rule for Continuous Real-Valued Functions
{qed}}
Category:Combination Theorem for Bounded Continuous Real-Valued Functions
gyep7v1ibm7q32uzdccowdwok87bjbr
Theorem: Combination Theorem for Bounded Continuous Real-Valued Functions/Absolute Value Rule

:$\size f$ is a bounded continuous real-valued function

Proof:
Follows from:
* Absolute Value Rule for Bounded Real-Valued Function
* Absolute Value Rule for Continuous Real-Valued Function
{{qed}}
Category:Combination Theorem for Bounded Continuous Real-Valued Functions
gz0dda15em4azdr34ejal629bvabl5y
Theorem: Combination Theorem for Bounded Continuous Real-Valued Functions/Maximum Rule

:$f \vee g$ is a bounded continuous real-valued function

Proof:
Follows from:
* Maximum Rule for Bounded Real-Valued Functions
* Maximum Rule for Continuous Real-Valued Functions
{{qed}}
Category:Combination Theorem for Bounded Continuous Real-Valued Functions
5dov7q0xan9kj94xfywaaqvmih6wi95
Theorem: Combination Theorem for Bounded Continuous Real-Valued Functions/Minimum Rule

:$f \wedge g$ is a bounded continuous real-valued function

Proof:
Follows from:
* Minimum Rule for Bounded Real-Valued Functions
* Minimum Rule for Continuous Real-Valued Functions
{{qed}}
Category:Combination Theorem for Bounded Continuous Real-Valued Functions
is078cyx8q5r0r920qp4l30v95d3m1r
Theorem: Max Operation Preserves Total Ordering

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $a, b, c, d \in S$:
:$a \preceq b, c \preceq d$
Then:
:$\max \set{a, c} \preceq \max \set{b, d}$
where $\max$ denotes the max operation on $\struct {S, \preceq}$.

Proof:
From Max Operation Equals an Operand, either:
:$\max \set{a, c} = a$
or
:$\max \set{a, c} = c$
{{WLOG}}, suppose:
:$\max \set{a, c} = a$
We have:
{{begin-eqn}}
{{eqn | l = \max \set{a, c}
      | r = a
      | c = {{Hypothesis}}
}}
{{eqn | o = \preceq
      | r = b
      | c = {{Hypothesis}}
}}
{{eqn | o = \preceq
      | r = \max \set{b, d} 
      | c = Max Operation Yields Supremum of Parameters and {{Defof|Supremum}}
}}
{{end-eqn}}
By transitivity of an ordering:
:$\max \set{a, c} \preceq \max \set{b, d}$
{{qed}}
Category:Max Operation
6suhycm0grj8h39ests5pbe0iz2lwkn
Theorem: Min Operation Preserves Total Ordering

Let $\struct {S, \preceq}$ be a totally ordered set.
Let $a, b, c, d \in S$:
:$a \preceq b, c \preceq d$
Then:
:$\min \set{a, c} \preceq \min \set{b, d}$
where $\min$ denotes the min operation on $\struct {S, \preceq}$.

Proof:
From Min Operation Equals an Operand, either:
:$\min \set{b, d} = b$
or
:$\min \set{b, d} = d$
{{WLOG}}, suppose:
:$\min \set{b, d} = b$
We have:
{{begin-eqn}}
{{eqn | l = \min \set{a, c}
      | o = \preceq
      | r = a
      | c = Min Operation Yields Infimum of Parameters and {{Defof|Infimum}}
}}
{{eqn | o = \preceq
      | r = b
      | c = {{Hypothesis}}
}}
{{eqn | r = \min \set{b, d} 
      | c = {{Hypothesis}}
}}
{{end-eqn}}
By transitivity of an ordering:
:$\min \set{a, c} \preceq \min \set{b, d}$
{{qed}}
Category:Min Operation
5o23u8qpe8ou7iok7ddrp76qjbehf0n
Theorem: Characterization of Pointwise Maximum of Real-Valued Functions

Let $S$ be a set.
Let $\R$ denote the real number line.
Let $f, g :S \to \R$ be real-valued functions.
Let $f \vee g$ denote the pointwise maximum of $f$ and $g$, that is, $f \vee g$ is the mapping defined by:
:$\forall s \in S : \map {\paren{f \vee g} } s = \max \set{\map f s, \map g s}$
Then:
:$f \vee g = \dfrac 1 2 \paren{f + g + \size{f - g}}$
where:
:$f + g$ denotes the pointwise addition of $f$ and $g$
:$f - g$ denotes the pointwise difference of $f$ and $g$
:$\size{f - g}$ denotes the absolute value of $f - g$
:$\dfrac 1 2 \paren{f + g + \size{f - g}}$ denotes the pointwise scalar multiplication of $f + g + \size{f - g}$ by $\dfrac 1 2$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \map {\paren {f \vee g} } s
      | r = \max \set {\map f x, \map g x}
      | c = {{Defof|Pointwise Maximum of Real-Valued Functions}}
}}
{{eqn | r = \dfrac 1 2 \paren {\map f x + \map g x + \size {\map f x - \map g x} }
      | c = Max is Half of Sum Plus Absolute Difference
}}
{{eqn | r = \dfrac 1 2 \paren {\map f x + \map g x + \size {\map {\paren{f - g} } s} }
      | c = {{Defof|Pointwise Difference of Real-Valued Functions}}
}}
{{eqn | r = \dfrac 1 2 \paren {\map f x + \map g x + \map {\size{f - g} } s}
      | c = {{Defof|Absolute Value of Real-Valued Function}}
}}
{{eqn | r = \dfrac 1 2 \map {\paren {f + g + \size {f - g} } } s
      | c = {{Defof|Pointwise Addition of Real-Valued Functions}}
}}
{{eqn | r = \map {\paren {\dfrac 1 2 \paren {f + g + \size {f - g} } } } s
      | c = {{Defof|Pointwise Scalar Multiplication of Real-Valued Function}}
}}
{{end-eqn}}
By definition of equality of mappings:
:$f \vee g = \dfrac 1 2 \paren{f + g + \size{f - g}}$
{{qed}}
Category:Real-Valued Functions
qp02jfrlyfb3w87jg3gs2ro9skozc17
Theorem: Orthocenter and Incenter Coincide if Triangle is Equilateral

Let $\triangle ABC$ be an equilateral triangle.
Let $G$ be the orthocenter of $\triangle ABC$.
Then:
$G$ is the incenter of $\triangle ABC$.

Proof:
Draw the circumcircle of $\triangle ABC$ through points $A, B,$ and $C$.
300px
Given:  $G$ is the orthocenter of $\triangle ABC$.
By Orthocenter, Centroid and Circumcenter Coincide iff Triangle is Equilateral:
:$G$ is also the centroid and circumcenter of $\triangle ABC$.
{{begin-eqn}}
{{eqn | l = AB
      | r = AC = CB
      | c = {{Defof|Equilateral Triangle}}
}}
{{eqn | l = AD
      | r = DB
      | c = Medians of Triangle Meet at Centroid
}}
{{eqn | l = AD
      | r = \dfrac 1 2 AB
      | c = {{Defof|Median}}
}}
{{eqn | l = AF
      | r = \dfrac 1 2 AC
      | c = {{Defof|Median}}
}}
{{eqn | l = AD
      | r = AF
      | c = Substitution
}}
{{eqn | l = AG
      | r = AG
      | c = Shared
}}
{{eqn | l = \angle ADG
      | r = \angle AFG
      | c = Given both are right angles
}}
{{eqn | l = \triangle ADG
      | o = \cong
      | r = \triangle AFG
      | c = Triangle Right-Angle-Hypotenuse-Side Congruence
}}
{{eqn | l = AG
      | r = BG = CG
      | c = Radii of the same circle
}}
{{eqn | l = DG
      | r = DG
      | c = Shared
}}
{{eqn | l = \triangle ADG
      | o = \cong
      | r = \triangle BDG
      | c = Triangle Side-Side-Side Congruence
}}
{{eqn | l = \triangle AFG
      | o = \cong
      | r = \triangle BDG
      | c = {{EuclidCommonNotionLink|1}}
}}
{{end-eqn}}
By {{mutatis}}:
all the smaller triangles are congruent.
So:
:$DG = EG = FG$
By definition of incircle:
:$DG$ is a radius of the incircle of $\triangle ABC$.
By definition of center: 
:$G$ is the center of the incircle of $\triangle ABC$
{{qed}}
Category:Equilateral Triangles
Category:Orthocenters of Triangles
Category:Incircles of Triangles
j9aqbkc93xpsp32r1rkgfn5gf62wrxq
Theorem: Characterization of Pointwise Minimum of Real-Valued Functions

Let $S$ be a set.
Let $\R$ denote the real number line.
Let $f, g :S \to \R$ be real-valued functions.
Let $f \wedge g$ denote the pointwise maximum of $f$ and $g$, that is, $f \wedge g$ is the mapping defined by:
:$\forall s \in S : \map {\paren {f \wedge g} } s = \min \set {\map f s, \map g s}$
Then:
:$f \wedge g = \dfrac 1 2 \paren {f + g - \size {f - g} }$
where:
:$f + g$ denotes the pointwise addition of $f$ and $g$
:$f - g$ denotes the pointwise difference of $f$ and $g$
:$\size{f - g}$ denotes the absolute value of $f - g$
:$\dfrac 1 2 \paren {f + g - \size {f - g}}$ denotes the pointwise scalar multiplication of $f + g - \size {f - g}$ by $\dfrac 1 2$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \map {\paren {f \wedge g} } s
      | r = \min \set {\map f s, \map g s}
      | c = {{Defof|Pointwise Minimum of Real-Valued Functions}}
}}
{{eqn | r = \dfrac 1 2 \paren {\map f s + \map g x - \size {\map f x - \map g x} }
      | c = Min is Half of Sum Less Absolute Difference
}}
{{eqn | r = \dfrac 1 2 \paren {\map f s + \map g s - \size{\map {\paren {f - g} } s} }
      | c = {{Defof|Pointwise Difference of Real-Valued Functions}}
}}
{{eqn | r = \dfrac 1 2 \paren {\map f s + \map g s - \map {\size {f - g} } s}
      | c = {{Defof|Absolute Value of Real-Valued Function}}
}}
{{eqn | r = \dfrac 1 2 \paren {\map {\paren {f + g} } s - \map {\size {f - g} } s}
      | c = {{Defof|Pointwise Addition of Real-Valued Functions}}
}}
{{eqn | r = \dfrac 1 2 \map {\paren {f + g - \size {f - g} } } s
      | c = {{Defof|Pointwise Difference of Real-Valued Functions}}
}}
{{eqn | r = \map {\paren {\dfrac 1 2 \paren {f + g - \size {f - g} } } } s
      | c = {{Defof|Pointwise Scalar Multiplication of Real-Valued Function}}
}}
{{end-eqn}}
By definition of equality of mappings:
:$f \wedge g = \dfrac 1 2 \paren{f + g - \size{f - g}}$
{{qed}}
Category:Real-Valued Functions
ifqwn0gjw82qn4zr2j1rzto1d1s1umg
Theorem: Combination Theorem for Continuous Real-Valued Functions/Difference Rule

:$f - g$ is a coninuous real-valued function

Proof:
From Pointwise Difference is Pointwise Addition with Negation:
:$f - g = f + \paren{-g}$
where:
:$-g$ denotes the pointwise negation of $g$
:$f + \paren{-g}$ denotes the pointwise addition of $f$ and $-g$
From Negation Rule for Continuous Real-Valued Function:
:$-g$ is a contiuous real-valued function
From Sum Rule for Continuous Real-Valued Functions
:$f + \paren{-g}$ is a contiuous real-valued function
The result follows.
{{qed}}
Category:Combination Theorem for Continuous Real-Valued Functions
bwyen4415sdblnnd8c5liee5d03c658
Theorem: Combination Theorem for Continuous Real-Valued Functions/Multiple Rule

:$\lambda f$ is a continuous real-valued function

Proof:
Follows from:
:Real Numbers form Valued Field
:By definition a valued field is a normed division ring
:Multiple Rule for Continuous Mappings into Normed Division Ring
{{qed}}
Category:Combination Theorem for Continuous Real-Valued Functions
jjr6i2ji3qfpjbsqavgzee86ruusar1
Theorem: Real Numbers form Valued Field

The set of real numbers $\R$ forms a valued field under addition, multiplication and absolute value: $\struct {\R, +, \times, \size {\,\cdot\,} }$.

Proof:
From Real Numbers form Field, we have that $\struct {\R, +, \times}$ forms a field.
From Absolute Value is Norm, we have that $\size {\size {\,\cdot\,} }$ is a norm on $\struct {\R, +, \times}$.
Hence $\struct {\R, +, \times, \size {\,\cdot\,} }$ is a valued field by definition.
{{qed}}