:: Properties of Fields :: by J\'ozef Bia{\l}as :: :: Received June 20, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies BINOP_1, CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, FUNCT_7, SUBSET_1, FUNCT_1, ALGSTR_0, ARYTM_3, SUPINF_2, REALSET1, VECTSP_1, STRUCT_0, MESFUNC1, RLVECT_1, LATTICES, ARYTM_1, REALSET2, MEMBERED; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, REALSET1, FUNCOP_1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_7, MEMBERED, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1; constructors RLVECT_1, BINOP_1, FUNCT_4, REALSET1, FUNCT_7, VECTSP_1, RELSET_1, MEMBERED, GROUP_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, STRUCT_0, RLVECT_1, VECTSP_1, ORDINAL1, ALGSTR_0, ZFMISC_1, CARD_1; requirements SUBSET, BOOLE, NUMERALS; begin definition func add_2 -> BinOp of 2 equals :: REALSET2:def 1 ((0,0) .--> 0) +* ((0,1).-->1) +* ((1,0).-->1) +* ((1,1).-->0); func mult_2 -> BinOp of 2 equals :: REALSET2:def 2 ((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0) +* ((1,1).-->1); end; reserve x,y for set; definition func dL-Z_2 -> doubleLoopStr equals :: REALSET2:def 3 doubleLoopStr(#2,add_2,mult_2,In(1,2),In(0,2)#); end; registration cluster dL-Z_2 -> strict non empty non degenerated; end; registration cluster dL-Z_2 -> add-associative distributive; end; registration cluster add-associative for non trivial strict doubleLoopStr; end; registration cluster the carrier of dL-Z_2 -> natural-membered; end; registration cluster empty for Element of dL-Z_2; cluster non empty for Element of dL-Z_2; end; definition let L be doubleLoopStr; attr L is Field-like means :: REALSET2:def 4 the multF of L is ((the carrier of L)\{0.L})-subsetpreserving & for B being non empty set, P being BinOp of B, e being Element of B holds B = NonZero L & e = 1.L & P = (the multF of L)||NonZero L implies addLoopStr(#B,P,e#) is AbGroup; end; registration let A be non empty set, od be BinOp of A, nd be Element of A, om be BinOp of A, nm be Element of A; cluster doubleLoopStr(#A,od,om,nm,nd#) -> non empty; end; registration cluster strict Field-like Abelian distributive add-associative right_zeroed right_complementable for non degenerated doubleLoopStr; end; registration cluster add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible -> Field-like for non degenerated doubleLoopStr; end; definition let F be Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr; func omf(F) -> ((the carrier of F) \ {0.F})-subsetpreserving BinOp of F equals :: REALSET2:def 5 the multF of F; end; theorem :: REALSET2:1 for F being Field holds the addLoopStr of F is AbGroup; theorem :: REALSET2:2 for F being Field, a being Element of F holds a+0.F = a & 0.F+a = a; theorem :: REALSET2:3 for F being AbGroup, a being Element of F ex b being Element of F st a+b = 0.F & b+a = 0.F; theorem :: REALSET2:4 for F being Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b,c being Element of NonZero F holds (a*b)*c = a*(b*c); theorem :: REALSET2:5 for F being Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b being Element of NonZero F holds a*b = b*a; theorem :: REALSET2:6 for F being Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a being Element of NonZero F holds a*1.F = a & 1.F*a = a; theorem :: REALSET2:7 for F being Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a being Element of NonZero F ex b being Element of NonZero F st a*b = 1.F & b*a = 1.F ; theorem :: REALSET2:8 for F being Field, x,y being Element of F holds x+y = 0.F implies y = (comp F).x; theorem :: REALSET2:9 for F being Field, x being Element of F holds x = (comp F).((comp F).x ); theorem :: REALSET2:10 for F being Field, a,b being Element of (the carrier of F)holds (the addF of F).(a,b) is Element of (the carrier of F)& omf(F).(a,b) is Element of ( the carrier of F)& (comp F).a is Element of the carrier of F; theorem :: REALSET2:11 for F being Field, a,b,c being Element of F holds a*(b-c) = a*b-a*c; theorem :: REALSET2:12 for F being Field, a,b,c being Element of F holds (a-b)*c = a*c-b*c; theorem :: REALSET2:13 for F being Field, a being Element of F holds a*0.F = 0.F; theorem :: REALSET2:14 for F being Field, a being Element of F holds 0.F*a = 0.F; theorem :: REALSET2:15 for F being Field, a,b being Element of F holds -(a*b) = a*-b; theorem :: REALSET2:16 for F being Field holds 1.F*0.F = 0.F; theorem :: REALSET2:17 for F being Field holds 0.F*1.F = 0.F; theorem :: REALSET2:18 for F being Field, a,b being Element of (the carrier of F)holds omf(F) .(a,b) is Element of the carrier of F; theorem :: REALSET2:19 for F being Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b,c being Element of F holds (a*b)*c = a*(b*c); theorem :: REALSET2:20 for F being Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a,b being Element of F holds a*b = b*a; theorem :: REALSET2:21 for F being Field-like Abelian distributive add-associative right_zeroed right_complementable non degenerated doubleLoopStr, a being Element of F holds a*1.F = a & 1.F*a = a; definition let F be Field; func revf(F) -> UnOp of NonZero F means :: REALSET2:def 6 for x being Element of NonZero F holds omf(F).(x,it.x) = 1.F; end; theorem :: REALSET2:22 for F being Field, x,y being Element of NonZero F holds x*y = 1.F implies y = revf(F).x; theorem :: REALSET2:23 for F being Field, x being Element of NonZero F holds x =revf(F).(revf (F).x) ; theorem :: REALSET2:24 for F being Field, a,b being Element of NonZero F holds omf(F).(a,b) is Element of NonZero F & revf(F).a is Element of NonZero F; theorem :: REALSET2:25 for F being Field, a,b,c being Element of F holds a+b = a+c implies b = c; theorem :: REALSET2:26 for F being Field, a being Element of NonZero F, b,c being Element of F holds a*b = a*c implies b = c; registration cluster Field-like Abelian distributive add-associative right_zeroed right_complementable -> commutative associative well-unital almost_left_invertible for non degenerated doubleLoopStr; end;