I wonder if Applicative is derived naturally through MonadTransformer's Monad

Question

For the type constraint's point of view, Monad be derived from Applicative, which is the reverse of what I wrote in the title. However, it's not a mistake. While studying Monad, I have checked all the relationships below to see if they are satisfied. Specifically, I always checked if the Applicative (and Functor) be derived naturally from Monad.

// 0. Monad -> Monad
join mma = mma >>= id

ma >> mb = ma >>= const mb

// 1. Moand -> Applicative
mf <*> ma = do
            x <- mf
            y <- ma
            return (x y)

pure = return

// 2. Monad -> Functor

fmap f ma = ma >>= return . f

// 3. Applicative -> Applicative
fa *> fb = pure (const id) <*> fa <*> fb

// 4. Applicative -> Functor
f <$> fa = pure f <*> fa

// 5. Applicative -> Monoid (for Monoid a)
mempty = pure mempty
fa <> fa' = (<>) <$> fa <*> fa'

// 6. Foldable -> Foldable
foldr f z ta = (foldMap f ta) z  // f :: a -> (b -> b). We consider (b -> b) as Endo monoid
foldMap f ta = foldr (\x y -> f x <> y) mempty ta

// 7. Traversable -> Functor
fmap f ta = runIdentity $ traverse (Identity . f) ta

// 8. Traversable -> Foldable
foldMap f ta = getConstant $ traverse (Constant . f) ta

It's cool. I checked all of the Monads so that all of the instances (Monad, Functor, Applicative, Monoid, Foldable, Traversable) have the same context.

All of the instances makes harmony, following above 0 ~ 9 laws. Maybe, Either, List, Reader, Writer, State, Constant, Products of arbitrary number of types with duplicated types etc...

Now, I finally entered the Monad Transformers chapter in the book I'm reading now.

And I'm in trouble.

I can't check if Applicative instance of MaybeT aligns with Monad instance of MaybeT.

Actually, I faild for all of the MonadTransformers, except for IdentityT.

MaybeT mMf :: MaybeT m (a -> b)
MaybeT mMa :: MaybeT m a
mMf :: m (Maybe (a -> b))
mMa :: m (Maybe a)


MaybeT $ (<*>) <$> (MaybeT mMf) <*> mMa == do
                                           x <- mMf
                                           y <- mMa
                                           return (x y)  // is this true???

//given
MaybeT mMx :: MaybeT m x
mMx :: m (Maybe x)

f :: x -> MaybeT m y

MaybeT mMx >>= f =
  MaybeT $ do
    Mx <- mMx
    case Mx of
      Nothing -> return Nothing
      Just x -> runMaybeT (f x)


return = pure

pure = MaybeT . pure . pure

Can I get some help to get assure that Applicative of MaybeT is in a same context with Monad of MaybeT?