MN0011

signed_matrix_four_full_determinant_functional

Both exact subtraction-free components of every signed four-by-four cofactor determinant are independent of the witnesses.

Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Historical partial components only: this chapter proves arbitrary signed cofactor minors and exact signed determinants through dimension four. T13 is now closed by the separate Alpha-v27 integer-linear-algebra branch: arbitrary determinant data, rank, and integer column spans, without a claim of lattice index or normal forms. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ a00p. ∀ a00n. ∀ a01p. ∀ a01n. ∀ a02p. ∀ a02n. ∀ a03p. ∀ a03n. ∀ a10p. ∀ a10n. ∀ a11p. ∀ a11n. ∀ a12p. ∀ a12n. ∀ a13p. ∀ a13n. ∀ a20p. ∀ a20n. ∀ a21p. ∀ a21n. ∀ a22p. ∀ a22n. ∀ a23p. ∀ a23n. ∀ a30p. ∀ a30n. ∀ a31p. ∀ a31n. ∀ a32p. ∀ a32n. ∀ a33p. ∀ a33n. ∀ p. ∀ n. ∀ q. ∀ m. p = a00p · (a11p · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + a11n · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + (a12p · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + a12n · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p))) + (a13p · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + a13n · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)))) + a00n · (a11p · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + a11n · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + (a12p · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + a12n · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n))) + (a13p · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + a13n · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)))) + (a01p · (a10p · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + a10n · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + (a12p · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p)) + a12n · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n))) + (a13p · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)) + a13n · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)))) + a01n · (a10p · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + a10n · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + (a12p · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n)) + a12n · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p))) + (a13p · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)) + a13n · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n))))) + (a02p · (a10p · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + a10n · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + (a11p · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n)) + a11n · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p))) + (a13p · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)) + a13n · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)))) + a02n · (a10p · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + a10n · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + (a11p · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p)) + a11n · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n))) + (a13p · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)) + a13n · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p))))) + (a03p · (a10p · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + a10n · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + (a11p · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)) + a11n · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n))) + (a12p · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)) + a12n · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)))) + a03n · (a10p · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + a10n · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + (a11p · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)) + a11n · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p))) + (a12p · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)) + a12n · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n))))) ∧ n = a00p · (a11p · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + a11n · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + (a12p · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + a12n · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n))) + (a13p · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + a13n · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)))) + a00n · (a11p · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + a11n · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + (a12p · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + a12n · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p))) + (a13p · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + a13n · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)))) + (a01p · (a10p · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + a10n · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + (a12p · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n)) + a12n · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p))) + (a13p · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)) + a13n · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)))) + a01n · (a10p · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + a10n · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + (a12p · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p)) + a12n · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n))) + (a13p · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)) + a13n · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p))))) + (a02p · (a10p · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + a10n · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + (a11p · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p)) + a11n · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n))) + (a13p · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)) + a13n · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)))) + a02n · (a10p · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + a10n · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + (a11p · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n)) + a11n · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p))) + (a13p · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)) + a13n · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n))))) + (a03p · (a10p · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + a10n · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + (a11p · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)) + a11n · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p))) + (a12p · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)) + a12n · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)))) + a03n · (a10p · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + a10n · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + (a11p · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)) + a11n · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n))) + (a12p · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)) + a12n · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p))))) → q = a00p · (a11p · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + a11n · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + (a12p · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + a12n · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p))) + (a13p · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + a13n · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)))) + a00n · (a11p · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + a11n · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + (a12p · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + a12n · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n))) + (a13p · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + a13n · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)))) + (a01p · (a10p · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + a10n · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + (a12p · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p)) + a12n · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n))) + (a13p · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)) + a13n · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)))) + a01n · (a10p · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + a10n · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + (a12p · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n)) + a12n · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p))) + (a13p · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)) + a13n · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n))))) + (a02p · (a10p · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + a10n · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + (a11p · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n)) + a11n · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p))) + (a13p · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)) + a13n · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)))) + a02n · (a10p · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + a10n · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + (a11p · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p)) + a11n · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n))) + (a13p · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)) + a13n · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p))))) + (a03p · (a10p · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + a10n · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + (a11p · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)) + a11n · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n))) + (a12p · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)) + a12n · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)))) + a03n · (a10p · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + a10n · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + (a11p · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)) + a11n · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p))) + (a12p · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)) + a12n · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n))))) ∧ m = a00p · (a11p · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + a11n · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + (a12p · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + a12n · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n))) + (a13p · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + a13n · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)))) + a00n · (a11p · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + a11n · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + (a12p · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + a12n · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p))) + (a13p · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + a13n · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)))) + (a01p · (a10p · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + a10n · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + (a12p · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n)) + a12n · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p))) + (a13p · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)) + a13n · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)))) + a01n · (a10p · (a22p · a33n + a22n · a33p + (a23p · a32p + a23n · a32n)) + a10n · (a22p · a33p + a22n · a33n + (a23p · a32n + a23n · a32p)) + (a12p · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p)) + a12n · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n))) + (a13p · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)) + a13n · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p))))) + (a02p · (a10p · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + a10n · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + (a11p · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p)) + a11n · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n))) + (a13p · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)) + a13n · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)))) + a02n · (a10p · (a21p · a33p + a21n · a33n + (a23p · a31n + a23n · a31p)) + a10n · (a21p · a33n + a21n · a33p + (a23p · a31p + a23n · a31n)) + (a11p · (a20p · a33n + a20n · a33p + (a23p · a30p + a23n · a30n)) + a11n · (a20p · a33p + a20n · a33n + (a23p · a30n + a23n · a30p))) + (a13p · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)) + a13n · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n))))) + (a03p · (a10p · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + a10n · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + (a11p · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n)) + a11n · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p))) + (a12p · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p)) + a12n · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)))) + a03n · (a10p · (a21p · a32n + a21n · a32p + (a22p · a31p + a22n · a31n)) + a10n · (a21p · a32p + a21n · a32n + (a22p · a31n + a22n · a31p)) + (a11p · (a20p · a32p + a20n · a32n + (a22p · a30n + a22n · a30p)) + a11n · (a20p · a32n + a20n · a32p + (a22p · a30p + a22n · a30n))) + (a12p · (a20p · a31n + a20n · a31p + (a21p · a30p + a21n · a30n)) + a12n · (a20p · a31p + a20n · a31n + (a21p · a30n + a21n · a30p))))) → p = q ∧ n = m

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

none

Actual proof prerequisites

signed_matrix_four_cofactor_expansion_functional
Original expanded first-order statement 
forall a00p a00n a01p a01n a02p a02n a03p a03n a10p a10n a11p a11n a12p a12n a13p a13n a20p a20n a21p a21n a22p a22n a23p a23n a30p a30n a31p a31n a32p a32n a33p a33n p n q m. (p = ((((((((a00p) * (((((((a11p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a11n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a12n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))))) + (((a13p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a13n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))))) + (a00n) * (((((((a11p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a11n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a12n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))))) + (((a13p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a13n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))))))) + (((a01p) * (((((((a10p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a10n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a12n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a13n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))) + (a01n) * (((((((a10p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a10n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a12n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a13n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))))))) + (((a02p) * (((((((a10p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a10n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))) + (((a11p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a11n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a13n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))) + (a02n) * (((((((a10p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a10n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))) + (((a11p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a11n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a13n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))))))) + (((a03p) * (((((((a10p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a10n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))) + (((a11p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a11n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))) + (((a12p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a12n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))) + (a03n) * (((((((a10p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a10n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))) + (((a11p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a11n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))) + (((a12p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a12n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n)))))))))))) /\ n = ((((((((a00p) * (((((((a11p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a11n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a12n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))))) + (((a13p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a13n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))))) + (a00n) * (((((((a11p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a11n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a12n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))))) + (((a13p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a13n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))))))) + (((a01p) * (((((((a10p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a10n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a12n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a13n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))) + (a01n) * (((((((a10p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a10n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a12n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a13n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))))))) + (((a02p) * (((((((a10p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a10n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))) + (((a11p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a11n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a13n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))) + (a02n) * (((((((a10p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a10n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))) + (((a11p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a11n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a13n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))))))) + (((a03p) * (((((((a10p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a10n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))) + (((a11p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a11n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))) + (((a12p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a12n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))) + (a03n) * (((((((a10p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a10n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))) + (((a11p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a11n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))) + (((a12p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a12n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))))))) -> (q = ((((((((a00p) * (((((((a11p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a11n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a12n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))))) + (((a13p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a13n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))))) + (a00n) * (((((((a11p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a11n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a12n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))))) + (((a13p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a13n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))))))) + (((a01p) * (((((((a10p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a10n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a12n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a13n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))) + (a01n) * (((((((a10p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a10n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a12n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a13n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))))))) + (((a02p) * (((((((a10p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a10n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))) + (((a11p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a11n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a13n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))) + (a02n) * (((((((a10p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a10n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))) + (((a11p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a11n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a13n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))))))) + (((a03p) * (((((((a10p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a10n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))) + (((a11p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a11n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))) + (((a12p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a12n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))) + (a03n) * (((((((a10p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a10n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))) + (((a11p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a11n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))) + (((a12p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a12n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n)))))))))))) /\ m = ((((((((a00p) * (((((((a11p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a11n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a12n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))))) + (((a13p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a13n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))))) + (a00n) * (((((((a11p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a11n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a12n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))))) + (((a13p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a13n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))))))) + (((a01p) * (((((((a10p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a10n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a12n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a13n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))) + (a01n) * (((((((a10p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a10n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a12n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a13n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))))))) + (((a02p) * (((((((a10p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a10n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))) + (((a11p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a11n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a13n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))) + (a02n) * (((((((a10p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a10n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))) + (((a11p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a11n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a13n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))))))) + (((a03p) * (((((((a10p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a10n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))) + (((a11p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a11n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))) + (((a12p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a12n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))) + (a03n) * (((((((a10p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a10n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))) + (((a11p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a11n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))) + (((a12p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a12n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))))))) -> (p = q /\ n = m)

Complete unchanged native tactic proof

All 61 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

61 script commands · 7 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
signed matrix four cofactor expansion functional
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a00p
  2. L2
    intro a00n
  3. L3
    intro a01p
  4. L4
    intro a01n
  5. L5
    intro a02p
  6. L6
    intro a02n
  7. L7
    intro a03p
  8. L8
    intro a03n
  9. L9
    intro a10p
  10. L10
    intro a10n
02Fix variables and assumptionsL11–20

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro a11p
  2. L12
    intro a11n
  3. L13
    intro a12p
  4. L14
    intro a12n
  5. L15
    intro a13p
  6. L16
    intro a13n
  7. L17
    intro a20p
  8. L18
    intro a20n
  9. L19
    intro a21p
  10. L20
    intro a21n
03Fix variables and assumptionsL21–30

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro a22p
  2. L22
    intro a22n
  3. L23
    intro a23p
  4. L24
    intro a23n
  5. L25
    intro a30p
  6. L26
    intro a30n
  7. L27
    intro a31p
  8. L28
    intro a31n
  9. L29
    intro a32p
  10. L30
    intro a32n
04Fix variables and assumptionsL31–38

Work with arbitrary variables or the premises of the current implication.

  1. L31
    intro a33p
  2. L32
    intro a33n
  3. L33
    intro p
  4. L34
    intro n
  5. L35
    intro q
  6. L36
    intro m
  7. L37
    intro hfirst
  8. L38
    intro hsecond
05Use earlier factsL39–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L39
    specialize signed_matrix_four_cofactor_expansion_functional a00p
  2. L40
    specialize signed_matrix_four_cofactor_expansion_functional a00n
  3. L41
    specialize signed_matrix_four_cofactor_expansion_functional a01p
  4. L42
    specialize signed_matrix_four_cofactor_expansion_functional a01n
  5. L43
    specialize signed_matrix_four_cofactor_expansion_functional a02p
  6. L44
    specialize signed_matrix_four_cofactor_expansion_functional a02n
  7. L45
    specialize signed_matrix_four_cofactor_expansion_functional a03p
  8. L46
    specialize signed_matrix_four_cofactor_expansion_functional a03n
  9. L47
    specialize signed_matrix_four_cofactor_expansion_functional ((((((a11p) * (((((a22p) * (a33p) + (a22n) * (a33n) · expand full local formula (633 characters)specialize signed_matrix_four_cofactor_expansion_functional ((((((a11p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a11n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a12n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))))) + (((a13p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a13n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))))
  10. L48
    specialize signed_matrix_four_cofactor_expansion_functional ((((((a11p) * (((((a22p) * (a33n) + (a22n) * (a33p) · expand full local formula (633 characters)specialize signed_matrix_four_cofactor_expansion_functional ((((((a11p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a11n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a12n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))))) + (((a13p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a13n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))))
06Use earlier factsL49–58

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L49
    specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a22p) * (a33p) + (a22n) * (a33n) · expand full local formula (633 characters)specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a10n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a12n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a13n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))
  2. L50
    specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a22p) * (a33n) + (a22n) * (a33p) · expand full local formula (633 characters)specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a10n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a12n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a13n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))
  3. L51
    specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a33p) + (a21n) * (a33n) · expand full local formula (633 characters)specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a10n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))) + (((a11p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a11n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a13n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))
  4. L52
    specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a33n) + (a21n) * (a33p) · expand full local formula (633 characters)specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a10n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))) + (((a11p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a11n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a13n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))
  5. L53
    specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a32p) + (a21n) * (a32n) · expand full local formula (633 characters)specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a10n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))) + (((a11p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a11n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))) + (((a12p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a12n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))
  6. L54
    specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a32n) + (a21n) * (a32p) · expand full local formula (633 characters)specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a10n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))) + (((a11p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a11n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))) + (((a12p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a12n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))
  7. L55
    specialize signed_matrix_four_cofactor_expansion_functional p
  8. L56
    specialize signed_matrix_four_cofactor_expansion_functional n
  9. L57
    specialize signed_matrix_four_cofactor_expansion_functional q
  10. L58
    specialize signed_matrix_four_cofactor_expansion_functional m
07Use earlier factsL59–61

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L59
    apply signed_matrix_four_cofactor_expansion_functional
  2. L60
    exact hfirst
  3. L61
    exact hsecond

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro a00p
  2. 0002intro a00n
  3. 0003intro a01p
  4. 0004intro a01n
  5. 0005intro a02p
  6. 0006intro a02n
  7. 0007intro a03p
  8. 0008intro a03n
  9. 0009intro a10p
  10. 0010intro a10n
  11. 0011intro a11p
  12. 0012intro a11n
  13. 0013intro a12p
  14. 0014intro a12n
  15. 0015intro a13p
  16. 0016intro a13n
  17. 0017intro a20p
  18. 0018intro a20n
  19. 0019intro a21p
  20. 0020intro a21n
  21. 0021intro a22p
  22. 0022intro a22n
  23. 0023intro a23p
  24. 0024intro a23n
  25. 0025intro a30p
  26. 0026intro a30n
  27. 0027intro a31p
  28. 0028intro a31n
  29. 0029intro a32p
  30. 0030intro a32n
  31. 0031intro a33p
  32. 0032intro a33n
  33. 0033intro p
  34. 0034intro n
  35. 0035intro q
  36. 0036intro m
  37. 0037intro hfirst
  38. 0038intro hsecond
  39. 0039specialize signed_matrix_four_cofactor_expansion_functional a00p
  40. 0040specialize signed_matrix_four_cofactor_expansion_functional a00n
  41. 0041specialize signed_matrix_four_cofactor_expansion_functional a01p
  42. 0042specialize signed_matrix_four_cofactor_expansion_functional a01n
  43. 0043specialize signed_matrix_four_cofactor_expansion_functional a02p
  44. 0044specialize signed_matrix_four_cofactor_expansion_functional a02n
  45. 0045specialize signed_matrix_four_cofactor_expansion_functional a03p
  46. 0046specialize signed_matrix_four_cofactor_expansion_functional a03n
  47. 0047specialize signed_matrix_four_cofactor_expansion_functional ((((((a11p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a11n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a12n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))))) + (((a13p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a13n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))))
  48. 0048specialize signed_matrix_four_cofactor_expansion_functional ((((((a11p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a11n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a12n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))))) + (((a13p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a13n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))))
  49. 0049specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))) + (a10n) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))))) + (((a12p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a12n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a13n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))
  50. 0050specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a22p) * (a33n) + (a22n) * (a33p))) + (((a23p) * (a32p) + (a23n) * (a32n))))) + (a10n) * (((((a22p) * (a33p) + (a22n) * (a33n))) + (((a23p) * (a32n) + (a23n) * (a32p))))))) + (((a12p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a12n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a13n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))
  51. 0051specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))) + (a10n) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))))) + (((a11p) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))) + (a11n) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))))))) + (((a13p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a13n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))
  52. 0052specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a33n) + (a21n) * (a33p))) + (((a23p) * (a31p) + (a23n) * (a31n))))) + (a10n) * (((((a21p) * (a33p) + (a21n) * (a33n))) + (((a23p) * (a31n) + (a23n) * (a31p))))))) + (((a11p) * (((((a20p) * (a33p) + (a20n) * (a33n))) + (((a23p) * (a30n) + (a23n) * (a30p))))) + (a11n) * (((((a20p) * (a33n) + (a20n) * (a33p))) + (((a23p) * (a30p) + (a23n) * (a30n))))))))) + (((a13p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a13n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))
  53. 0053specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))) + (a10n) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))))) + (((a11p) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))) + (a11n) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))))))) + (((a12p) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))) + (a12n) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))))))
  54. 0054specialize signed_matrix_four_cofactor_expansion_functional ((((((a10p) * (((((a21p) * (a32n) + (a21n) * (a32p))) + (((a22p) * (a31p) + (a22n) * (a31n))))) + (a10n) * (((((a21p) * (a32p) + (a21n) * (a32n))) + (((a22p) * (a31n) + (a22n) * (a31p))))))) + (((a11p) * (((((a20p) * (a32p) + (a20n) * (a32n))) + (((a22p) * (a30n) + (a22n) * (a30p))))) + (a11n) * (((((a20p) * (a32n) + (a20n) * (a32p))) + (((a22p) * (a30p) + (a22n) * (a30n))))))))) + (((a12p) * (((((a20p) * (a31n) + (a20n) * (a31p))) + (((a21p) * (a30p) + (a21n) * (a30n))))) + (a12n) * (((((a20p) * (a31p) + (a20n) * (a31n))) + (((a21p) * (a30n) + (a21n) * (a30p))))))))
  55. 0055specialize signed_matrix_four_cofactor_expansion_functional p
  56. 0056specialize signed_matrix_four_cofactor_expansion_functional n
  57. 0057specialize signed_matrix_four_cofactor_expansion_functional q
  58. 0058specialize signed_matrix_four_cofactor_expansion_functional m
  59. 0059apply signed_matrix_four_cofactor_expansion_functional
  60. 0060exact hfirst
  61. 0061exact hsecond