Field Product with Zero

Theorem

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$.

Let $a \in F$.

Then:

$a \times 0_F = 0_F$

That is, $0_F$ acts as a zero element of $F$, which justifies its name.

Proof

 $\ds a$ $=$ $\ds a \times 1_F$ Field Axiom $\text M3$: Identity for Product: $1_F$ is the unity of $F$ $\ds$ $=$ $\ds a \times \paren {0_F + 1_F}$ Field Axiom $\text A3$: Identity for Addition $\ds$ $=$ $\ds a \times 0_F + a \times 1_F$ Field Axiom $\text D$: Distributivity of Product over Addition $\ds$ $=$ $\ds a \times 0_F + a$ Field Axiom $\text M3$: Identity for Product $\ds \leadsto \ \$ $\ds \paren {a \times 0_F + a} + \paren {-a}$ $=$ $\ds a + \paren {-a}$ adding $-a$ to both sides $\ds \leadsto \ \$ $\ds a \times 0_F + \paren {a + \paren {-a} }$ $=$ $\ds a + \paren {-a}$ Field Axiom $\text A1$: Associativity of Addition $\ds \leadsto \ \$ $\ds a \times 0_F + 0_F$ $=$ $\ds 0_F$ Field Axiom $\text A4$: Inverses for Addition $\ds \leadsto \ \$ $\ds a \times 0_F$ $=$ $\ds 0_F$ Field Axiom $\text A3$: Identity for Addition

$\blacksquare$