Algebraic proof methods for identities of matrices and operators: improvements of Hartwig's triple reverse order law

TL;DR

This paper enhances algebraic proof methods for matrix and operator identities, specifically improving Hartwig's triple reverse order law using a new framework and software, enabling more general and simplified proofs in rings with involution.

Contribution

It introduces a novel algebraic proof framework and software application that generalizes and simplifies the proof of Hartwig's triple reverse order law.

Findings

Improved proof of Hartwig's triple reverse order law

Framework applicable to rings with involution

Computer-assisted proofs extend results to broader settings

Abstract

When improving results about generalized inverses, the aim often is to do this in the most general setting possible by eliminating superfluous assumptions and by simplifying some of the conditions in statements. In this paper, we use Hartwig's well-known triple reverse order law as an example for showing how this can be done using a recent framework for algebraic proofs and the software package OperatorGB. Our improvements of Hartwig's result are proven in rings with involution and we discuss computer-assisted proofs that show these results in other settings based on the framework and a single computation with noncommutative polynomials.