∀ {R : Type u_3} {B : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  (fg :
    { fg //
      (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
        (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }),
  (∀ (x y : A),
      ((↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1,
                MulOpposite.op (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).2 • (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1.toLinearMap).2
            x *
          ((↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1,
                MulOpposite.op (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).2 • (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1.toLinearMap).2
            y =
        0) ∧
    (∀ (r x : A),
        ((↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1,
                MulOpposite.op (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).2 • (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1.toLinearMap).2
            (r • x) =
          ((↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1,
                  MulOpposite.op (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).2 • (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1.toLinearMap).1
              r *
            ((↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1,
                  MulOpposite.op (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).2 • (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1.toLinearMap).2
              x) ∧
      ∀ (r x : A),
        ((↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1,
                MulOpposite.op (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).2 • (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1.toLinearMap).2
            (MulOpposite.op r • x) =
          ((↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1,
                  MulOpposite.op (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).2 • (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1.toLinearMap).2
              x *
            ((↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1,
                  MulOpposite.op (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).2 • (↑⟨((↑fg).1, (↑fg).2 1), ⋯⟩).1.toLinearMap).1
              r