metamath/valid/algebra-2rootspoly-apatapbeq2asqp2ab.mm

${
  algebra-2rootspoly-apatapbeq2asqp2ab.0 $e |- ( ph -> A e. CC ) $.
  algebra-2rootspoly-apatapbeq2asqp2ab.1 $e |- ( ph -> B e. CC ) $.
  $( (Contributed by Stanislas Polu, 8-Oct-2020.) $)
  algebra-2rootspoly-apatapbeq2asqp2ab $p |- ( ph -> ( ( A + A ) x. ( A + B ) ) 
= ( ( 2 x. ( A ^ 2 ) ) + ( 2 x. ( A x. B ) ) ) ) $=
( c2 cexp cmul caddc adddid sqvald eqcomd eqidd oveq12d eqtrd oveq2d addcld co 
mulcld eqtr3d 2timesd adddird 2cnd sqcld ) AFBFGRZBCHRZIRZHRZBBIRBCIRZHR 
ZFUEHRFUFHRIRAFBUIHRZHRZUHUJAUKUGFHAUKBBHRZUFIRUGABBCDDEJAUMUEUFUFIAUEUMABD 
KLAUFMNOPAULUKUKIRZUJAUKABUIDABCDEQZSUAAUJUNABBUIDDUOUBLOTAFUEUFAUCABDUDABC 
DESJT $. 
$}