let R be domRing; :: thesis: for a, b being Element of R holds
( a ^2 = b ^2 iff ( a = b or a = - b ) )
let a, b be Element of R; :: thesis: ( a ^2 = b ^2 iff ( a = b or a = - b ) )
hereby :: thesis: ( ( a = b or a = - b ) implies a ^2 = b ^2 )
assume a ^2 = b ^2 ; :: thesis: ( a = b or a = - b )
then 0. R = (a ^2) - (b ^2) by RLVECT_1:15
.= (a + b) * (a - b) by P4a ;
per cases then ( a + b = 0. R or a - b = 0. R ) by VECTSP_2:def 1;
suppose a + b = 0. R ; :: thesis: ( a = b or a = - b )
hence ( a = b or a = - b ) by RLVECT_1:6; :: thesis: verum
end;
suppose a - b = 0. R ; :: thesis: ( a = b or a = - b )
hence ( a = b or a = - b ) by RLVECT_1:21; :: thesis: verum
end;
end;
end;
assume ( a = b or a = - b ) ; :: thesis: a ^2 = b ^2
per cases then ( a = b or a = - b ) ;
suppose a = b ; :: thesis: a ^2 = b ^2
hence a ^2 = b ^2 ; :: thesis: verum
end;
suppose a = - b ; :: thesis: a ^2 = b ^2
hence a ^2 = b ^2 by VECTSP_1:10; :: thesis: verum
end;
end;