:: SYMSP_1 semantic presentation
begin
definition
let F be Field;
attrc2 is strict ;
struct SymStr over F -> RelStr , VectSpStr over F;
aggrSymStr(# carrier, addF, ZeroF, lmult, InternalRel #) -> SymStr over F;
end;
registration
let F be Field;
cluster non empty for SymStr over F;
existence
not for b1 being SymStr over F holds b1 is empty
proof
set X = the non empty set ;
set a = the BinOp of the non empty set ;
set Z = the Element of the non empty set ;
set l = the Function of [: the carrier of F, the non empty set :], the non empty set ;
set r = the Relation of the non empty set ;
take SymStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set , the Relation of the non empty set #) ; ::_thesis: not SymStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set , the Relation of the non empty set #) is empty
thus not the carrier of SymStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set , the Relation of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
notation
let F be Field;
let S be SymStr over F;
let a, b be Element of S;
synonym a _|_ b for S <= a;
end;
set X = {0};
reconsider o = 0 as Element of {0} by TARSKI:def_1;
deffunc H1( Element of {0}, Element of {0}) -> Element of {0} = o;
consider md being BinOp of {0} such that
Lm1: for x, y being Element of {0} holds md . (x,y) = H1(x,y) from BINOP_1:sch_4();
Lm2: now__::_thesis:_for_F_being_Field_ex_mo_being_Relation_of_{0}_st_
for_x_being_set_holds_
(_x_in_mo_iff_(_x_in_[:{0},{0}:]_&_ex_a,_b_being_Element_of_{0}_st_
(_x_=_[a,b]_&_b_=_o_)_)_)
defpred S1[ set ] means ex a, b being Element of {0} st
( $1 = [a,b] & b = o );
set CV = [:{0},{0}:];
let F be Field; ::_thesis: ex mo being Relation of {0} st
for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) )
consider mo being set such that
A1: for x being set holds
( x in mo iff ( x in [:{0},{0}:] & S1[x] ) ) from XBOOLE_0:sch_1();
mo c= [:{0},{0}:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in mo or x in [:{0},{0}:] )
thus ( not x in mo or x in [:{0},{0}:] ) by A1; ::_thesis: verum
end;
then reconsider mo = mo as Relation of {0} ;
take mo = mo; ::_thesis: for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) )
thus for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) ) by A1; ::_thesis: verum
end;
registration
let F be Field;
let X be non empty set ;
let md be BinOp of X;
let o be Element of X;
let mF be Function of [: the carrier of F,X:],X;
let mo be Relation of X;
cluster SymStr(# X,md,o,mF,mo #) -> non empty ;
coherence
not SymStr(# X,md,o,mF,mo #) is empty ;
end;
Lm3: for F being Field
for mF being Function of [: the carrier of F,{0}:],{0}
for mo being Relation of {0} holds
( SymStr(# {0},md,o,mF,mo #) is Abelian & SymStr(# {0},md,o,mF,mo #) is add-associative & SymStr(# {0},md,o,mF,mo #) is right_zeroed & SymStr(# {0},md,o,mF,mo #) is right_complementable )
proof
let F be Field; ::_thesis: for mF being Function of [: the carrier of F,{0}:],{0}
for mo being Relation of {0} holds
( SymStr(# {0},md,o,mF,mo #) is Abelian & SymStr(# {0},md,o,mF,mo #) is add-associative & SymStr(# {0},md,o,mF,mo #) is right_zeroed & SymStr(# {0},md,o,mF,mo #) is right_complementable )
let mF be Function of [: the carrier of F,{0}:],{0}; ::_thesis: for mo being Relation of {0} holds
( SymStr(# {0},md,o,mF,mo #) is Abelian & SymStr(# {0},md,o,mF,mo #) is add-associative & SymStr(# {0},md,o,mF,mo #) is right_zeroed & SymStr(# {0},md,o,mF,mo #) is right_complementable )
let mo be Relation of {0}; ::_thesis: ( SymStr(# {0},md,o,mF,mo #) is Abelian & SymStr(# {0},md,o,mF,mo #) is add-associative & SymStr(# {0},md,o,mF,mo #) is right_zeroed & SymStr(# {0},md,o,mF,mo #) is right_complementable )
set H = SymStr(# {0},md,o,mF,mo #);
thus SymStr(# {0},md,o,mF,mo #) is Abelian ::_thesis: ( SymStr(# {0},md,o,mF,mo #) is add-associative & SymStr(# {0},md,o,mF,mo #) is right_zeroed & SymStr(# {0},md,o,mF,mo #) is right_complementable )
proof
let x, y be Element of SymStr(# {0},md,o,mF,mo #); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider x = x, y = y as Element of {0} ;
md . (x,y) = o by Lm1;
hence x + y = y + x by Lm1; ::_thesis: verum
end;
thus SymStr(# {0},md,o,mF,mo #) is add-associative ::_thesis: ( SymStr(# {0},md,o,mF,mo #) is right_zeroed & SymStr(# {0},md,o,mF,mo #) is right_complementable )
proof
let x, y, z be Element of SymStr(# {0},md,o,mF,mo #); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider x = x, y = y, z = z as Element of {0} ;
md . (x,(md . (y,z))) = o by Lm1;
hence (x + y) + z = x + (y + z) by Lm1; ::_thesis: verum
end;
thus SymStr(# {0},md,o,mF,mo #) is right_zeroed ::_thesis: SymStr(# {0},md,o,mF,mo #) is right_complementable
proof
let x be Element of SymStr(# {0},md,o,mF,mo #); :: according to RLVECT_1:def_4 ::_thesis: x + (0. SymStr(# {0},md,o,mF,mo #)) = x
reconsider x = x as Element of {0} ;
md . (x,(0. SymStr(# {0},md,o,mF,mo #))) = o by Lm1;
hence x + (0. SymStr(# {0},md,o,mF,mo #)) = x by TARSKI:def_1; ::_thesis: verum
end;
let x be Element of SymStr(# {0},md,o,mF,mo #); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
take - x ; :: according to ALGSTR_0:def_11 ::_thesis: x + (- x) = 0. SymStr(# {0},md,o,mF,mo #)
thus x + (- x) = 0. SymStr(# {0},md,o,mF,mo #) by Lm1; ::_thesis: verum
end;
registration
let F be Field;
cluster non empty right_complementable Abelian add-associative right_zeroed for SymStr over F;
existence
ex b1 being non empty SymStr over F st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable )
proof
set mo = the Relation of {0};
set mF = the Function of [: the carrier of F,{0}:],{0};
( SymStr(# {0},md,o, the Function of [: the carrier of F,{0}:],{0}, the Relation of {0} #) is Abelian & SymStr(# {0},md,o, the Function of [: the carrier of F,{0}:],{0}, the Relation of {0} #) is add-associative & SymStr(# {0},md,o, the Function of [: the carrier of F,{0}:],{0}, the Relation of {0} #) is right_zeroed & SymStr(# {0},md,o, the Function of [: the carrier of F,{0}:],{0}, the Relation of {0} #) is right_complementable ) by Lm3;
hence ex b1 being non empty SymStr over F st
( b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable ) ; ::_thesis: verum
end;
end;
Lm4: now__::_thesis:_for_F_being_Field
for_mF_being_Function_of_[:_the_carrier_of_F,{0}:],{0}_st_(_for_a_being_Element_of_F
for_x_being_Element_of_{0}_holds_mF_._(a,x)_=_o_)_holds_
for_mo_being_Relation_of_{0}
for_MPS_being_non_empty_right_complementable_Abelian_add-associative_right_zeroed_SymStr_over_F_st_MPS_=_SymStr(#_{0},md,o,mF,mo_#)_holds_
(_MPS_is_vector-distributive_&_MPS_is_scalar-distributive_&_MPS_is_scalar-associative_&_MPS_is_scalar-unital_)
let F be Field; ::_thesis: for mF being Function of [: the carrier of F,{0}:],{0} st ( for a being Element of F
for x being Element of {0} holds mF . (a,x) = o ) holds
for mo being Relation of {0}
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# {0},md,o,mF,mo #) holds
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
let mF be Function of [: the carrier of F,{0}:],{0}; ::_thesis: ( ( for a being Element of F
for x being Element of {0} holds mF . (a,x) = o ) implies for mo being Relation of {0}
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# {0},md,o,mF,mo #) holds
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) )
assume A1: for a being Element of F
for x being Element of {0} holds mF . (a,x) = o ; ::_thesis: for mo being Relation of {0}
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# {0},md,o,mF,mo #) holds
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
let mo be Relation of {0}; ::_thesis: for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# {0},md,o,mF,mo #) holds
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
let MPS be non empty right_complementable Abelian add-associative right_zeroed SymStr over F; ::_thesis: ( MPS = SymStr(# {0},md,o,mF,mo #) implies ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) )
assume A2: MPS = SymStr(# {0},md,o,mF,mo #) ; ::_thesis: ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
for x, y being Element of F
for v, w being Element of MPS holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ F) * v = v )
proof
let x, y be Element of F; ::_thesis: for v, w being Element of MPS holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ F) * v = v )
let v, w be Element of MPS; ::_thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ F) * v = v )
A3: (x * y) * v = x * (y * v)
proof
set z = x * y;
A4: (x * y) * v = mF . ((x * y),v) by A2, VECTSP_1:def_12;
reconsider v = v as Element of MPS ;
reconsider v = v as Element of MPS ;
A5: (x * y) * v = o by A1, A2, A4;
reconsider v = v as Element of MPS ;
A6: mF . (y,v) = o by A1, A2;
reconsider v = v as Element of MPS ;
y * v = o by A2, A6, VECTSP_1:def_12;
then x * (y * v) = mF . (x,o) by A2, VECTSP_1:def_12;
hence (x * y) * v = x * (y * v) by A1, A5; ::_thesis: verum
end;
A7: x * (v + w) = (x * v) + (x * w)
proof
reconsider v = v, w = w as Element of {0} by A2;
A8: md . (v,w) = o by Lm1;
reconsider v = v, w = w as Element of MPS ;
x * (v + w) = mF . (x,o) by A2, A8, VECTSP_1:def_12;
then A9: x * (v + w) = o by A1;
mF . (x,v) = o by A1;
then A10: x * v = o by A2, VECTSP_1:def_12;
mF . (x,w) = o by A1;
then A11: x * w = o by A2, VECTSP_1:def_12;
o = 0. MPS by A2;
hence x * (v + w) = (x * v) + (x * w) by A9, A10, A11, RLVECT_1:4; ::_thesis: verum
end;
A12: (x + y) * v = (x * v) + (y * v)
proof
set z = x + y;
A13: (x + y) * v = mF . ((x + y),v) by A2, VECTSP_1:def_12;
reconsider v = v as Element of MPS ;
reconsider v = v as Element of MPS ;
A14: (x + y) * v = o by A1, A2, A13;
reconsider v = v as Element of MPS ;
A15: mF . (x,v) = o by A1, A2;
reconsider v = v as Element of MPS ;
A16: x * v = o by A2, A15, VECTSP_1:def_12;
reconsider v = v as Element of MPS ;
A17: mF . (y,v) = o by A1, A2;
A18: o = 0. MPS by A2;
reconsider v = v as Element of MPS ;
y * v = o by A2, A17, VECTSP_1:def_12;
hence (x + y) * v = (x * v) + (y * v) by A14, A16, A18, RLVECT_1:4; ::_thesis: verum
end;
(1_ F) * v = v
proof
set one1 = 1_ F;
A19: (1_ F) * v = mF . ((1_ F),v) by A2, VECTSP_1:def_12;
reconsider v = v as Element of MPS ;
mF . ((1_ F),v) = o by A1, A2;
hence (1_ F) * v = v by A2, A19, TARSKI:def_1; ::_thesis: verum
end;
hence ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ F) * v = v ) by A7, A12, A3; ::_thesis: verum
end;
hence ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) by VECTSP_1:def_14, VECTSP_1:def_15, VECTSP_1:def_16, VECTSP_1:def_17; ::_thesis: verum
end;
Lm5: now__::_thesis:_for_F_being_Field
for_mF_being_Function_of_[:_the_carrier_of_F,{0}:],{0}
for_mo_being_Relation_of_{0}_st_(_for_x_being_set_holds_
(_x_in_mo_iff_(_x_in_[:{0},{0}:]_&_ex_a,_b_being_Element_of_{0}_st_
(_x_=_[a,b]_&_b_=_o_)_)_)_)_holds_
for_MPS_being_non_empty_right_complementable_Abelian_add-associative_right_zeroed_SymStr_over_F_st_MPS_=_SymStr(#_{0},md,o,mF,mo_#)_holds_
(_(_for_a_being_Element_of_MPS_st_a_<>_0._MPS_holds_
ex_p_being_Element_of_MPS_st_not_a__|__)_&_(_for_a,_b_being_Element_of_MPS
for_l_being_Element_of_F_st_b__|__holds_
b__|__)_&_(_for_a,_b,_c_being_Element_of_MPS_st_a__|__&_a__|__holds_
a__|__)_&_(_for_a,_b,_x_being_Element_of_MPS_st_not_a__|__holds_
ex_k_being_Element_of_F_st_a__|__)_&_(_for_a,_b,_c_being_Element_of_MPS_st_b_+_c__|__&_c_+_a__|__holds_
a_+_b__|__)_)
set CV = [:{0},{0}:];
let F be Field; ::_thesis: for mF being Function of [: the carrier of F,{0}:],{0}
for mo being Relation of {0} st ( for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) ) ) holds
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# {0},md,o,mF,mo #) holds
( ( for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) )
let mF be Function of [: the carrier of F,{0}:],{0}; ::_thesis: for mo being Relation of {0} st ( for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) ) ) holds
for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# {0},md,o,mF,mo #) holds
( ( for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) )
let mo be Relation of {0}; ::_thesis: ( ( for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) ) ) implies for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# {0},md,o,mF,mo #) holds
( ( for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) ) )
assume A1: for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) ) ; ::_thesis: for MPS being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st MPS = SymStr(# {0},md,o,mF,mo #) holds
( ( for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) )
let MPS be non empty right_complementable Abelian add-associative right_zeroed SymStr over F; ::_thesis: ( MPS = SymStr(# {0},md,o,mF,mo #) implies ( ( for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) ) )
assume A2: MPS = SymStr(# {0},md,o,mF,mo #) ; ::_thesis: ( ( for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ ) & ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) )
thus for a being Element of MPS st a <> 0. MPS holds
ex p being Element of MPS st not a _|_ by A2, TARSKI:def_1; ::_thesis: ( ( for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ) & ( for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) )
A3: for a, b being Element of MPS holds
( b _|_ iff ( [a,b] in [:{0},{0}:] & ex c, d being Element of {0} st
( [a,b] = [c,d] & d = o ) ) )
proof
let a, b be Element of MPS; ::_thesis: ( b _|_ iff ( [a,b] in [:{0},{0}:] & ex c, d being Element of {0} st
( [a,b] = [c,d] & d = o ) ) )
( b _|_ iff [a,b] in mo ) by A2, ORDERS_2:def_5;
hence ( b _|_ iff ( [a,b] in [:{0},{0}:] & ex c, d being Element of {0} st
( [a,b] = [c,d] & d = o ) ) ) by A1; ::_thesis: verum
end;
A4: for a, b being Element of MPS holds
( b _|_ iff b = o )
proof
let a, b be Element of MPS; ::_thesis: ( b _|_ iff b = o )
A5: ( b = o implies b _|_ )
proof
consider c, d being Element of MPS such that
A6: ( c = a & d = b ) ;
assume A7: b = o ; ::_thesis: b _|_
[a,b] = [c,d] by A6;
hence b _|_ by A2, A3, A7; ::_thesis: verum
end;
( b _|_ implies b = o )
proof
assume b _|_ ; ::_thesis: b = o
then ex c, d being Element of {0} st
( [a,b] = [c,d] & d = o ) by A3;
hence b = o by XTUPLE_0:1; ::_thesis: verum
end;
hence ( b _|_ iff b = o ) by A5; ::_thesis: verum
end;
thus for a, b being Element of MPS
for l being Element of F st b _|_ holds
b _|_ ::_thesis: ( ( for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ) & ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) )
proof
let a, b be Element of MPS; ::_thesis: for l being Element of F st b _|_ holds
b _|_
let l be Element of F; ::_thesis: ( b _|_ implies b _|_ )
assume b _|_ ; ::_thesis: b _|_
then b = o by A4;
hence b _|_ by A4; ::_thesis: verum
end;
thus for a, b, c being Element of MPS st a _|_ & a _|_ holds
a _|_ ::_thesis: ( ( for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ) & ( for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_ ) )
proof
let a, b, c be Element of MPS; ::_thesis: ( a _|_ & a _|_ implies a _|_ )
assume that
A8: a _|_ and
a _|_ ; ::_thesis: a _|_
a = o by A4, A8;
hence a _|_ by A4; ::_thesis: verum
end;
thus for a, b, x being Element of MPS st not a _|_ holds
ex k being Element of F st a _|_ ::_thesis: for a, b, c being Element of MPS st b + c _|_ & c + a _|_ holds
a + b _|_
proof
let a, b, x be Element of MPS; ::_thesis: ( not a _|_ implies ex k being Element of F st a _|_ )
assume A9: not a _|_ ; ::_thesis: ex k being Element of F st a _|_
assume for k being Element of F holds not a _|_ ; ::_thesis: contradiction
a <> o by A4, A9;
hence contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
let a, b, c be Element of MPS; ::_thesis: ( b + c _|_ & c + a _|_ implies a + b _|_ )
assume that
b + c _|_ and
c + a _|_ ; ::_thesis: a + b _|_
assume not a + b _|_ ; ::_thesis: contradiction
then a + b <> o by A4;
hence contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
definition
let F be Field;
let IT be non empty right_complementable Abelian add-associative right_zeroed SymStr over F;
attrIT is SymSp-like means :Def1: :: SYMSP_1:def 1
for a, b, c, x being Element of IT
for l being Element of F holds
( ( a <> 0. IT implies ex y being Element of IT st not a _|_ ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b + c _|_ & c + a _|_ implies a + b _|_ ) );
end;
:: deftheorem Def1 defines SymSp-like SYMSP_1:def_1_:_
for F being Field
for IT being non empty right_complementable Abelian add-associative right_zeroed SymStr over F holds
( IT is SymSp-like iff for a, b, c, x being Element of IT
for l being Element of F holds
( ( a <> 0. IT implies ex y being Element of IT st not a _|_ ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b + c _|_ & c + a _|_ implies a + b _|_ ) ) );
registration
let F be Field;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict SymSp-like for SymStr over F;
existence
ex b1 being non empty right_complementable Abelian add-associative right_zeroed SymStr over F st
( b1 is SymSp-like & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is strict )
proof
deffunc H2( Element of F, Element of {0}) -> Element of {0} = o;
consider mF being Function of [: the carrier of F,{0}:],{0} such that
A1: for a being Element of F
for x being Element of {0} holds mF . (a,x) = H2(a,x) from BINOP_1:sch_4();
consider mo being Relation of {0} such that
A2: for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) ) by Lm2;
reconsider MPS = SymStr(# {0},md,o,mF,mo #) as non empty right_complementable Abelian add-associative right_zeroed SymStr over F by Lm3;
take MPS ; ::_thesis: ( MPS is SymSp-like & MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital & MPS is strict )
thus for a, b, c, x being Element of MPS
for l being Element of F holds
( ( a <> 0. MPS implies ex y being Element of MPS st not a _|_ ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b + c _|_ & c + a _|_ implies a + b _|_ ) ) by A2, Lm5; :: according to SYMSP_1:def_1 ::_thesis: ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital & MPS is strict )
thus ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) by A1, Lm4; ::_thesis: MPS is strict
thus MPS is strict ; ::_thesis: verum
end;
end;
definition
let F be Field;
mode SymSp of F is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital SymSp-like SymStr over F;
end;
theorem Th1: :: SYMSP_1:1
for F being Field
for S being SymSp of F
for a being Element of S holds a _|_
proof
let F be Field; ::_thesis: for S being SymSp of F
for a being Element of S holds a _|_
let S be SymSp of F; ::_thesis: for a being Element of S holds a _|_
let a be Element of S; ::_thesis: a _|_
set 0V = 0. S;
set 0F = 0. F;
A1: now__::_thesis:_(_not_a__|__implies_a__|__)
assume not a _|_ ; ::_thesis: a _|_
then consider m being Element of F such that
A2: a _|_ by Def1;
a _|_ by A2, Def1;
hence a _|_ by VECTSP_1:14; ::_thesis: verum
end;
now__::_thesis:_(_a__|__implies_a__|__)
assume a _|_ ; ::_thesis: a _|_
then a _|_ by Def1;
hence a _|_ by VECTSP_1:14; ::_thesis: verum
end;
hence a _|_ by A1; ::_thesis: verum
end;
theorem Th2: :: SYMSP_1:2
for F being Field
for S being SymSp of F
for a, b being Element of S st b _|_ holds
a _|_
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, b being Element of S st b _|_ holds
a _|_
let S be SymSp of F; ::_thesis: for a, b being Element of S st b _|_ holds
a _|_
let a, b be Element of S; ::_thesis: ( b _|_ implies a _|_ )
set 0V = 0. S;
assume b _|_ ; ::_thesis: a _|_
then A1: (0. S) + b _|_ by RLVECT_1:4;
b + a _|_ by Th1;
then a + (0. S) _|_ by A1, Def1;
hence a _|_ by RLVECT_1:4; ::_thesis: verum
end;
theorem Th3: :: SYMSP_1:3
for F being Field
for S being SymSp of F
for a, b, c being Element of S st not b _|_ & b _|_ holds
not b _|_
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, b, c being Element of S st not b _|_ & b _|_ holds
not b _|_
let S be SymSp of F; ::_thesis: for a, b, c being Element of S st not b _|_ & b _|_ holds
not b _|_
let a, b, c be Element of S; ::_thesis: ( not b _|_ & b _|_ implies not b _|_ )
assume that
A1: not b _|_ and
A2: b _|_ ; ::_thesis: not b _|_
assume b _|_ ; ::_thesis: contradiction
then b _|_ by Def1;
then b _|_ by VECTSP_1:14;
then b _|_ by A2, Def1;
then b _|_ by RLVECT_1:def_3;
then b _|_ by RLVECT_1:5;
hence contradiction by A1, RLVECT_1:4; ::_thesis: verum
end;
theorem Th4: :: SYMSP_1:4
for F being Field
for S being SymSp of F
for b, a, c being Element of S st not a _|_ & a _|_ holds
not a _|_
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, c being Element of S st not a _|_ & a _|_ holds
not a _|_
let S be SymSp of F; ::_thesis: for b, a, c being Element of S st not a _|_ & a _|_ holds
not a _|_
let b, a, c be Element of S; ::_thesis: ( not a _|_ & a _|_ implies not a _|_ )
assume that
A1: not a _|_ and
A2: a _|_ ; ::_thesis: not a _|_
a _|_ by A2, Def1;
then A3: a _|_ by VECTSP_1:14;
assume a _|_ ; ::_thesis: contradiction
then a _|_ by A3, Def1;
then a _|_ by RLVECT_1:def_3;
then a _|_ by RLVECT_1:5;
hence contradiction by A1, RLVECT_1:4; ::_thesis: verum
end;
theorem Th5: :: SYMSP_1:5
for F being Field
for S being SymSp of F
for b, a being Element of S
for l being Element of F st not a _|_ & not l = 0. F holds
( not a _|_ & not l * a _|_ )
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a being Element of S
for l being Element of F st not a _|_ & not l = 0. F holds
( not a _|_ & not l * a _|_ )
let S be SymSp of F; ::_thesis: for b, a being Element of S
for l being Element of F st not a _|_ & not l = 0. F holds
( not a _|_ & not l * a _|_ )
let b, a be Element of S; ::_thesis: for l being Element of F st not a _|_ & not l = 0. F holds
( not a _|_ & not l * a _|_ )
let l be Element of F; ::_thesis: ( not a _|_ & not l = 0. F implies ( not a _|_ & not l * a _|_ ) )
set 1F = 1. F;
assume that
A1: not a _|_ and
A2: not l = 0. F ; ::_thesis: ( not a _|_ & not l * a _|_ )
A3: now__::_thesis:_not_l_*_a__|_
consider k being Element of F such that
A4: k * l = 1. F by A2, VECTSP_1:def_9;
assume l * a _|_ ; ::_thesis: contradiction
then b _|_ by Th2;
then b _|_ by Def1;
then b _|_ by A4, VECTSP_1:def_16;
then b _|_ by VECTSP_1:def_17;
hence contradiction by A1, Th2; ::_thesis: verum
end;
now__::_thesis:_not_a__|_
consider k being Element of F such that
A5: k * l = 1. F by A2, VECTSP_1:def_9;
assume a _|_ ; ::_thesis: contradiction
then a _|_ by Def1;
then a _|_ by A5, VECTSP_1:def_16;
hence contradiction by A1, VECTSP_1:def_17; ::_thesis: verum
end;
hence ( not a _|_ & not l * a _|_ ) by A3; ::_thesis: verum
end;
theorem Th6: :: SYMSP_1:6
for F being Field
for S being SymSp of F
for a, b being Element of S st b _|_ holds
b _|_
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, b being Element of S st b _|_ holds
b _|_
let S be SymSp of F; ::_thesis: for a, b being Element of S st b _|_ holds
b _|_
let a, b be Element of S; ::_thesis: ( b _|_ implies b _|_ )
assume b _|_ ; ::_thesis: b _|_
then b _|_ by Def1;
hence b _|_ by VECTSP_1:14; ::_thesis: verum
end;
theorem Th7: :: SYMSP_1:7
for F being Field
for S being SymSp of F
for a, c, b being Element of S holds
( c _|_ or not c _|_ or not c _|_ )
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, c, b being Element of S holds
( c _|_ or not c _|_ or not c _|_ )
let S be SymSp of F; ::_thesis: for a, c, b being Element of S holds
( c _|_ or not c _|_ or not c _|_ )
let a, c, b be Element of S; ::_thesis: ( c _|_ or not c _|_ or not c _|_ )
set 1F = 1_ F;
assume A1: not c _|_ ; ::_thesis: ( not c _|_ or not c _|_ )
assume A2: ( c _|_ & c _|_ ) ; ::_thesis: contradiction
then c _|_ by VECTSP_1:def_15;
then c _|_ by VECTSP_1:def_17;
then c _|_ by VECTSP_1:def_17;
then c _|_ by RLVECT_1:def_3;
hence contradiction by A1, A2, Th4; ::_thesis: verum
end;
theorem Th8: :: SYMSP_1:8
for F being Field
for S being SymSp of F
for a9, a, b, b9 being Element of S st not a _|_ & b _|_ & not b _|_ & a _|_ holds
( not a _|_ & not b _|_ )
proof
let F be Field; ::_thesis: for S being SymSp of F
for a9, a, b, b9 being Element of S st not a _|_ & b _|_ & not b _|_ & a _|_ holds
( not a _|_ & not b _|_ )
let S be SymSp of F; ::_thesis: for a9, a, b, b9 being Element of S st not a _|_ & b _|_ & not b _|_ & a _|_ holds
( not a _|_ & not b _|_ )
let a9, a, b, b9 be Element of S; ::_thesis: ( not a _|_ & b _|_ & not b _|_ & a _|_ implies ( not a _|_ & not b _|_ ) )
set 0V = 0. S;
assume that
A1: not a _|_ and
A2: b _|_ and
A3: not b _|_ and
A4: a _|_ ; ::_thesis: ( not a _|_ & not b _|_ )
assume ( a _|_ or b _|_ ) ; ::_thesis: contradiction
then ( ( a _|_ & a _|_ ) or ( b _|_ & b _|_ ) ) by A2, A4, Def1;
then ( ( a _|_ & a _|_ ) or ( b _|_ & b _|_ ) ) by VECTSP_1:14;
then ( a _|_ or b _|_ ) by Def1;
then ( a _|_ or b _|_ ) by RLVECT_1:def_3;
then ( a _|_ or b _|_ ) by RLVECT_1:5;
hence contradiction by A1, A3, RLVECT_1:4; ::_thesis: verum
end;
theorem Th9: :: SYMSP_1:9
for F being Field
for S being SymSp of F
for a, b being Element of S st a <> 0. S & b <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ )
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, b being Element of S st a <> 0. S & b <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ )
let S be SymSp of F; ::_thesis: for a, b being Element of S st a <> 0. S & b <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ )
let a, b be Element of S; ::_thesis: ( a <> 0. S & b <> 0. S implies ex p being Element of S st
( not a _|_ & not b _|_ ) )
assume that
A1: a <> 0. S and
A2: b <> 0. S ; ::_thesis: ex p being Element of S st
( not a _|_ & not b _|_ )
consider a9 being Element of S such that
A3: not a _|_ by A1, Def1;
now__::_thesis:_(_b__|__implies_ex_p_being_Element_of_S_st_
(_not_a__|__&_not_b__|__)_)
consider b9 being Element of S such that
A4: not b _|_ by A2, Def1;
assume A5: b _|_ ; ::_thesis: ex p being Element of S st
( not a _|_ & not b _|_ )
now__::_thesis:_(_a__|__implies_ex_p_being_Element_of_S_st_
(_not_a__|__&_not_b__|__)_)
assume a _|_ ; ::_thesis: ex p being Element of S st
( not a _|_ & not b _|_ )
then ( not a _|_ & not b _|_ ) by A3, A5, A4, Th8;
hence ex p being Element of S st
( not a _|_ & not b _|_ ) ; ::_thesis: verum
end;
hence ex p being Element of S st
( not a _|_ & not b _|_ ) by A4; ::_thesis: verum
end;
hence ex p being Element of S st
( not a _|_ & not b _|_ ) by A3; ::_thesis: verum
end;
theorem Th10: :: SYMSP_1:10
for F being Field
for S being SymSp of F
for a, b, c being Element of S st (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, b, c being Element of S st (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
let S be SymSp of F; ::_thesis: for a, b, c being Element of S st (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
let a, b, c be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & a <> 0. S & b <> 0. S & c <> 0. S implies ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) )
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: a <> 0. S and
A3: b <> 0. S and
A4: c <> 0. S ; ::_thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
consider r being Element of S such that
A5: not a _|_ and
A6: not b _|_ by A2, A3, Th9;
consider s being Element of S such that
A7: not a _|_ and
A8: not c _|_ by A2, A4, Th9;
now__::_thesis:_(_c__|__&_b__|__implies_ex_p_being_Element_of_S_st_
(_not_a__|__&_not_b__|__&_not_c__|__)_)
assume that
A9: c _|_ and
A10: b _|_ ; ::_thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
A11: now__::_thesis:_(_not_a__|__implies_ex_p_being_Element_of_S_st_
(_not_a__|__&_not_b__|__&_not_c__|__)_)
c _|_ by A9, Def1;
then A12: not c _|_ by A8, Th4;
not b _|_ by A1, A6, Th5;
then A13: not b _|_ by A10, Th4;
assume not a _|_ ; ::_thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A13, A12; ::_thesis: verum
end;
now__::_thesis:_(_not_a__|__implies_ex_p_being_Element_of_S_st_
(_not_a__|__&_not_b__|__&_not_c__|__)_)
assume A14: not a _|_ ; ::_thesis: ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ )
( not b _|_ & not c _|_ ) by A6, A8, A9, A10, Th4;
hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A14; ::_thesis: verum
end;
hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A5, A11, Th7; ::_thesis: verum
end;
hence ex p being Element of S st
( not a _|_ & not b _|_ & not c _|_ ) by A5, A6, A7, A8; ::_thesis: verum
end;
theorem Th11: :: SYMSP_1:11
for F being Field
for S being SymSp of F
for a, b, d, c being Element of S st d _|_ & d _|_ holds
d _|_
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, b, d, c being Element of S st d _|_ & d _|_ holds
d _|_
let S be SymSp of F; ::_thesis: for a, b, d, c being Element of S st d _|_ & d _|_ holds
d _|_
let a, b, d, c be Element of S; ::_thesis: ( d _|_ & d _|_ implies d _|_ )
assume that
A1: d _|_ and
A2: d _|_ ; ::_thesis: d _|_
d _|_ by A1, Th6;
then d _|_ by VECTSP_1:17;
then d _|_ by A2, Def1;
then d _|_ by RLVECT_1:def_3;
then d _|_ by RLVECT_1:def_3;
then d _|_ by RLVECT_1:5;
hence d _|_ by RLVECT_1:4; ::_thesis: verum
end;
theorem Th12: :: SYMSP_1:12
for F being Field
for S being SymSp of F
for b, a, x being Element of S
for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds
k = l
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x being Element of S
for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds
k = l
let S be SymSp of F; ::_thesis: for b, a, x being Element of S
for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds
k = l
let b, a, x be Element of S; ::_thesis: for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds
k = l
let k, l be Element of F; ::_thesis: ( not a _|_ & a _|_ & a _|_ implies k = l )
assume that
A1: not a _|_ and
A2: ( a _|_ & a _|_ ) ; ::_thesis: k = l
set 1F = 1_ F;
a _|_ by A2, Th11;
then a _|_ by VECTSP_1:14;
then a _|_ by VECTSP_1:def_16;
then a _|_ by VECTSP_1:9;
then a _|_ by VECTSP_1:def_8;
then a _|_ by VECTSP_1:def_15;
then a _|_ by Def1;
then A3: a _|_ by VECTSP_1:def_16;
assume not k = l ; ::_thesis: contradiction
then k - l <> 0. F by RLVECT_1:21;
then a _|_ by A3, VECTSP_1:def_10;
hence contradiction by A1, VECTSP_1:def_17; ::_thesis: verum
end;
theorem Th13: :: SYMSP_1:13
for F being Field
for S being SymSp of F
for a being Element of S st (1_ F) + (1_ F) <> 0. F holds
a _|_
proof
let F be Field; ::_thesis: for S being SymSp of F
for a being Element of S st (1_ F) + (1_ F) <> 0. F holds
a _|_
let S be SymSp of F; ::_thesis: for a being Element of S st (1_ F) + (1_ F) <> 0. F holds
a _|_
let a be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F implies a _|_ )
set 1F = 1_ F;
assume A1: (1_ F) + (1_ F) <> 0. F ; ::_thesis: a _|_
now__::_thesis:_(_a_<>_0._S_implies_a__|__)
assume a <> 0. S ; ::_thesis: a _|_
then consider c being Element of S such that
A2: not a _|_ by Def1;
consider k being Element of F such that
A3: a _|_ by A2, Def1;
a + (- (k * c)) _|_ by A3, Th2;
then a + a _|_ by Def1;
then a + ((1_ F) * a) _|_ by VECTSP_1:def_17;
then ((1_ F) * a) + ((1_ F) * a) _|_ by VECTSP_1:def_17;
then ((1_ F) * a) + ((1_ F) * a) _|_ by VECTSP_1:14;
then ((1_ F) + (1_ F)) * a _|_ by VECTSP_1:def_15;
then ((1_ F) + (1_ F)) * a _|_ by VECTSP_1:def_16;
then ((1_ F) + (1_ F)) * a _|_ by VECTSP_1:9;
then ((1_ F) + (1_ F)) * a _|_ by VECTSP_1:def_8;
then (- k) * c _|_ by Th2;
then (- k) * c _|_ by Def1;
then (- k) * c _|_ by A1, VECTSP_1:20;
then A4: a _|_ by Th2;
a _|_ by A3, VECTSP_1:21;
hence a _|_ by A4, Th4; ::_thesis: verum
end;
hence a _|_ by Th1; ::_thesis: verum
end;
definition
let F be Field;
let S be SymSp of F;
let a, b, x be Element of S;
assume A1: not a _|_ ;
func ProJ (a,b,x) -> Element of F means :Def2: :: SYMSP_1:def 2
for l being Element of F st a _|_ holds
it = l;
existence
ex b1 being Element of F st
for l being Element of F st a _|_ holds
b1 = l
proof
consider k being Element of F such that
A2: a _|_ by A1, Def1;
take k ; ::_thesis: for l being Element of F st a _|_ holds
k = l
let l be Element of F; ::_thesis: ( a _|_ implies k = l )
assume a _|_ ; ::_thesis: k = l
hence k = l by A1, A2, Th12; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of F st ( for l being Element of F st a _|_ holds
b1 = l ) & ( for l being Element of F st a _|_ holds
b2 = l ) holds
b1 = b2
proof
let l1, l2 be Element of F; ::_thesis: ( ( for l being Element of F st a _|_ holds
l1 = l ) & ( for l being Element of F st a _|_ holds
l2 = l ) implies l1 = l2 )
assume that
A3: for l being Element of F st a _|_ holds
l1 = l and
A4: for l being Element of F st a _|_ holds
l2 = l ; ::_thesis: l1 = l2
consider k being Element of F such that
A5: a _|_ by A1, Def1;
l1 = k by A3, A5;
hence l1 = l2 by A4, A5; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines ProJ SYMSP_1:def_2_:_
for F being Field
for S being SymSp of F
for a, b, x being Element of S st not a _|_ holds
for b6 being Element of F holds
( b6 = ProJ (a,b,x) iff for l being Element of F st a _|_ holds
b6 = l );
theorem Th14: :: SYMSP_1:14
for F being Field
for S being SymSp of F
for b, a, x being Element of S st not a _|_ holds
a _|_
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x being Element of S st not a _|_ holds
a _|_
let S be SymSp of F; ::_thesis: for b, a, x being Element of S st not a _|_ holds
a _|_
let b, a, x be Element of S; ::_thesis: ( not a _|_ implies a _|_ )
assume A1: not a _|_ ; ::_thesis: a _|_
then ex l being Element of F st a _|_ by Def1;
hence a _|_ by A1, Def2; ::_thesis: verum
end;
theorem Th15: :: SYMSP_1:15
for F being Field
for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
let S be SymSp of F; ::_thesis: for b, a, x being Element of S
for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
let b, a, x be Element of S; ::_thesis: for l being Element of F st not a _|_ holds
ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
let l be Element of F; ::_thesis: ( not a _|_ implies ProJ (a,b,(l * x)) = l * (ProJ (a,b,x)) )
set L = x - ((ProJ (a,b,x)) * b);
A1: l * (x - ((ProJ (a,b,x)) * b)) = (l * x) - (l * ((ProJ (a,b,x)) * b)) by VECTSP_1:23
.= (l * x) - ((l * (ProJ (a,b,x))) * b) by VECTSP_1:def_16 ;
assume A2: not a _|_ ; ::_thesis: ProJ (a,b,(l * x)) = l * (ProJ (a,b,x))
then A3: a _|_ by Th14;
a _|_ by A2, Th14;
then a _|_ by A1, Def1;
hence ProJ (a,b,(l * x)) = l * (ProJ (a,b,x)) by A2, A3, Th12; ::_thesis: verum
end;
theorem Th16: :: SYMSP_1:16
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S st not a _|_ holds
ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x, y being Element of S st not a _|_ holds
ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))
let S be SymSp of F; ::_thesis: for b, a, x, y being Element of S st not a _|_ holds
ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))
let b, a, x, y be Element of S; ::_thesis: ( not a _|_ implies ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y)) )
set 1F = 1_ F;
set L = (x - ((ProJ (a,b,x)) * b)) + (y - ((ProJ (a,b,y)) * b));
A1: (x - ((ProJ (a,b,x)) * b)) + (y - ((ProJ (a,b,y)) * b)) = (((- ((ProJ (a,b,x)) * b)) + x) + y) + (- ((ProJ (a,b,y)) * b)) by RLVECT_1:def_3
.= ((x + y) + (- ((ProJ (a,b,x)) * b))) + (- ((ProJ (a,b,y)) * b)) by RLVECT_1:def_3
.= (x + y) + ((- ((ProJ (a,b,x)) * b)) + (- ((ProJ (a,b,y)) * b))) by RLVECT_1:def_3
.= (x + y) + (((1_ F) * (- ((ProJ (a,b,x)) * b))) + (- ((ProJ (a,b,y)) * b))) by VECTSP_1:def_17
.= (x + y) + (((1_ F) * (- ((ProJ (a,b,x)) * b))) + ((1_ F) * (- ((ProJ (a,b,y)) * b)))) by VECTSP_1:def_17
.= (x + y) + (((1_ F) * ((- (ProJ (a,b,x))) * b)) + ((1_ F) * (- ((ProJ (a,b,y)) * b)))) by VECTSP_1:21
.= (x + y) + (((1_ F) * ((- (ProJ (a,b,x))) * b)) + ((1_ F) * ((- (ProJ (a,b,y))) * b))) by VECTSP_1:21
.= (x + y) + ((((1_ F) * (- (ProJ (a,b,x)))) * b) + ((1_ F) * ((- (ProJ (a,b,y))) * b))) by VECTSP_1:def_16
.= (x + y) + ((((- (ProJ (a,b,x))) * (1_ F)) * b) + (((1_ F) * (- (ProJ (a,b,y)))) * b)) by VECTSP_1:def_16
.= (x + y) + (((- (ProJ (a,b,x))) * b) + (((- (ProJ (a,b,y))) * (1_ F)) * b)) by VECTSP_1:def_8
.= (x + y) + (((- (ProJ (a,b,x))) * b) + ((- (ProJ (a,b,y))) * b)) by VECTSP_1:def_8
.= (x + y) + (((- (ProJ (a,b,x))) + (- (ProJ (a,b,y)))) * b) by VECTSP_1:def_15
.= (x + y) + ((- ((ProJ (a,b,x)) + (ProJ (a,b,y)))) * b) by RLVECT_1:31
.= (x + y) - (((ProJ (a,b,x)) + (ProJ (a,b,y))) * b) by VECTSP_1:21 ;
assume A2: not a _|_ ; ::_thesis: ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y))
then ( a _|_ & a _|_ ) by Th14;
then A3: a _|_ by Def1;
a _|_ by A2, Th14;
hence ProJ (a,b,(x + y)) = (ProJ (a,b,x)) + (ProJ (a,b,y)) by A2, A3, A1, Th12; ::_thesis: verum
end;
theorem :: SYMSP_1:17
for F being Field
for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
let S be SymSp of F; ::_thesis: for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
let b, a, x be Element of S; ::_thesis: for l being Element of F st not a _|_ & l <> 0. F holds
ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
let l be Element of F; ::_thesis: ( not a _|_ & l <> 0. F implies ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x)) )
assume that
A1: not a _|_ and
A2: l <> 0. F ; ::_thesis: ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x))
set L = x - ((ProJ (a,(l * b),x)) * (l * b));
not a _|_ by A1, A2, Th5;
then A3: a _|_ by Th14;
A4: x - ((ProJ (a,(l * b),x)) * (l * b)) = x - (((ProJ (a,(l * b),x)) * l) * b) by VECTSP_1:def_16;
a _|_ by A1, Th14;
then (ProJ (a,b,x)) * (l ") = ((ProJ (a,(l * b),x)) * l) * (l ") by A1, A3, A4, Th12;
then (ProJ (a,b,x)) * (l ") = (ProJ (a,(l * b),x)) * (l * (l ")) by GROUP_1:def_3;
then (l ") * (ProJ (a,b,x)) = (ProJ (a,(l * b),x)) * (1_ F) by A2, VECTSP_1:def_10;
hence ProJ (a,(l * b),x) = (l ") * (ProJ (a,b,x)) by VECTSP_1:def_8; ::_thesis: verum
end;
theorem Th18: :: SYMSP_1:18
for F being Field
for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
let S be SymSp of F; ::_thesis: for b, a, x being Element of S
for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
let b, a, x be Element of S; ::_thesis: for l being Element of F st not a _|_ & l <> 0. F holds
ProJ ((l * a),b,x) = ProJ (a,b,x)
let l be Element of F; ::_thesis: ( not a _|_ & l <> 0. F implies ProJ ((l * a),b,x) = ProJ (a,b,x) )
assume that
A1: not a _|_ and
A2: l <> 0. F ; ::_thesis: ProJ ((l * a),b,x) = ProJ (a,b,x)
not l * a _|_ by A1, A2, Th5;
then l * a _|_ by Th14;
then x - ((ProJ ((l * a),b,x)) * b) _|_ by Th2;
then x - ((ProJ ((l * a),b,x)) * b) _|_ by Def1;
then x - ((ProJ ((l * a),b,x)) * b) _|_ by VECTSP_1:def_16;
then x - ((ProJ ((l * a),b,x)) * b) _|_ by A2, VECTSP_1:def_10;
then x - ((ProJ ((l * a),b,x)) * b) _|_ by VECTSP_1:def_17;
then A3: a _|_ by Th2;
a _|_ by A1, Th14;
hence ProJ ((l * a),b,x) = ProJ (a,b,x) by A1, A3, Th12; ::_thesis: verum
end;
theorem Th19: :: SYMSP_1:19
for F being Field
for S being SymSp of F
for b, a, p, c being Element of S st not a _|_ & a _|_ holds
( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, p, c being Element of S st not a _|_ & a _|_ holds
( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )
let S be SymSp of F; ::_thesis: for b, a, p, c being Element of S st not a _|_ & a _|_ holds
( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )
let b, a, p, c be Element of S; ::_thesis: ( not a _|_ & a _|_ implies ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) ) )
set 0V = 0. S;
assume that
A1: not a _|_ and
A2: a _|_ ; ::_thesis: ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) )
not a _|_ by A1, A2, Th4;
then a _|_ by Th14;
then a _|_ by VECTSP_1:def_14;
then A3: a _|_ by VECTSP_1:17;
( a _|_ & a _|_ ) by A1, A2, Th6, Th14;
then a _|_ by Def1;
then a _|_ by RLVECT_1:def_3;
then a _|_ by RLVECT_1:def_3;
then a _|_ by RLVECT_1:5;
then A4: a _|_ by RLVECT_1:4;
a _|_ by A2, Def1;
then a _|_ by A3, Def1;
then a _|_ by RLVECT_1:def_3;
then a _|_ by RLVECT_1:5;
then A5: a _|_ by RLVECT_1:4;
a _|_ by A1, Th14;
hence ( ProJ (a,(b + p),c) = ProJ (a,b,c) & ProJ (a,b,(c + p)) = ProJ (a,b,c) ) by A1, A5, A4, Th12; ::_thesis: verum
end;
theorem Th20: :: SYMSP_1:20
for F being Field
for S being SymSp of F
for b, a, p, c being Element of S st not a _|_ & b _|_ & c _|_ holds
ProJ ((a + p),b,c) = ProJ (a,b,c)
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, p, c being Element of S st not a _|_ & b _|_ & c _|_ holds
ProJ ((a + p),b,c) = ProJ (a,b,c)
let S be SymSp of F; ::_thesis: for b, a, p, c being Element of S st not a _|_ & b _|_ & c _|_ holds
ProJ ((a + p),b,c) = ProJ (a,b,c)
let b, a, p, c be Element of S; ::_thesis: ( not a _|_ & b _|_ & c _|_ implies ProJ ((a + p),b,c) = ProJ (a,b,c) )
assume that
A1: not a _|_ and
A2: b _|_ and
A3: c _|_ ; ::_thesis: ProJ ((a + p),b,c) = ProJ (a,b,c)
p _|_ by A2, Th2;
then p _|_ by Def1;
then A4: p _|_ by Th6;
p _|_ by A3, Th2;
then p _|_ by A4, Def1;
then A5: c - ((ProJ (a,b,c)) * b) _|_ by Th2;
a _|_ by A1, Th14;
then c - ((ProJ (a,b,c)) * b) _|_ by Th2;
then c - ((ProJ (a,b,c)) * b) _|_ by A5, Def1;
then A6: a + p _|_ by Th2;
not b _|_ by A1, Th2;
then not b _|_ by A2, Th4;
then A7: not a + p _|_ by Th2;
then a + p _|_ by Th14;
hence ProJ ((a + p),b,c) = ProJ (a,b,c) by A7, A6, Th12; ::_thesis: verum
end;
theorem Th21: :: SYMSP_1:21
for F being Field
for S being SymSp of F
for b, a, c being Element of S st not a _|_ & a _|_ holds
ProJ (a,b,c) = 1_ F
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, c being Element of S st not a _|_ & a _|_ holds
ProJ (a,b,c) = 1_ F
let S be SymSp of F; ::_thesis: for b, a, c being Element of S st not a _|_ & a _|_ holds
ProJ (a,b,c) = 1_ F
let b, a, c be Element of S; ::_thesis: ( not a _|_ & a _|_ implies ProJ (a,b,c) = 1_ F )
assume that
A1: not a _|_ and
A2: a _|_ ; ::_thesis: ProJ (a,b,c) = 1_ F
( a _|_ & a _|_ ) by A1, A2, Th14, VECTSP_1:def_17;
hence ProJ (a,b,c) = 1_ F by A1, Th12; ::_thesis: verum
end;
theorem Th22: :: SYMSP_1:22
for F being Field
for S being SymSp of F
for b, a being Element of S st not a _|_ holds
ProJ (a,b,b) = 1_ F
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a being Element of S st not a _|_ holds
ProJ (a,b,b) = 1_ F
let S be SymSp of F; ::_thesis: for b, a being Element of S st not a _|_ holds
ProJ (a,b,b) = 1_ F
let b, a be Element of S; ::_thesis: ( not a _|_ implies ProJ (a,b,b) = 1_ F )
A1: b - b = 0. S by RLVECT_1:5;
assume not a _|_ ; ::_thesis: ProJ (a,b,b) = 1_ F
hence ProJ (a,b,b) = 1_ F by A1, Th1, Th21; ::_thesis: verum
end;
theorem Th23: :: SYMSP_1:23
for F being Field
for S being SymSp of F
for b, a, x being Element of S st not a _|_ holds
( a _|_ iff ProJ (a,b,x) = 0. F )
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x being Element of S st not a _|_ holds
( a _|_ iff ProJ (a,b,x) = 0. F )
let S be SymSp of F; ::_thesis: for b, a, x being Element of S st not a _|_ holds
( a _|_ iff ProJ (a,b,x) = 0. F )
let b, a, x be Element of S; ::_thesis: ( not a _|_ implies ( a _|_ iff ProJ (a,b,x) = 0. F ) )
set 0F = 0. F;
set 0V = 0. S;
A1: now__::_thesis:_(_not_a__|__&_a__|__implies_ProJ_(a,b,x)_=_0._F_)
assume that
A2: not a _|_ and
A3: a _|_ ; ::_thesis: ProJ (a,b,x) = 0. F
a _|_ by A3, RLVECT_1:4;
then a _|_ by RLVECT_1:12;
then A4: a _|_ by VECTSP_1:14;
a _|_ by A2, Th14;
hence ProJ (a,b,x) = 0. F by A2, A4, Th12; ::_thesis: verum
end;
now__::_thesis:_(_not_a__|__&_ProJ_(a,b,x)_=_0._F_implies_a__|__)
assume ( not a _|_ & ProJ (a,b,x) = 0. F ) ; ::_thesis: a _|_
then a _|_ by Th14;
then a _|_ by VECTSP_1:14;
then a _|_ by RLVECT_1:12;
hence a _|_ by RLVECT_1:4; ::_thesis: verum
end;
hence ( not a _|_ implies ( a _|_ iff ProJ (a,b,x) = 0. F ) ) by A1; ::_thesis: verum
end;
theorem Th24: :: SYMSP_1:24
for F being Field
for S being SymSp of F
for b, a, q, p being Element of S st not a _|_ & not a _|_ holds
(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, q, p being Element of S st not a _|_ & not a _|_ holds
(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)
let S be SymSp of F; ::_thesis: for b, a, q, p being Element of S st not a _|_ & not a _|_ holds
(ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)
let b, a, q, p be Element of S; ::_thesis: ( not a _|_ & not a _|_ implies (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p) )
assume that
A1: not a _|_ and
A2: not a _|_ ; ::_thesis: (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p)
( a _|_ & a _|_ ) by A1, A2, Th14;
then a _|_ by Def1;
then a _|_ by RLVECT_1:def_3;
then a _|_ by RLVECT_1:def_3;
then a _|_ by RLVECT_1:5;
then a _|_ by RLVECT_1:4;
then A3: a _|_ by A1, Th15;
a _|_ by A1, Th14;
then (ProJ (a,q,p)) * (ProJ (a,b,q)) = ProJ (a,b,p) by A1, A3, Th12;
then A4: (ProJ (a,q,p)) * ((ProJ (a,b,q)) * ((ProJ (a,b,q)) ")) = (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") by GROUP_1:def_3;
ProJ (a,b,q) <> 0. F by A1, A2, Th23;
then (ProJ (a,q,p)) * (1_ F) = (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") by A4, VECTSP_1:def_10;
hence (ProJ (a,b,p)) * ((ProJ (a,b,q)) ") = ProJ (a,q,p) by VECTSP_1:def_8; ::_thesis: verum
end;
theorem Th25: :: SYMSP_1:25
for F being Field
for S being SymSp of F
for b, a, c being Element of S st not a _|_ & not a _|_ holds
ProJ (a,b,c) = (ProJ (a,c,b)) "
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, c being Element of S st not a _|_ & not a _|_ holds
ProJ (a,b,c) = (ProJ (a,c,b)) "
let S be SymSp of F; ::_thesis: for b, a, c being Element of S st not a _|_ & not a _|_ holds
ProJ (a,b,c) = (ProJ (a,c,b)) "
let b, a, c be Element of S; ::_thesis: ( not a _|_ & not a _|_ implies ProJ (a,b,c) = (ProJ (a,c,b)) " )
set 1F = 1_ F;
set 0F = 0. F;
assume that
A1: not a _|_ and
A2: not a _|_ ; ::_thesis: ProJ (a,b,c) = (ProJ (a,c,b)) "
A3: ProJ (a,c,b) <> 0. F by A1, A2, Th23;
(ProJ (a,b,b)) * ((ProJ (a,b,c)) ") = ProJ (a,c,b) by A1, A2, Th24;
then ((ProJ (a,b,c)) ") * (1_ F) = ProJ (a,c,b) by A1, Th22;
then A4: (ProJ (a,b,c)) " = ProJ (a,c,b) by VECTSP_1:def_8;
ProJ (a,b,c) <> 0. F by A1, A2, Th23;
then 1_ F = (ProJ (a,c,b)) * (ProJ (a,b,c)) by A4, VECTSP_1:def_10;
then (ProJ (a,c,b)) " = ((ProJ (a,c,b)) ") * ((ProJ (a,c,b)) * (ProJ (a,b,c))) by VECTSP_1:def_8
.= (((ProJ (a,c,b)) ") * (ProJ (a,c,b))) * (ProJ (a,b,c)) by GROUP_1:def_3
.= (ProJ (a,b,c)) * (1_ F) by A3, VECTSP_1:def_10 ;
hence ProJ (a,b,c) = (ProJ (a,c,b)) " by VECTSP_1:def_8; ::_thesis: verum
end;
theorem Th26: :: SYMSP_1:26
for F being Field
for S being SymSp of F
for b, a, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = ProJ (c,b,a)
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = ProJ (c,b,a)
let S be SymSp of F; ::_thesis: for b, a, c being Element of S st not a _|_ & c + a _|_ holds
ProJ (a,b,c) = ProJ (c,b,a)
let b, a, c be Element of S; ::_thesis: ( not a _|_ & c + a _|_ implies ProJ (a,b,c) = ProJ (c,b,a) )
assume that
A1: not a _|_ and
A2: c + a _|_ ; ::_thesis: ProJ (a,b,c) = ProJ (c,b,a)
c + a _|_ by A2, Def1;
then A3: c + a _|_ by Th6;
a _|_ by A1, Th14;
then (- ((ProJ (a,b,c)) * b)) + c _|_ by Th2;
then a + (- ((ProJ (a,b,c)) * b)) _|_ by A3, Def1;
then A4: c _|_ by Th2;
( not b _|_ & b _|_ ) by A1, A2, Th2;
then not b _|_ by Th3;
then A5: not c _|_ by Th2;
then c _|_ by Th14;
hence ProJ (a,b,c) = ProJ (c,b,a) by A5, A4, Th12; ::_thesis: verum
end;
theorem Th27: :: SYMSP_1:27
for F being Field
for S being SymSp of F
for a, b, c being Element of S st not b _|_ & not b _|_ holds
ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c))
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, b, c being Element of S st not b _|_ & not b _|_ holds
ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c))
let S be SymSp of F; ::_thesis: for a, b, c being Element of S st not b _|_ & not b _|_ holds
ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c))
let a, b, c be Element of S; ::_thesis: ( not b _|_ & not b _|_ implies ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c)) )
set 1F = 1_ F;
assume that
A1: not b _|_ and
A2: not b _|_ ; ::_thesis: ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c))
A3: ProJ (b,a,c) <> 0. F by A1, A2, Th23;
then A4: - ((ProJ (b,a,c)) ") <> 0. F by VECTSP_1:25;
(- (1_ F)) * (((ProJ (b,a,c)) ") * (ProJ (b,a,c))) = (- (1_ F)) * (1_ F) by A3, VECTSP_1:def_10;
then ((- (1_ F)) * ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = (- (1_ F)) * (1_ F) by GROUP_1:def_3;
then ((- (1_ F)) * ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = - (1_ F) by VECTSP_1:def_8;
then (- (((ProJ (b,a,c)) ") * (1_ F))) * (ProJ (b,a,c)) = - (1_ F) by VECTSP_1:9;
then (- ((ProJ (b,a,c)) ")) * (ProJ (b,a,c)) = - (1_ F) by VECTSP_1:def_8;
then ProJ (b,a,((- ((ProJ (b,a,c)) ")) * c)) = - (1_ F) by A1, Th15;
then b _|_ by A1, Th14;
then b _|_ by VECTSP_1:14;
then b _|_ by RLVECT_1:17;
then A5: ((- ((ProJ (b,a,c)) ")) * c) + a _|_ by Th2;
not a _|_ by A1, Th2;
then ProJ (a,b,((- ((ProJ (b,a,c)) ")) * c)) = ProJ (((- ((ProJ (b,a,c)) ")) * c),b,a) by A5, Th26;
then ProJ (a,b,((- ((ProJ (b,a,c)) ")) * c)) = ProJ (c,b,a) by A2, A4, Th2, Th18;
hence ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c)) by A1, Th2, Th15; ::_thesis: verum
end;
theorem Th28: :: SYMSP_1:28
for F being Field
for S being SymSp of F
for a, p, q, b being Element of S st (1_ F) + (1_ F) <> 0. F & not p _|_ & not q _|_ & not q _|_ holds
(ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, p, q, b being Element of S st (1_ F) + (1_ F) <> 0. F & not p _|_ & not q _|_ & not q _|_ holds
(ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
let S be SymSp of F; ::_thesis: for a, p, q, b being Element of S st (1_ F) + (1_ F) <> 0. F & not p _|_ & not q _|_ & not q _|_ holds
(ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
let a, p, q, b be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & not p _|_ & not q _|_ & not q _|_ implies (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) )
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not p _|_ and
A3: not q _|_ and
A4: not q _|_ ; ::_thesis: (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
A5: now__::_thesis:_(_q__|__&_b__|__implies_(ProJ_(a,p,q))_*_(ProJ_(b,q,p))_=_(ProJ_(p,a,b))_*_(ProJ_(q,b,a))_)
assume that
A6: q _|_ and
A7: b _|_ ; ::_thesis: (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
not b _|_ by A4, Th2;
then A8: ProJ (b,q,p) = ProJ (b,q,(p + a)) by A7, Th19;
A9: not q _|_ by A3, A6, Th4;
then A10: ProJ (b,q,(p + a)) = (- ((ProJ (q,(p + a),b)) ")) * (ProJ ((p + a),q,b)) by A4, Th27;
A11: a _|_ by A1, Th13;
A12: not a _|_ by A2, Th2;
then A13: ProJ (a,p,q) = ProJ (a,(p + a),q) by A11, Th19;
not a _|_ by A12, A11, Th4;
then A14: not p + a _|_ by Th2;
A15: not p + a _|_ by A9, Th2;
then ProJ (a,(p + a),q) = (- ((ProJ ((p + a),q,a)) ")) * (ProJ (q,(p + a),a)) by A14, Th27;
then (ProJ (a,p,q)) * (ProJ (b,q,p)) = (((ProJ (q,(p + a),a)) * (- ((ProJ ((p + a),q,a)) "))) * (- ((ProJ (q,(p + a),b)) "))) * (ProJ ((p + a),q,b)) by A13, A8, A10, GROUP_1:def_3
.= ((ProJ (q,(p + a),a)) * ((- ((ProJ ((p + a),q,a)) ")) * (- ((ProJ (q,(p + a),b)) ")))) * (ProJ ((p + a),q,b)) by GROUP_1:def_3
.= ((ProJ (q,(p + a),a)) * (((ProJ (q,(p + a),b)) ") * ((ProJ ((p + a),q,a)) "))) * (ProJ ((p + a),q,b)) by VECTSP_1:10
.= (((ProJ (q,(p + a),a)) * ((ProJ (q,(p + a),b)) ")) * ((ProJ ((p + a),q,a)) ")) * (ProJ ((p + a),q,b)) by GROUP_1:def_3
.= ((ProJ (q,b,a)) * ((ProJ ((p + a),q,a)) ")) * (ProJ ((p + a),q,b)) by A4, A9, Th24
.= (ProJ (q,b,a)) * ((ProJ ((p + a),q,b)) * ((ProJ ((p + a),q,a)) ")) by GROUP_1:def_3
.= (ProJ (q,b,a)) * (ProJ ((p + a),a,b)) by A14, A15, Th24
.= (ProJ (q,b,a)) * (ProJ (p,a,b)) by A2, A7, A11, Th20 ;
hence (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) ; ::_thesis: verum
end;
A16: now__::_thesis:_(_not_b__|__implies_(ProJ_(a,p,q))_*_(ProJ_(b,q,p))_=_(ProJ_(p,a,b))_*_(ProJ_(q,b,a))_)
assume A17: not b _|_ ; ::_thesis: (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
A18: not b _|_ by A4, Th2;
then A19: ProJ (q,b,a) = (- ((ProJ (b,a,q)) ")) * (ProJ (a,b,q)) by A17, Th27;
A20: not a _|_ by A2, Th2;
A21: not a _|_ by A17, Th2;
then ProJ (p,a,b) = (- ((ProJ (a,b,p)) ")) * (ProJ (b,a,p)) by A20, Th27;
then (ProJ (p,a,b)) * (ProJ (q,b,a)) = (((ProJ (b,a,p)) * (- ((ProJ (a,b,p)) "))) * (- ((ProJ (b,a,q)) "))) * (ProJ (a,b,q)) by A19, GROUP_1:def_3
.= ((ProJ (b,a,p)) * ((- ((ProJ (a,b,p)) ")) * (- ((ProJ (b,a,q)) ")))) * (ProJ (a,b,q)) by GROUP_1:def_3
.= ((ProJ (b,a,p)) * (((ProJ (b,a,q)) ") * ((ProJ (a,b,p)) "))) * (ProJ (a,b,q)) by VECTSP_1:10
.= (((ProJ (b,a,p)) * ((ProJ (b,a,q)) ")) * ((ProJ (a,b,p)) ")) * (ProJ (a,b,q)) by GROUP_1:def_3
.= ((ProJ (b,q,p)) * ((ProJ (a,b,p)) ")) * (ProJ (a,b,q)) by A17, A18, Th24
.= (ProJ (b,q,p)) * ((ProJ (a,b,q)) * ((ProJ (a,b,p)) ")) by GROUP_1:def_3
.= (ProJ (b,q,p)) * (ProJ (a,p,q)) by A21, A20, Th24 ;
hence (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) ; ::_thesis: verum
end;
now__::_thesis:_(_not_q__|__implies_(ProJ_(a,p,q))_*_(ProJ_(b,q,p))_=_(ProJ_(p,a,b))_*_(ProJ_(q,b,a))_)
assume A22: not q _|_ ; ::_thesis: (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a))
then A23: ProJ (b,q,p) = (- ((ProJ (q,p,b)) ")) * (ProJ (p,q,b)) by A4, Th27;
A24: not p _|_ by A22, Th2;
then ProJ (a,p,q) = (- ((ProJ (p,q,a)) ")) * (ProJ (q,p,a)) by A2, Th27;
then (ProJ (a,p,q)) * (ProJ (b,q,p)) = (((ProJ (q,p,a)) * (- ((ProJ (p,q,a)) "))) * (- ((ProJ (q,p,b)) "))) * (ProJ (p,q,b)) by A23, GROUP_1:def_3
.= ((ProJ (q,p,a)) * ((- ((ProJ (p,q,a)) ")) * (- ((ProJ (q,p,b)) ")))) * (ProJ (p,q,b)) by GROUP_1:def_3
.= ((ProJ (q,p,a)) * (((ProJ (q,p,b)) ") * ((ProJ (p,q,a)) "))) * (ProJ (p,q,b)) by VECTSP_1:10
.= (((ProJ (q,p,a)) * ((ProJ (q,p,b)) ")) * ((ProJ (p,q,a)) ")) * (ProJ (p,q,b)) by GROUP_1:def_3
.= ((ProJ (q,b,a)) * ((ProJ (p,q,a)) ")) * (ProJ (p,q,b)) by A4, A22, Th24
.= (ProJ (q,b,a)) * ((ProJ (p,q,b)) * ((ProJ (p,q,a)) ")) by GROUP_1:def_3
.= (ProJ (q,b,a)) * (ProJ (p,a,b)) by A2, A24, Th24 ;
hence (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) ; ::_thesis: verum
end;
hence (ProJ (a,p,q)) * (ProJ (b,q,p)) = (ProJ (p,a,b)) * (ProJ (q,b,a)) by A16, A5; ::_thesis: verum
end;
theorem Th29: :: SYMSP_1:29
for F being Field
for S being SymSp of F
for p, a, x, q being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x))
proof
let F be Field; ::_thesis: for S being SymSp of F
for p, a, x, q being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x))
let S be SymSp of F; ::_thesis: for p, a, x, q being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ holds
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x))
let p, a, x, q be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ implies (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ and
A3: not x _|_ and
A4: not a _|_ and
A5: not x _|_ ; ::_thesis: (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x))
A6: ( not q _|_ & not q _|_ ) by A4, A5, Th2;
(ProJ (p,a,x)) * (ProJ (q,x,a)) = (ProJ (a,p,q)) * (ProJ (x,q,p)) by A1, A2, A3, A5, Th28;
then (ProJ (p,a,x)) * (ProJ (q,x,a)) = ((ProJ (a,q,p)) ") * (ProJ (x,q,p)) by A2, A4, Th25;
then A7: (ProJ (a,q,p)) * ((ProJ (p,a,x)) * (ProJ (q,x,a))) = ((ProJ (a,q,p)) * ((ProJ (a,q,p)) ")) * (ProJ (x,q,p)) by GROUP_1:def_3;
ProJ (a,q,p) <> 0. F by A2, A4, Th23;
then (ProJ (a,q,p)) * ((ProJ (p,a,x)) * (ProJ (q,x,a))) = (ProJ (x,q,p)) * (1_ F) by A7, VECTSP_1:def_10;
then (ProJ (a,q,p)) * ((ProJ (p,a,x)) * (ProJ (q,x,a))) = ProJ (x,q,p) by VECTSP_1:def_8;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (ProJ (q,x,a)) = ProJ (x,q,p) by GROUP_1:def_3;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * ((ProJ (q,a,x)) ") = ProJ (x,q,p) by A6, Th25;
then A8: ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (((ProJ (q,a,x)) ") * (ProJ (q,a,x))) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by GROUP_1:def_3;
ProJ (q,a,x) <> 0. F by A6, Th23;
then ((ProJ (a,q,p)) * (ProJ (p,a,x))) * (1_ F) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by A8, VECTSP_1:def_10;
hence (ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by VECTSP_1:def_8; ::_thesis: verum
end;
theorem Th30: :: SYMSP_1:30
for F being Field
for S being SymSp of F
for p, a, x, q, b, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ & not a _|_ holds
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
proof
let F be Field; ::_thesis: for S being SymSp of F
for p, a, x, q, b, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ & not a _|_ holds
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
let S be SymSp of F; ::_thesis: for p, a, x, q, b, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ & not a _|_ holds
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
let p, a, x, q, b, y be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ & not x _|_ & not a _|_ & not x _|_ & not a _|_ implies ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: ( (1_ F) + (1_ F) <> 0. F & not a _|_ ) and
A2: not x _|_ and
A3: not a _|_ and
A4: not x _|_ and
A5: not a _|_ ; ::_thesis: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
A6: now__::_thesis:_(_not_x__|__implies_((ProJ_(a,b,p))_*_(ProJ_(p,a,x)))_*_(ProJ_(x,p,y))_=_((ProJ_(a,b,q))_*_(ProJ_(q,a,x)))_*_(ProJ_(x,q,y))_)
A7: ProJ (a,b,q) <> 0. F by A3, A5, Th23;
assume A8: not x _|_ ; ::_thesis: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
(ProJ (a,q,p)) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by A1, A2, A3, A4, Th29;
then ((ProJ (a,b,p)) * ((ProJ (a,b,q)) ")) * (ProJ (p,a,x)) = (ProJ (x,q,p)) * (ProJ (q,a,x)) by A3, A5, Th24;
then (((ProJ (a,b,q)) ") * (ProJ (a,b,p))) * (ProJ (p,a,x)) = ((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x)) by A4, A8, Th24;
then (ProJ (a,b,q)) * (((ProJ (a,b,q)) ") * ((ProJ (a,b,p)) * (ProJ (p,a,x)))) = (ProJ (a,b,q)) * (((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x))) by GROUP_1:def_3;
then ((ProJ (a,b,q)) * ((ProJ (a,b,q)) ")) * ((ProJ (a,b,p)) * (ProJ (p,a,x))) = (ProJ (a,b,q)) * (((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x))) by GROUP_1:def_3;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (1_ F) = (ProJ (a,b,q)) * (((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x))) by A7, VECTSP_1:def_10;
then (ProJ (a,b,p)) * (ProJ (p,a,x)) = (ProJ (a,b,q)) * (((ProJ (x,y,p)) * ((ProJ (x,y,q)) ")) * (ProJ (q,a,x))) by VECTSP_1:def_8;
then (ProJ (a,b,p)) * (ProJ (p,a,x)) = (ProJ (a,b,q)) * ((((ProJ (x,y,q)) ") * ((ProJ (x,p,y)) ")) * (ProJ (q,a,x))) by A2, A8, Th25;
then (ProJ (a,b,p)) * (ProJ (p,a,x)) = ((ProJ (a,b,q)) * (((ProJ (x,y,q)) ") * ((ProJ (x,p,y)) "))) * (ProJ (q,a,x)) by GROUP_1:def_3;
then (ProJ (a,b,p)) * (ProJ (p,a,x)) = (ProJ (q,a,x)) * (((ProJ (a,b,q)) * ((ProJ (x,y,q)) ")) * ((ProJ (x,p,y)) ")) by GROUP_1:def_3;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = (((ProJ (q,a,x)) * ((ProJ (a,b,q)) * ((ProJ (x,y,q)) "))) * ((ProJ (x,p,y)) ")) * (ProJ (x,p,y)) by GROUP_1:def_3;
then A9: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (q,a,x)) * ((ProJ (a,b,q)) * ((ProJ (x,y,q)) "))) * (((ProJ (x,p,y)) ") * (ProJ (x,p,y))) by GROUP_1:def_3;
ProJ (x,p,y) <> 0. F by A2, A8, Th23;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (q,a,x)) * ((ProJ (a,b,q)) * ((ProJ (x,y,q)) "))) * (1_ F) by A9, VECTSP_1:def_10;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = (ProJ (q,a,x)) * ((ProJ (a,b,q)) * ((ProJ (x,y,q)) ")) by VECTSP_1:def_8;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = (ProJ (q,a,x)) * ((ProJ (a,b,q)) * (ProJ (x,q,y))) by A4, A8, Th25;
hence ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) by GROUP_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_x__|__implies_((ProJ_(a,b,p))_*_(ProJ_(p,a,x)))_*_(ProJ_(x,p,y))_=_((ProJ_(a,b,q))_*_(ProJ_(q,a,x)))_*_(ProJ_(x,q,y))_)
assume A10: x _|_ ; ::_thesis: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
then ProJ (x,p,y) = 0. F by A2, Th23;
then A11: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F by VECTSP_1:7;
ProJ (x,q,y) = 0. F by A4, A10, Th23;
hence ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) by A11, VECTSP_1:7; ::_thesis: verum
end;
hence ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) by A6; ::_thesis: verum
end;
theorem Th31: :: SYMSP_1:31
for F being Field
for S being SymSp of F
for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
proof
let F be Field; ::_thesis: for S being SymSp of F
for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
let S be SymSp of F; ::_thesis: for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
let a, p, x, y be Element of S; ::_thesis: ( not p _|_ & not p _|_ & not p _|_ implies (ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x)) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: not p _|_ and
A2: not p _|_ and
A3: not p _|_ ; ::_thesis: (ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
A4: not y _|_ by A3, Th2;
A5: not x _|_ by A2, Th2;
A6: now__::_thesis:_(_not_x__|__implies_(ProJ_(p,a,x))_*_(ProJ_(x,p,y))_=_(-_(ProJ_(p,a,y)))_*_(ProJ_(y,p,x))_)
A7: ProJ (p,a,x) <> 0. F by A1, A2, Th23;
assume A8: not x _|_ ; ::_thesis: (ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
then A9: not y _|_ by Th2;
(ProJ (p,a,y)) * ((ProJ (p,a,x)) ") = ProJ (p,x,y) by A1, A2, Th24;
then ((ProJ (p,a,y)) * ((ProJ (p,a,x)) ")) * (ProJ (p,a,x)) = ((- ((ProJ (x,y,p)) ")) * (ProJ (y,x,p))) * (ProJ (p,a,x)) by A5, A8, Th27;
then (ProJ (p,a,y)) * (((ProJ (p,a,x)) ") * (ProJ (p,a,x))) = ((- ((ProJ (x,y,p)) ")) * (ProJ (y,x,p))) * (ProJ (p,a,x)) by GROUP_1:def_3;
then (ProJ (p,a,y)) * (1_ F) = ((- ((ProJ (x,y,p)) ")) * (ProJ (y,x,p))) * (ProJ (p,a,x)) by A7, VECTSP_1:def_10;
then ProJ (p,a,y) = ((ProJ (y,x,p)) * (- ((ProJ (x,y,p)) "))) * (ProJ (p,a,x)) by VECTSP_1:def_8;
then ProJ (p,a,y) = (ProJ (y,x,p)) * ((- ((ProJ (x,y,p)) ")) * (ProJ (p,a,x))) by GROUP_1:def_3;
then (ProJ (y,p,x)) * (ProJ (p,a,y)) = (ProJ (y,p,x)) * (((ProJ (y,p,x)) ") * ((- ((ProJ (x,y,p)) ")) * (ProJ (p,a,x)))) by A4, A9, Th25;
then A10: (ProJ (y,p,x)) * (ProJ (p,a,y)) = ((ProJ (y,p,x)) * ((ProJ (y,p,x)) ")) * ((- ((ProJ (x,y,p)) ")) * (ProJ (p,a,x))) by GROUP_1:def_3;
ProJ (y,p,x) <> 0. F by A4, A9, Th23;
then (ProJ (y,p,x)) * (ProJ (p,a,y)) = ((- ((ProJ (x,y,p)) ")) * (ProJ (p,a,x))) * (1_ F) by A10, VECTSP_1:def_10;
then (ProJ (p,a,y)) * (ProJ (y,p,x)) = (- ((ProJ (x,y,p)) ")) * (ProJ (p,a,x)) by VECTSP_1:def_8;
then - ((ProJ (p,a,y)) * (ProJ (y,p,x))) = - (- (((ProJ (x,y,p)) ") * (ProJ (p,a,x)))) by VECTSP_1:9;
then - ((ProJ (p,a,y)) * (ProJ (y,p,x))) = ((ProJ (x,y,p)) ") * (ProJ (p,a,x)) by RLVECT_1:17;
then (- (ProJ (p,a,y))) * (ProJ (y,p,x)) = ((ProJ (x,y,p)) ") * (ProJ (p,a,x)) by VECTSP_1:9;
hence (ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x)) by A5, A8, Th25; ::_thesis: verum
end;
now__::_thesis:_(_x__|__implies_(ProJ_(p,a,x))_*_(ProJ_(x,p,y))_=_(-_(ProJ_(p,a,y)))_*_(ProJ_(y,p,x))_)
assume A11: x _|_ ; ::_thesis: (ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))
then ProJ (x,p,y) = 0. F by A5, Th23;
then A12: (ProJ (p,a,x)) * (ProJ (x,p,y)) = 0. F by VECTSP_1:7;
y _|_ by A11, Th2;
then ProJ (y,p,x) = 0. F by A4, Th23;
hence (ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x)) by A12, VECTSP_1:7; ::_thesis: verum
end;
hence (ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x)) by A6; ::_thesis: verum
end;
definition
let F be Field;
let S be SymSp of F;
let x, y, a, b be Element of S;
assume A1: ( not a _|_ & (1_ F) + (1_ F) <> 0. F ) ;
func PProJ (a,b,x,y) -> Element of F means :Def3: :: SYMSP_1:def 3
for q being Element of S st not a _|_ & not x _|_ holds
it = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) if ex p being Element of S st
( not a _|_ & not x _|_ )
otherwise it = 0. F;
existence
( ( ex p being Element of S st
( not a _|_ & not x _|_ ) implies ex b1 being Element of F st
for q being Element of S st not a _|_ & not x _|_ holds
b1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ex b1 being Element of F st b1 = 0. F ) )
proof
thus ( ex p being Element of S st
( not a _|_ & not x _|_ ) implies ex IT being Element of F st
for q being Element of S st not a _|_ & not x _|_ holds
IT = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) ::_thesis: ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ex b1 being Element of F st b1 = 0. F )
proof
given p being Element of S such that A2: ( not a _|_ & not x _|_ ) ; ::_thesis: ex IT being Element of F st
for q being Element of S st not a _|_ & not x _|_ holds
IT = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
take ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) ; ::_thesis: for q being Element of S st not a _|_ & not x _|_ holds
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
let q be Element of S; ::_thesis: ( not a _|_ & not x _|_ implies ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) )
assume ( not a _|_ & not x _|_ ) ; ::_thesis: ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y))
hence ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) by A1, A2, Th30; ::_thesis: verum
end;
thus ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ex b1 being Element of F st b1 = 0. F ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of F holds
( ( ex p being Element of S st
( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds
b1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( for q being Element of S st not a _|_ & not x _|_ holds
b2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies b1 = b2 ) & ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & b1 = 0. F & b2 = 0. F implies b1 = b2 ) )
proof
let IT1, IT2 be Element of F; ::_thesis: ( ( ex p being Element of S st
( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds
IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( for q being Element of S st not a _|_ & not x _|_ holds
IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies IT1 = IT2 ) & ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) )
thus ( ex p being Element of S st
( not a _|_ & not x _|_ ) & ( for q being Element of S st not a _|_ & not x _|_ holds
IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) & ( for q being Element of S st not a _|_ & not x _|_ holds
IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) implies IT1 = IT2 ) ::_thesis: ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 )
proof
given p being Element of S such that A3: ( not a _|_ & not x _|_ ) ; ::_thesis: ( ex q being Element of S st
( not a _|_ & not x _|_ & not IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) or ex q being Element of S st
( not a _|_ & not x _|_ & not IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) or IT1 = IT2 )
consider r being Element of S such that
A4: ( not a _|_ & not x _|_ ) by A3;
assume that
A5: for q being Element of S st not a _|_ & not x _|_ holds
IT1 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) and
A6: for q being Element of S st not a _|_ & not x _|_ holds
IT2 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ; ::_thesis: IT1 = IT2
IT1 = ((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)) by A5, A4;
hence IT1 = IT2 by A6, A4; ::_thesis: verum
end;
thus ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) & IT1 = 0. F & IT2 = 0. F implies IT1 = IT2 ) ; ::_thesis: verum
end;
consistency
for b1 being Element of F holds verum ;
end;
:: deftheorem Def3 defines PProJ SYMSP_1:def_3_:_
for F being Field
for S being SymSp of F
for x, y, a, b being Element of S st not a _|_ & (1_ F) + (1_ F) <> 0. F holds
for b7 being Element of F holds
( ( ex p being Element of S st
( not a _|_ & not x _|_ ) implies ( b7 = PProJ (a,b,x,y) iff for q being Element of S st not a _|_ & not x _|_ holds
b7 = ((ProJ (a,b,q)) * (ProJ (q,a,x))) * (ProJ (x,q,y)) ) ) & ( ( for p being Element of S holds
( a _|_ or x _|_ ) ) implies ( b7 = PProJ (a,b,x,y) iff b7 = 0. F ) ) );
theorem Th32: :: SYMSP_1:32
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F
let S be SymSp of F; ::_thesis: for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ & x = 0. S holds
PProJ (a,b,x,y) = 0. F
let b, a, x, y be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ & x = 0. S implies PProJ (a,b,x,y) = 0. F )
assume that
A1: ( (1_ F) + (1_ F) <> 0. F & not a _|_ ) and
A2: x = 0. S ; ::_thesis: PProJ (a,b,x,y) = 0. F
for p being Element of S holds
( a _|_ or x _|_ ) by A2, Th1, Th2;
hence PProJ (a,b,x,y) = 0. F by A1, Def3; ::_thesis: verum
end;
theorem Th33: :: SYMSP_1:33
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
( PProJ (a,b,x,y) = 0. F iff x _|_ )
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
( PProJ (a,b,x,y) = 0. F iff x _|_ )
let S be SymSp of F; ::_thesis: for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
( PProJ (a,b,x,y) = 0. F iff x _|_ )
let b, a, x, y be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ implies ( PProJ (a,b,x,y) = 0. F iff x _|_ ) )
set 0F = 0. F;
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ ; ::_thesis: ( PProJ (a,b,x,y) = 0. F iff x _|_ )
A3: a <> 0. S by A2, Th1, Th2;
A4: ( PProJ (a,b,x,y) = 0. F implies x _|_ )
proof
assume A5: PProJ (a,b,x,y) = 0. F ; ::_thesis: x _|_
A6: now__::_thesis:_(_ex_p_being_Element_of_S_st_
(_not_a__|__&_not_x__|__)_implies_x__|__)
given p being Element of S such that A7: not a _|_ and
A8: not x _|_ ; ::_thesis: x _|_
A9: now__::_thesis:_not_ProJ_(p,a,x)_=_0._F
assume A10: ProJ (p,a,x) = 0. F ; ::_thesis: contradiction
not p _|_ by A7, Th2;
then p _|_ by A10, Th23;
hence contradiction by A8, Th2; ::_thesis: verum
end;
((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F by A1, A2, A5, A7, A8, Def3;
then ( (ProJ (a,b,p)) * (ProJ (p,a,x)) = 0. F or ProJ (x,p,y) = 0. F ) by VECTSP_1:12;
then ( ProJ (a,b,p) = 0. F or ProJ (p,a,x) = 0. F or ProJ (x,p,y) = 0. F ) by VECTSP_1:12;
hence x _|_ by A2, A7, A8, A9, Th23; ::_thesis: verum
end;
now__::_thesis:_(_(_for_p_being_Element_of_S_holds_
(_a__|__or_x__|__)_)_implies_x__|__)
assume for p being Element of S holds
( a _|_ or x _|_ ) ; ::_thesis: x _|_
then x = 0. S by A3, Th9;
hence x _|_ by Th1, Th2; ::_thesis: verum
end;
hence x _|_ by A6; ::_thesis: verum
end;
( x _|_ implies PProJ (a,b,x,y) = 0. F )
proof
assume A11: x _|_ ; ::_thesis: PProJ (a,b,x,y) = 0. F
A12: now__::_thesis:_(_x_<>_0._S_implies_PProJ_(a,b,x,y)_=_0._F_)
assume x <> 0. S ; ::_thesis: PProJ (a,b,x,y) = 0. F
then consider p being Element of S such that
A13: not a _|_ and
A14: not x _|_ by A3, Th9;
ProJ (x,p,y) = 0. F by A11, A14, Th23;
then ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) = 0. F by VECTSP_1:7;
hence PProJ (a,b,x,y) = 0. F by A1, A2, A13, A14, Def3; ::_thesis: verum
end;
now__::_thesis:_(_x_=_0._S_implies_PProJ_(a,b,x,y)_=_0._F_)
assume x = 0. S ; ::_thesis: PProJ (a,b,x,y) = 0. F
then for p being Element of S holds
( a _|_ or x _|_ ) by Th1, Th2;
hence PProJ (a,b,x,y) = 0. F by A1, A2, Def3; ::_thesis: verum
end;
hence PProJ (a,b,x,y) = 0. F by A12; ::_thesis: verum
end;
hence ( PProJ (a,b,x,y) = 0. F iff x _|_ ) by A4; ::_thesis: verum
end;
theorem :: SYMSP_1:34
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
let S be SymSp of F; ::_thesis: for b, a, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
let b, a, x, y be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ implies PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) )
set 0F = 0. F;
set 1F = 1_ F;
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ ; ::_thesis: PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
A3: now__::_thesis:_(_not_y__|__implies_PProJ_(a,b,x,y)_=_-_(PProJ_(a,b,y,x))_)
assume not y _|_ ; ::_thesis: PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
then A4: ( x <> 0. S & y <> 0. S ) by Th1, Th2;
a <> 0. S by A2, Th1, Th2;
then consider r being Element of S such that
A5: not a _|_ and
A6: not x _|_ and
A7: not y _|_ by A1, A4, Th10;
A8: not r _|_ by A7, Th2;
PProJ (a,b,y,x) = ((ProJ (a,b,r)) * (ProJ (r,a,y))) * (ProJ (y,r,x)) by A1, A2, A5, A7, Def3;
then A9: PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((ProJ (r,a,y)) * (ProJ (y,r,x))) by GROUP_1:def_3;
( not r _|_ & not r _|_ ) by A5, A6, Th2;
then PProJ (a,b,y,x) = (ProJ (a,b,r)) * ((- (ProJ (r,a,x))) * (ProJ (x,r,y))) by A8, A9, Th31;
then PProJ (a,b,y,x) = ((- (ProJ (r,a,x))) * (ProJ (a,b,r))) * (ProJ (x,r,y)) by GROUP_1:def_3;
then PProJ (a,b,y,x) = (- ((ProJ (r,a,x)) * (ProJ (a,b,r)))) * (ProJ (x,r,y)) by VECTSP_1:9;
then (- (1_ F)) * (PProJ (a,b,y,x)) = (- (1_ F)) * (- (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)))) by VECTSP_1:9;
then - ((PProJ (a,b,y,x)) * (1_ F)) = (- (1_ F)) * (- (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)))) by VECTSP_1:9;
then - (PProJ (a,b,y,x)) = (- (1_ F)) * (- (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)))) by VECTSP_1:def_8;
then A10: - (PProJ (a,b,y,x)) = (((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y))) * (1_ F) by VECTSP_1:10;
PProJ (a,b,x,y) = ((ProJ (a,b,r)) * (ProJ (r,a,x))) * (ProJ (x,r,y)) by A1, A2, A5, A6, Def3;
hence PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) by A10, VECTSP_1:def_8; ::_thesis: verum
end;
now__::_thesis:_(_y__|__implies_PProJ_(a,b,x,y)_=_-_(PProJ_(a,b,y,x))_)
assume A11: y _|_ ; ::_thesis: PProJ (a,b,x,y) = - (PProJ (a,b,y,x))
then (- (1_ F)) * (PProJ (a,b,y,x)) = (- (1_ F)) * (0. F) by A1, A2, Th33;
then - ((PProJ (a,b,y,x)) * (1_ F)) = (- (1_ F)) * (0. F) by VECTSP_1:9;
then A12: - (PProJ (a,b,y,x)) = (- (1_ F)) * (0. F) by VECTSP_1:def_8;
x _|_ by A11, Th2;
then PProJ (a,b,x,y) = 0. F by A1, A2, Th33;
hence PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) by A12, VECTSP_1:7; ::_thesis: verum
end;
hence PProJ (a,b,x,y) = - (PProJ (a,b,y,x)) by A3; ::_thesis: verum
end;
theorem :: SYMSP_1:35
for F being Field
for S being SymSp of F
for b, a, x, y being Element of S
for l being Element of F st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x, y being Element of S
for l being Element of F st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
let S be SymSp of F; ::_thesis: for b, a, x, y being Element of S
for l being Element of F st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
let b, a, x, y be Element of S; ::_thesis: for l being Element of F st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
let l be Element of F; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ implies PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) )
set 0F = 0. F;
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ ; ::_thesis: PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
A3: now__::_thesis:_(_not_y__|__implies_PProJ_(a,b,x,(l_*_y))_=_l_*_(PProJ_(a,b,x,y))_)
assume not y _|_ ; ::_thesis: PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
then A4: x <> 0. S by Th1;
a <> 0. S by A2, Th1, Th2;
then consider p being Element of S such that
A5: not a _|_ and
A6: not x _|_ by A4, Th9;
PProJ (a,b,x,(l * y)) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,(l * y))) by A1, A2, A5, A6, Def3;
then A7: PProJ (a,b,x,(l * y)) = (l * (ProJ (x,p,y))) * ((ProJ (a,b,p)) * (ProJ (p,a,x))) by A6, Th15;
PProJ (a,b,x,y) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) by A1, A2, A5, A6, Def3;
hence PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) by A7, GROUP_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_y__|__implies_PProJ_(a,b,x,(l_*_y))_=_l_*_(PProJ_(a,b,x,y))_)
assume A8: y _|_ ; ::_thesis: PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y))
then x _|_ by Th2;
then x _|_ by Def1;
then A9: PProJ (a,b,x,(l * y)) = 0. F by A1, A2, Th33;
x _|_ by A8, Th2;
then l * (PProJ (a,b,x,y)) = l * (0. F) by A1, A2, Th33;
hence PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) by A9, VECTSP_1:7; ::_thesis: verum
end;
hence PProJ (a,b,x,(l * y)) = l * (PProJ (a,b,x,y)) by A3; ::_thesis: verum
end;
theorem :: SYMSP_1:36
for F being Field
for S being SymSp of F
for b, a, x, y, z being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
proof
let F be Field; ::_thesis: for S being SymSp of F
for b, a, x, y, z being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
let S be SymSp of F; ::_thesis: for b, a, x, y, z being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
let b, a, x, y, z be Element of S; ::_thesis: ( (1_ F) + (1_ F) <> 0. F & not a _|_ implies PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) )
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: not a _|_ ; ::_thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
A3: now__::_thesis:_(_x_<>_0._S_implies_PProJ_(a,b,x,(y_+_z))_=_(PProJ_(a,b,x,y))_+_(PProJ_(a,b,x,z))_)
assume A4: x <> 0. S ; ::_thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
a <> 0. S by A2, Th1, Th2;
then consider p being Element of S such that
A5: ( not a _|_ & not x _|_ ) by A4, Th9;
A6: ( PProJ (a,b,x,(y + z)) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,(y + z))) & PProJ (a,b,x,y) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,y)) ) by A1, A2, A5, Def3;
( PProJ (a,b,x,z) = ((ProJ (a,b,p)) * (ProJ (p,a,x))) * (ProJ (x,p,z)) & ProJ (x,p,(y + z)) = (ProJ (x,p,y)) + (ProJ (x,p,z)) ) by A1, A2, A5, Def3, Th16;
hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A6, VECTSP_1:def_7; ::_thesis: verum
end;
set 0F = 0. F;
now__::_thesis:_(_x_=_0._S_implies_PProJ_(a,b,x,(y_+_z))_=_(PProJ_(a,b,x,y))_+_(PProJ_(a,b,x,z))_)
assume A7: x = 0. S ; ::_thesis: PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z))
then A8: PProJ (a,b,x,z) = 0. F by A1, A2, Th32;
( PProJ (a,b,x,(y + z)) = 0. F & PProJ (a,b,x,y) = 0. F ) by A1, A2, A7, Th32;
hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A8, RLVECT_1:4; ::_thesis: verum
end;
hence PProJ (a,b,x,(y + z)) = (PProJ (a,b,x,y)) + (PProJ (a,b,x,z)) by A3; ::_thesis: verum
end;