let R be Field; :: thesis: for S being Subset of R st S * S c= S & SQ R c= S holds
( S /\ (- S) = {(0. R)} iff not - (1. R) in S )
let S be Subset of R; :: thesis: ( S * S c= S & SQ R c= S implies ( S /\ (- S) = {(0. R)} iff not - (1. R) in S ) )
assume AS: ( S * S c= S & SQ R c= S ) ; :: thesis: ( S /\ (- S) = {(0. R)} iff not - (1. R) in S )
A0: 1. R in SQ R ;
X: now :: thesis: ( S /\ (- S) = {(0. R)} implies not - (1. R) in S )
assume A: S /\ (- S) = {(0. R)} ; :: thesis: not - (1. R) in S
now :: thesis: not - (1. R) in S
assume - (1. R) in S ; :: thesis: contradiction
then - (- (1. R)) in - S ;
then 1. R in S /\ (- S) by XBOOLE_0:def 4, A0, AS;
hence contradiction by A, TARSKI:def 1; :: thesis: verum
end;
hence not - (1. R) in S ; :: thesis: verum
end;
now :: thesis: ( not - (1. R) in S implies S /\ (- S) = {(0. R)} )
assume A: not - (1. R) in S ; :: thesis: S /\ (- S) = {(0. R)}
now :: thesis: not S /\ (- S) <> {(0. R)}
assume A2: S /\ (- S) <> {(0. R)} ; :: thesis: contradiction
B0: 0. R in SQ R ;
then - (0. R) in - S by AS;
then 0. R in S /\ (- S) by AS, B0, XBOOLE_0:def 4;
then A3: {(0. R)} c= S /\ (- S) by TARSKI:def 1;
now :: thesis: ex a being Element of R st
( a <> 0. R & a in S /\ (- S) )
assume A4: for a being Element of R holds
( not a <> 0. R or not a in S /\ (- S) ) ; :: thesis: contradiction
now :: thesis: for o being object st o in S /\ (- S) holds
o in {(0. R)}
let o be object ; :: thesis: ( o in S /\ (- S) implies o in {(0. R)} )
assume o in S /\ (- S) ; :: thesis: o in {(0. R)}
then o = 0. R by A4;
hence o in {(0. R)} by TARSKI:def 1; :: thesis: verum
end;
hence contradiction by A2, A3, TARSKI:2; :: thesis: verum
end;
then consider a being Element of R such that
A5: ( a <> 0. R & a in S /\ (- S) ) ;
A9: ( a in S & a in - S ) by A5, XBOOLE_0:def 4;
then A6: - a in - (- S) ;
A7: now :: thesis: not - a = 0. R
assume - a = 0. R ; :: thesis: contradiction
then - (- a) = 0. R ;
hence contradiction by A5; :: thesis: verum
end;
((- a) ") ^2 is square ;
then ((- a) ") ^2 in SQ R ;
then A8: (((- a) ") ^2) * (- a) in S * S by AS, A6;
(- a) " in S
proof
(((- a) ") ^2) * (- a) = ((- a) ") * (((- a) ") * (- a)) by GROUP_1:def 3
.= ((- a) ") * (1. R) by A7, VECTSP_1:def 10
.= (- a) " ;
hence (- a) " in S by A8, AS; :: thesis: verum
end;
then A8: a * ((- a) ") in S * S by A9;
(- (a ")) * (- a) = a * (a ") by VECTSP_1:10
.= 1. R by A5, VECTSP_1:def 10 ;
then a * ((- a) ") = a * (- (a ")) by A7, VECTSP_1:def 10
.= - (a * (a ")) by VECTSP_1:8
.= - (1. R) by A5, VECTSP_1:def 10 ;
hence contradiction by A8, A, AS; :: thesis: verum
end;
hence S /\ (- S) = {(0. R)} ; :: thesis: verum
end;
hence ( S /\ (- S) = {(0. R)} iff not - (1. R) in S ) by X; :: thesis: verum