quaternion_coordinate_square_transport

Statement with defined notation

forall a b c d e f g h m0 m1 m2 m3. ((((a * e) = (b * f + c * g + d * h) + m0) \/ ((b * f + c * g + d * h) = (a * e) + m0)) /\ ((((a * f + b * e + c * h) = (d * g) + m1) \/ ((d * g) = (a * f + b * e + c * h) + m1)) /\ ((((a * g + c * e + d * f) = (b * h) + m2) \/ ((b * h) = (a * g + c * e + d * f) + m2)) /\ (((a * h + b * g + d * e) = (c * f) + m3) \/ ((c * f) = (a * h + b * g + d * e) + m3))))) -> (((a * e) * (a * e) + (b * f + c * g + d * h) * (b * f + c * g + d * h) = m0 * m0 + ((a * e) * (b * f + c * g + d * h) + (b * f + c * g + d * h) * (a * e))) /\ (((a * f + b * e + c * h) * (a * f + b * e + c * h) + (d * g) * (d * g) = m1 * m1 + ((a * f + b * e + c * h) * (d * g) + (d * g) * (a * f + b * e + c * h))) /\ (((a * g + c * e + d * f) * (a * g + c * e + d * f) + (b * h) * (b * h) = m2 * m2 + ((a * g + c * e + d * f) * (b * h) + (b * h) * (a * g + c * e + d * f))) /\ ((a * h + b * g + d * e) * (a * h + b * g + d * e) + (c * f) * (c * f) = m3 * m3 + ((a * h + b * g + d * e) * (c * f) + (c * f) * (a * h + b * g + d * e))))))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

In local proof propositions

Proof neighborhood

Direct theorem prerequisites

Direct theorem dependents

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.