:: 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;