${
  algebra-manipexpr-apbeq2cceqiacpbceqm2.0 $e |- ( ph -> A e. CC ) $.
  algebra-manipexpr-apbeq2cceqiacpbceqm2.1 $e |- ( ph -> B e. CC ) $.
  algebra-manipexpr-apbeq2cceqiacpbceqm2.2 $e |- ( ph -> ( A + B ) = ( 2 x. C ) 
) $.
  algebra-manipexpr-apbeq2cceqiacpbceqm2.3 $e |- ( ph -> C e. CC ) $.
  algebra-manipexpr-apbeq2cceqiacpbceqm2.4 $e |- ( ph -> C = _i ) $.
  $( (Contributed by Stanislas Polu, 14-Sep-2020.) $)
  algebra-manipexpr-apbeq2cceqiacpbceqm2 $p |- ( ph -> ( ( A x. C ) + ( B x. C 
) ) = -u 2 ) $=
( caddc co cmul c2 cneg adddird ci oveq12d 2cnd a1i 2cn wcel ax-icn mulassd cc 
oveq1d oveq2d ixi oveq2i wceq neg1cn mulm1i mulcomli syl5eq eqtrd 3eqtrd c1 
eqtr3d ) ABCJKZDLKZBDLKCDLKJKMNZABCDEFHOAUSMDLKZPLKMDPLKZLKZUTAURVADPLGI 
QAMDPARHPUDUAAUBSUCAVCMPPLKZLKZUTAVBVDMLADPPLIUEUFAVEMUPNZLKZUTVDVFMLUGUHVG 
UTUIAVFMUTUJTMTUKULSUMUNUOUQ $. 
$}