How do I know what we already know in a proof when the assumptions we can use are even more complex?

As others have said in the comments, you know what rules and axioms you can use because you are given or choose a particular collection. One of the most common misunderstandings I see is the thought that there is one set of rules and axioms that all mathematicians agree on. This is especially pernicious in logic but exists in other areas too. Usually what happens is a student sees one definition and assumes that that is the definition. It usually takes a while before they realize that all of these things have a variety of different but equivalent definitions, and in most cases also have genuinely different definitions. In the case of logic, just looking at the sheer number of entries under "logic" in the Stanford Encyclopedia of Philosophy, many of which correspond to different logics, gives an indication. And it is not comprehensive by any means.

For your example, all the reasoning is equational so which logic we're using is not as critical. We do need the laws for equality which could be roughly described as "a congruence with respect to everything". First, equality is an equivalence relation meaning it is reflexive, $x=x$; symmetric, if $x = y$ then $y = x$; and transitive, if $x = y$ and $y = z$ then $x = z$. Then what makes equality equality is the indiscernibility of indenticals which is usually expressed as a rule rather than an axiom and states: if $x = y$ and $P$ is some predicate with free variable $z$, then if $P[x/z]$ is provable so is $P[y/z]$ where $P[x/z]$ means $P$ with all free occurrences of $z$ replaced with $x$, i.e. substituting $x$ for $z$, and similarly for $P[y/z]$. (Again, there are other ways of presenting these rules and axioms. Indeed, this set is redundant...)

The proof of a statement like $0x=0$ is common in the theory of rings. For example, using the definition of a ring given on Wikipedia, this is a theorem but not an axiom. The aspect I mentioned before strikes here too. There are other choices you could take for the axioms of a ring, including ones where $0x=0$ is taken axiomatically. Also, the term "ring" is ambiguous as many authors consider "rings without unit" (i.e. which don't necessarily have an element that behaves like $1$). The definition Wikipedia gives is a ring with unit. These definitions are not equivalent.

Anyway, using the definition on Wikipedia, one way to prove $0x=0$ is the following: $$\begin{align} &0x-0x=0 \tag{additive inverse} \\ \iff & (0+0)x-0x=0 \tag{additive identity} \\ \iff & (0x+0x)-0x = 0 \tag{left distributivity} \\ \iff & 0x+(0x-0x) = 0 \tag{additive associativity} \\ \iff & 0x + 0 = 0 \tag{additive inverse} \\ \iff & 0x = 0 \tag{additive identity} \end{align}$$

Each $\iff$ is hiding a use of the indiscernibility of identicals. For example, the first step is: let $P$ be $zx-0x=0$, the additive identity axiom for $0$ states $0+0=0$ or, by symmetry, $0=0+0$, if $P[0/z]$ is provable, then $P[(0+0)/z]$ is provable. This gives the $\Rightarrow$ direction, the $\Leftarrow$ direction just uses the same equality the other way.

So why don't we just take $0x=0$ as an axiom. Well, we could. However, doing so wouldn't let us derive the other axioms and given the other axioms we can derive this one. Using a minimal collection of axioms makes it easier to verify if something is a ring (or a ring homomorphism). We would have to explicitly verify $0x=0$ while having it be a theorem means we can derive it once and for all for all rings. Another factor affecting the choice of axioms is also evident in Wikipedia's presentation. We often want to build our definitions in a modular fashion (which often leads to non-minimal lists of axioms). In this case, Wikipedia's definition starts with the axioms of an commutative group. That is, a ring is an commutative group and simultaneously a monoid whose "multiplication" distributes over the group operation. This way of presenting rings allows us to "import" theorems about commutative groups and monoids and apply them to rings. We could, of course, still do this if we had a different presentation of the axioms of a ring, but we'd have to derive the commutative group/monoid structure first, and this structure may not be obvious from the alternate presentation.

If you really want to get a visceral feel for all of this, I recommend getting familiar with a proof assistant like Agda, Coq, LEAN, or several others. I particularly recommend Agda as it puts all the gory details of the proofs right in your face. Most other proof assistants use a tactics-based approach which means you typically write "proof scripts" which are little programs that search for proofs for you. You don't typically see the proofs in those systems. Nevertheless, any of them will make it very apparent what it means to work with a given definition, what is and is not available at any point in time, and why structuring definitions one way versus another may be desirable. They all have pretty steep learning curves though and LEAN and Coq have better introductory material than Agda.