A zero fine coordinate kills a selected coarse-address word

import Definitions.Def_mme_dwz_step1_projector_basis_api
import Definitions.Def_mme_dwz_cw_square_fine_split_grading

open MME Module PiTensorProduct
open MME.DWZStep1Support
open MME.DWZSourceAligned

universe u

set_option autoImplicit false

theorem mme_dwz_coarseAddress_selected_mode_words_postmap_eq_zero_of_coordinate
    {K : Type u} [Field K] {N : ℕ}
    (outer : Fin N → Fin 15)
    (word : ∀ i : Fin 3, AddressModeWord outer i)
    {W : Fin 3 → Type u}
    [∀ i, AddCommGroup (W i)] [∀ i, Module K (W i)]
    (post : ∀ i, (coarseAddressObj K outer).V i →ₗ[K] W i)
    (r : Fin N)
    (hzero : (cwSquareFineSplitGrading K 6).blockTensor
      (fun i ↦ fineSplitGrade
        (word i r).leftGrade (word i r).rightGrade) = 0) :
    PiTensorProduct.map
        (fun i ↦ (post i).comp
          (DWZComponentRestriction.basisLabelProjection
            (coarseAddressModeBasis K outer i) id {word i}))
        (coarseAddressObj K outer).t = 0 := by
  sorry