Has the concept of using a hand checked simple theorem prover to validate more complex theorem provers been explored before?
Not that I know of.  A more typical architecture is to decompose the theorem prover into a prover plus a proof checker.  Then only the proof checker needs to be validated.  If proofs are expressed in a simple enough language, then the proof checker might be extremely simple.  All of the smarts can go into the prover (which tries various strategies to try to find a valid proof), but it doesn't need to be validated, since its output will always be checked by the proof checker.