English
If Z(P) ≠ 0, then the vector dblXYZ(P) factors as dblZ(P) times the affine 3-vector with first two components given by addX and addY evaluated at the scaled coordinates and the last entry 1.
Русский
Если Z(P) ≠ 0, то dblXYZ(P) раскладывается как dblZ(P) умноженное на аффинный трёхмерный вектор с первыми двумя компонентами, заданными addX и addY, и последней компонентой 1.
LaTeX
$$$W'.dblXYZ(P) = W'.dblZ(P) \cdot \Big( W.toAffine.addX\big( \tfrac{P_x}{P_z}, \tfrac{Q_x}{Q_z} \big),\ W.toAffine.addY\big( \tfrac{P_x}{P_z}, \tfrac{Q_x}{Q_z}, \tfrac{P_y}{P_z}\big) ,\;1\Big)$$$
Lean4
theorem dblXYZ_of_Z_ne_zero [DecidableEq F] {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
(hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ W.negY Q * P z) :
W.dblXYZ P =
W.dblZ P •
![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
(W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
1] :=
by
have hZ : IsUnit <| W.dblZ P := isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx hy
erw [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, ←
dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]
