:: Properties of Fields
:: by J\'ozef Bia{\l}as
::
:: Received June 20, 1990
:: Copyright (c) 1990-2017 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;
definitions RLVECT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_0;
equalities TARSKI, REALSET1, BINOP_1, STRUCT_0, FUNCOP_1, ALGSTR_0, ORDINAL1;
expansions RLVECT_1, TARSKI, MEMBERED, VECTSP_1;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, ENUMSET1, REALSET1, VECTSP_1,
RELSET_1, XBOOLE_0, RLVECT_1, FUNCT_4, FUNCOP_1, CARD_1, XBOOLE_1,
STRUCT_0, GROUP_1, ALGSTR_0, XTUPLE_0, SUBSET_1;
schemes FUNCT_2;
begin
definition
func add_2 -> BinOp of 2 equals
((0,0) .--> 0) +* ((0,1).-->1) +* ((1,0).-->1) +* ((1,1).-->0);
coherence
proof
set f2 = ((0,0).-->0) +* ((0,1).-->1), f1 = f2 +* ((1,0).-->1), f = f1 +*(
(1,1).-->0);
A1: dom f = dom f1 \/ dom((1,1).-->0) by FUNCT_4:def 1
.= dom f1 \/ {[1,1]} by FUNCOP_1:13
.= dom f2 \/ dom((1,0).-->1) \/ {[1,1]} by FUNCT_4:def 1
.= dom f2 \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
.= dom((0,0) .--> 0) \/ dom ((0,1).-->1) \/ {[1,0]} \/ {[1,1]} by
FUNCT_4:def 1
.= dom((0,0) .--> 0) \/ {[0,1]} \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
.= {[0,0]} \/ {[0,1]} \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
.= {[0,0],[0,1]} \/ {[1,0]} \/ {[1,1]} by ENUMSET1:1
.= {[0,0],[0,1],[1,0]} \/ {[1,1]} by ENUMSET1:3
.= {[0,0],[0,1],[1,0],[1,1]} by ENUMSET1:6
.= [:2,2:] by CARD_1:50,ZFMISC_1:122;
A2: 1 c= 2 by CARD_1:49,50,ZFMISC_1:7;
rng ((0,0).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
then
A3: rng ((0,0).-->0) c= 2 by A2;
A4: {1} c= 2 by CARD_1:50,ZFMISC_1:7;
rng ((0,1).-->1) c= {1} by FUNCOP_1:13;
then rng ((0,1).-->1) c= 2 by A4;
then
A5: rng ((0,0).-->0) \/ rng ((0,1).-->1) c= 2 by A3,XBOOLE_1:8;
rng ((1,0).-->1) c= {1} by FUNCOP_1:13;
then
A6: rng ((1,0).-->1) c= 2 by A4;
rng f2 c= rng ((0,0).-->0) \/ rng ((0,1).-->1) by FUNCT_4:17;
then rng f2 c= 2 by A5;
then
A7: rng f2 \/ rng ((1,0).-->1) c= 2 by A6,XBOOLE_1:8;
rng ((1,1).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
then
A8: rng ((1,1).-->0) c= 2 by A2;
rng f1 c= rng f2 \/ rng ((1,0).-->1) by FUNCT_4:17;
then rng f1 c= 2 by A7;
then
A9: rng f1 \/ rng ((1,1).-->0) c= 2 by A8,XBOOLE_1:8;
rng f c= rng f1 \/ rng ((1,1).-->0) by FUNCT_4:17;
then rng f c= 2 by A9;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
func mult_2 -> BinOp of 2 equals
((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0
) +* ((1,1).-->1);
coherence
proof
A10: rng ((1,1).-->1) c= {1} by FUNCOP_1:13;
{1} c= 2 by CARD_1:50,ZFMISC_1:7;
then
A11: rng ((1,1).-->1) c= 2 by A10;
set f2 = ((0,0).-->0) +* ((0,1).-->0), f1 = f2 +* ((1,0).-->0), f = f1 +*
((1,1).-->1);
A12: dom f = dom f1 \/ dom ((1,1).-->1) by FUNCT_4:def 1
.= dom f1 \/ {[1,1]} by FUNCOP_1:13
.= dom f2 \/ dom ((1,0).-->0) \/ {[1,1]} by FUNCT_4:def 1
.= dom f2 \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
.= dom(((0,0).-->0)) \/ dom ((0,1).-->0) \/ {[1,0]} \/ {[1,1]} by
FUNCT_4:def 1
.= dom(((0,0).-->0)) \/ {[0,1]} \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
.= {[0,0]} \/ {[0,1]} \/ {[1,0]} \/ {[1,1]} by FUNCOP_1:13
.= {[0,0],[0,1]} \/ {[1,0]} \/ {[1,1]} by ENUMSET1:1
.= {[0,0],[0,1],[1,0]} \/ {[1,1]} by ENUMSET1:3
.= {[0,0],[0,1],[1,0],[1,1]} by ENUMSET1:6
.= [:2,2:] by CARD_1:50,ZFMISC_1:122;
A13: 1 c= 2 by CARD_1:49,50,ZFMISC_1:7;
rng ((0,0).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
then
A14: rng ((0,0).-->0) c= 2 by A13;
rng ((0,1).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
then rng ((0,1).-->0) c= 2 by A13;
then
A15: rng ((0,0).-->0) \/ rng ((0,1).-->0) c= 2 by A14,XBOOLE_1:8;
rng ((1,0).-->0) c= 1 by CARD_1:49,FUNCOP_1:13;
then
A16: rng ((1,0).-->0) c= 2 by A13;
rng f2 c= rng ((0,0).-->0) \/ rng ((0,1).-->0) by FUNCT_4:17;
then rng f2 c= 2 by A15;
then
A17: rng f2 \/ rng ((1,0).-->0) c= 2 by A16,XBOOLE_1:8;
rng f1 c= rng f2 \/ rng ((1,0).-->0) by FUNCT_4:17;
then rng f1 c= 2 by A17;
then
A18: rng f1 \/ rng ((1,1).-->1) c= 2 by A11,XBOOLE_1:8;
rng f c= rng f1 \/ rng ((1,1).-->1) by FUNCT_4:17;
then rng f c= 2 by A18;
hence thesis by A12,FUNCT_2:def 1,RELSET_1:4;
end;
end;
reserve x,y for set;
:: Properties of fields
set x = In(0,2), y = In(1,2);
Lm1: 1 in 2 by CARD_1:50,TARSKI:def 2;
Lm2: 0 in 2 by CARD_1:50,TARSKI:def 2;
then
Lm3: x = 0 by SUBSET_1:def 8;
Lm4: y = 1 by Lm1,SUBSET_1:def 8;
set Z = 2;
reconsider A = Z as non trivial set by Lm1,Lm2,ZFMISC_1:def 10;
reconsider nd = x as Element of A;
Lm5: dom ((1,1).-->0) = {[1,1]} by FUNCOP_1:13;
Lm6: dom(((1,0).-->1)) = {[1,0]} by FUNCOP_1:13;
Lm7: dom ((0,1).-->1) = {[0,1]} by FUNCOP_1:13;
Lm8: add_2.(x,x) = x
proof
[x,x] <> [0,1] by Lm3,XTUPLE_0:1;
then
A1: not [x,x] in dom ((0,1).-->1) by Lm7,TARSKI:def 1;
[x,x] <> [1,0] by Lm3,XTUPLE_0:1;
then
A2: not [x,x] in dom(((1,0).-->1)) by Lm6,TARSKI:def 1;
[x,x] <> [1,1] by Lm3,XTUPLE_0:1;
then not [x,x] in dom ((1,1).-->0) by Lm5,TARSKI:def 1;
hence add_2.(x,x) = (((0,0).-->0) +* ((0,1).-->1) +* ((1,0).-->1)).(x,x) by
FUNCT_4:11
.= (((0,0).-->0) +* ((0,1).-->1)).(x,x) by A2,FUNCT_4:11
.= (((0,0).-->0)).(x,x) by A1,FUNCT_4:11
.= x by Lm3,FUNCOP_1:71;
end;
Lm9: add_2.(x,y) = y
proof
[x,y] <> [1,0] by Lm3,XTUPLE_0:1;
then
A1: not [x,y] in dom(((1,0).-->1)) by Lm6,TARSKI:def 1;
A2: [x,y] in dom(((0,1).-->1)) by Lm3,Lm4,Lm7,TARSKI:def 1;
[x,y] <> [1,1] by Lm3,XTUPLE_0:1;
then not [x,y] in dom ((1,1).-->0) by Lm5,TARSKI:def 1;
hence add_2.(x,y) = (((0,0).-->0) +* ((0,1).-->1) +* ((1,0).-->1)).(x,y) by
FUNCT_4:11
.= (((0,0).-->0) +* ((0,1).-->1)).(x,y) by A1,FUNCT_4:11
.= (((0,1).-->1)).(x,y) by A2,FUNCT_4:13
.= y by Lm3,Lm4,FUNCOP_1:71;
end;
Lm10: add_2.(y,x) = y
proof
A1: [y,x] in dom(((1,0).-->1)) by Lm3,Lm4,Lm6,TARSKI:def 1;
[y,x] <> [1,1] by Lm3,XTUPLE_0:1;
then not [y,x] in dom ((1,1).-->0) by Lm5,TARSKI:def 1;
hence add_2.(y,x) = (((0,0).-->0) +* ((0,1).-->1) +* ((1,0).-->1)).(y,x) by
FUNCT_4:11
.= (((1,0).-->1)).(y,x) by A1,FUNCT_4:13
.= y by Lm3,Lm4,FUNCOP_1:71;
end;
Lm11: add_2.(y,y) = x
proof
[y,y] in dom ((1,1).-->0) by Lm4,Lm5,TARSKI:def 1;
hence add_2.(y,y) = (((1,1).-->0)).(y,y) by FUNCT_4:13
.= x by Lm3,Lm4,FUNCOP_1:71;
end;
Lm12: dom ((1,1).-->1) = {[1,1]} by FUNCOP_1:13;
Lm13: dom ((1,0).-->0) = {[1,0]} by FUNCOP_1:13;
Lm14: dom ((0,1).-->0) = {[0,1]} by FUNCOP_1:13;
Lm15: mult_2.(x,x) = x
proof
[x,x] <> [0,1] by Lm3,XTUPLE_0:1;
then
A1: not [x,x] in dom ((0,1).-->0) by Lm14,TARSKI:def 1;
[x,x] <> [1,0] by Lm3,XTUPLE_0:1;
then
A2: not [x,x] in dom ((1,0).-->0) by Lm13,TARSKI:def 1;
[x,x] <> [1,1] by Lm3,XTUPLE_0:1;
then not [x,x] in dom ((1,1).-->1) by Lm12,TARSKI:def 1;
hence mult_2.(x,x) = (((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0)).(x,x) by
FUNCT_4:11
.= (((0,0).-->0) +* ((0,1).-->0)).(x,x) by A2,FUNCT_4:11
.= (((0,0).-->0)).(x,x) by A1,FUNCT_4:11
.= x by Lm3,FUNCOP_1:71;
end;
Lm16: mult_2.(x,y) = x
proof
[x,y] <> [1,0] by Lm3,XTUPLE_0:1;
then
A1: not [x,y] in dom ((1,0).-->0) by Lm13,TARSKI:def 1;
A2: [x,y] in dom ((0,1).-->0) by Lm3,Lm4,Lm14,TARSKI:def 1;
[x,y] <> [1,1] by Lm3,XTUPLE_0:1;
then not [x,y] in dom ((1,1).-->1) by Lm12,TARSKI:def 1;
hence mult_2.(x,y) = (((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0)).(x,y) by
FUNCT_4:11
.= (((0,0).-->0) +* ((0,1).-->0)).(x,y) by A1,FUNCT_4:11
.= (((0,1).-->0)).(x,y) by A2,FUNCT_4:13
.= x by Lm3,Lm4,FUNCOP_1:71;
end;
Lm17: mult_2.(y,x) = x
proof
A1: [y,x] in dom ((1,0).-->0) by Lm3,Lm4,Lm13,TARSKI:def 1;
[y,x] <> [1,1] by Lm3,XTUPLE_0:1;
then not [y,x] in dom ((1,1).-->1) by Lm12,TARSKI:def 1;
hence mult_2.(y,x) = (((0,0).-->0) +* ((0,1).-->0) +* ((1,0).-->0)).(y,x) by
FUNCT_4:11
.= (((1,0).-->0)).(y,x) by A1,FUNCT_4:13
.= x by Lm3,Lm4,FUNCOP_1:71;
end;
Lm18: mult_2.(y,y) = y
proof
[y,y] in dom ((1,1).-->1) by Lm4,Lm12,TARSKI:def 1;
hence mult_2.(y,y) = (((1,1).-->1)).(y,y) by FUNCT_4:13
.= y by Lm4,FUNCOP_1:71;
end;
set om = mult_2;
Lm19: A\{x}={y} by Lm3,Lm4,CARD_1:50,ZFMISC_1:17;
then
Lm20: [:A\{x},A\{x}:] = {[y,y]} by ZFMISC_1:29;
Lm21: for t being set holds t in [:A\{x},A\{x}:] implies om.t in A\{x}
proof
let t be set;
assume t in [:A\{x},A\{x}:];
then t=[y,y] by Lm20,TARSKI:def 1;
hence thesis by Lm18,Lm19,TARSKI:def 1;
end;
reconsider nm = y as Element of A\{nd} by Lm19,TARSKI:def 1;
reconsider od0=add_2 as BinOp of A;
reconsider om0=om as BinOp of A;
Lm22: for a,b,d being Element of A holds add_2.(add_2.(a,b),d) = add_2.(a,
add_2.(b,d))
proof
let a,b,d be Element of A;
A1: a = x or a = y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
A2: b = x or b = y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
A3: d = x or d = y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
per cases by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
suppose
a = x;
hence thesis by A2,A3,Lm8,Lm9,Lm10,Lm11;
end;
suppose
b = x;
hence thesis by A1,A3,Lm8,Lm9,Lm10;
end;
suppose
d = x;
hence thesis by A1,A2,Lm8,Lm9,Lm10,Lm11;
end;
suppose
a = y & b = y & d = y;
hence thesis by Lm9,Lm10,Lm11;
end;
end;
reconsider dL=doubleLoopStr(#A,od0,om0,nm,nd#) as non empty doubleLoopStr;
Lm23: for a being Element of dL holds a + 0.dL = a
proof
let a be Element of dL;
a=x or a=y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
hence thesis by Lm8,Lm10;
end;
Lm24: for a,b,c being Element of dL holds a+b+c = a+(b+c) by Lm22;
Lm25: for a,b being Element of dL holds a+b = b+a
proof
let a,b be Element of dL;
a=x & b=x or a=x & b=y or a=y & b=x or a=y & b=y by Lm3,Lm4,CARD_1:50
,TARSKI:def 2;
hence thesis by Lm9,Lm10;
end;
reconsider om1=om as DnT of nd,A by Lm21,REALSET1:def 6;
Lm26: for B being non empty set, P being BinOp of B, e being Element of B st B
= A\{nd} & e = nm holds addLoopStr(#B,P,e#) is AbGroup
proof
let B be non empty set, P be BinOp of B, e be Element of B;
assume that
A1: B = A\{nd} and
A2: e = nm;
A3: addLoopStr(#B,P,e#) is right_complementable
proof
let a be Element of addLoopStr(#B,P,e#);
take a;
thus thesis by A1,A2,Lm19,TARSKI:def 1;
end;
for a,b,c being Element of B holds P.(P.(a,b),c) = P.(a,P.(b,c))
proof
let a,b,c be Element of B;
A4: b = y by A1,Lm19,TARSKI:def 1;
A5: c = y by A1,Lm19,TARSKI:def 1;
a = y by A1,Lm19,TARSKI:def 1;
hence thesis by A1,A4,A5,Lm19,TARSKI:def 1;
end;
then
A6: for a,b,c being Element of addLoopStr(#B,P,e#) holds a+b+c = a+(b+c);
A7: for a,b being Element of addLoopStr(#B,P,e#) holds a+b = b+a
proof
let a,b be Element of addLoopStr(#B,P,e#);
a = y by A1,Lm19,TARSKI:def 1;
hence thesis by A1,Lm19,TARSKI:def 1;
end;
for a being Element of addLoopStr(#B,P,e#) holds a+0.addLoopStr(#B,P,e#) = a
proof
let a be Element of addLoopStr(#B,P,e#);
a = y by A1,Lm19,TARSKI:def 1;
hence thesis by A1,Lm19,TARSKI:def 1;
end;
hence thesis by A3,A6,A7,RLVECT_1:def 2,def 3,def 4;
end;
Lm27: for a,b,d being Element of dL holds a*(b+d) = a*b+a*d & (b+d)*a = b*a+d*
a
proof
let a,b,d be Element of dL;
A1: a=x & b=x & d=x or a=x & b=x & d=y or a=x & b=y & d=x or a=x & b=y & d=y
or a=y & b=x & d=x or a=y & b=x & d=y or a=y & b=y & d=x or a=y & b=y & d=y by
Lm3,Lm4,CARD_1:50,TARSKI:def 2;
hence a*(b+d) = a*b+a*d by Lm8,Lm9,Lm10,Lm11,Lm15,Lm16,Lm17,Lm18;
thus thesis by A1,Lm8,Lm9,Lm10,Lm11,Lm15,Lm16,Lm17,Lm18;
end;
definition
func dL-Z_2 -> doubleLoopStr equals
doubleLoopStr(#2,add_2,mult_2,In(1,2),In(0,2)#);
coherence;
end;
registration
cluster dL-Z_2 -> strict non empty non degenerated;
coherence
proof
thus dL-Z_2 is strict;
thus the carrier of dL-Z_2 is non empty;
0 in 2 by CARD_1:50,TARSKI:def 2;
then
A1: 0.dL-Z_2 = 0 by SUBSET_1:def 8;
1 in 2 by CARD_1:50,TARSKI:def 2;
hence 0.dL-Z_2 <> 1.dL-Z_2 by A1,SUBSET_1:def 8;
end;
end;
registration
cluster dL-Z_2 -> add-associative distributive;
coherence
proof
for a,b,c being Element of dL-Z_2 holds a+b+c = a+(b+c) by Lm22;
hence dL-Z_2 is add-associative;
thus dL-Z_2 is distributive
proof
let a,b,d be Element of dL-Z_2;
A1: a=x & b=x & d=x or a=x & b=x & d=y or a=x & b=y & d=x or a=x & b=y &
d=y or a=y & b=x & d=x or a=y & b=x & d=y or a=y & b=y & d=x or a=y & b=y & d=y
by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
hence a*(b+d) = a*b+a*d by Lm8,Lm9,Lm10,Lm11,Lm15,Lm16,Lm17,Lm18;
thus thesis by A1,Lm8,Lm9,Lm10,Lm11,Lm15,Lm16,Lm17,Lm18;
end;
end;
end;
registration
cluster add-associative for non trivial strict doubleLoopStr;
existence
proof
take dL-Z_2;
thus thesis;
end;
end;
registration
cluster the carrier of dL-Z_2 -> natural-membered;
coherence
by CARD_1:50,TARSKI:def 2;
end;
registration
cluster empty for Element of dL-Z_2;
existence
proof
reconsider z = 0 as Element of dL-Z_2 by CARD_1:50,TARSKI:def 2;
take z;
thus thesis;
end;
cluster non empty for Element of dL-Z_2;
existence
proof
reconsider z = 1 as Element of dL-Z_2 by CARD_1:50,TARSKI:def 2;
take z;
thus thesis;
end;
end;
definition
let L be doubleLoopStr;
attr L is Field-like means
:Def4:
the multF of L is DnT of 0.L,the carrier
of L & 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;
coherence;
end;
Lm28: for
B being non empty set, P being BinOp of B, e being Element of B st B =
A\{nd} & e = nm & P = om1!(A,nd) holds addLoopStr(#B,P,e#) is AbGroup by Lm26;
registration
cluster strict Field-like Abelian distributive add-associative right_zeroed
right_complementable for non degenerated doubleLoopStr;
existence
proof
set L = doubleLoopStr(#A,od0,om0,nm,nd#);
A1: 0.L = nd;
1.L = nm;
then reconsider L as non degenerated doubleLoopStr by A1,Lm3,Lm4,
STRUCT_0:def 8;
take L;
thus L is strict;
thus the multF of L is DnT of 0.L,the carrier of L by Lm28;
L is right_complementable
proof
let a be Element of L;
take a;
a=x or a=y by Lm3,Lm4,CARD_1:50,TARSKI:def 2;
hence thesis by Lm8,Lm11;
end;
hence thesis by Lm23,Lm24,Lm25,Lm26,Lm27;
end;
end;
registration
cluster add-associative right_zeroed right_complementable Abelian
commutative associative well-unital distributive almost_left_invertible ->
Field-like for non degenerated doubleLoopStr;
coherence
proof
let L be non degenerated doubleLoopStr;
set B = NonZero L;
assume
A1: L is add-associative right_zeroed right_complementable Abelian
commutative associative well-unital distributive almost_left_invertible;
A2: for y being set st y in [:B,B:] holds (the multF of L).y in B
proof
let z be set;
assume z in [:B,B:];
then consider x,y being object such that
A3: x in B and
A4: y in B and
A5: z = [x,y] by ZFMISC_1:84;
reconsider x,y as Element of L by A3,A4;
not y in {0.L} by A4,XBOOLE_0:def 5;
then
A6: y <> 0.L by TARSKI:def 1;
not x in {0.L} by A3,XBOOLE_0:def 5;
then x <> 0.L by TARSKI:def 1;
then x*y <> 0.L by A1,A6,VECTSP_1:12;
then not x*y in {0.L} by TARSKI:def 1;
hence thesis by A5,XBOOLE_0:def 5;
end;
hence the multF of L is DnT of 0.L,the carrier of L by REALSET1:def 6;
reconsider om = the multF of L as DnT of 0.L,the carrier of L by A2,
REALSET1:def 6;
let B be non empty set, P be BinOp of B, e be Element of B such that
A7: B = NonZero L and
A8: e = 1.L and
A9: P = (the multF of L)||NonZero L;
set K = addLoopStr(#B,P,e#);
A10: K is Abelian
proof
let v,w be Element of K;
reconsider a=v, b=w as Element of L by A7,XBOOLE_0:def 5;
A11: [w,v] in [:B,B:];
[v,w] in [:B,B:];
hence v + w = a*b by A7,A9,FUNCT_1:49
.= b*a by A1,GROUP_1:def 12
.= w + v by A7,A9,A11,FUNCT_1:49;
end;
A12: K is right_complementable
proof
let v be Element of K;
reconsider a=v as Element of L by A7,XBOOLE_0:def 5;
not a in {0.L} by A7,XBOOLE_0:def 5;
then a <> 0.L by TARSKI:def 1;
then consider b being Element of L such that
A13: b*a = 1.L by A1;
A14: a*b = 1.L by A1,A13,GROUP_1:def 12;
then b <> 0.L by A1,VECTSP_1:6;
then not b in {0.L} by TARSKI:def 1;
then reconsider w=b as Element of K by A7,XBOOLE_0:def 5;
take w;
[v,w] in [:B,B:];
hence thesis by A7,A8,A9,A14,FUNCT_1:49;
end;
A15: K is add-associative
proof
let u,v,w be Element of K;
reconsider a=u, b=v, c =w as Element of L by A7,XBOOLE_0:def 5;
A16: [v,w] in [:B,B:];
then P.(v,w) in B by FUNCT_2:5;
then
A17: [u,(om||B).(v,w)] in [:B,B:] by A7,A9,ZFMISC_1:87;
A18: [u,v] in [:B,B:];
then P.(u,v) in B by FUNCT_2:5;
then [(om||B).(u,v),w] in [:B,B:] by A7,A9,ZFMISC_1:87;
hence (u + v) + w = om.((om||B).(u,v),w) by A7,A9,FUNCT_1:49
.= (a*b)*c by A18,FUNCT_1:49
.= a*(b*c) by A1,GROUP_1:def 3
.= om.(u,(om||B).(v,w)) by A16,FUNCT_1:49
.= u + (v + w) by A7,A9,A17,FUNCT_1:49;
end;
K is right_zeroed
proof
let v be Element of K;
reconsider a=v as Element of L by A7,XBOOLE_0:def 5;
[v,0.K] in [:B,B:];
hence v + 0.K = a*1.L by A7,A8,A9,FUNCT_1:49
.= v by A1;
end;
hence thesis by A10,A15,A12;
end;
end;
deffunc suppf1(Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr) = the carrier of $1;
definition
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr;
func omf(F) -> DnT of 0.F,the carrier of F equals
the multF of F;
coherence by Def4;
end;
theorem
for F being Field holds the addLoopStr of F is AbGroup
proof
let F be Field;
set L = the addLoopStr of F;
A1: L is add-associative
proof
let u,v,w being Element of L;
reconsider a=u, b=v, c = w as Element of F;
thus (u + v) + w = (a + b) + c .= a + (b + c) by RLVECT_1:def 3
.= u + (v + w);
end;
A2: L is right_zeroed
proof
let v be Element of L;
reconsider a=v as Element of F;
thus v + 0.L = a + 0.F .= v;
end;
A3: L is right_complementable
proof
let v be Element of L;
reconsider a=v as Element of F;
consider b being Element of F such that
A4: a + b = 0.F by ALGSTR_0:def 11;
reconsider w=b as Element of L;
take w;
thus thesis by A4;
end;
L is Abelian
proof
let v,w be Element of L;
reconsider a=v, b=w as Element of F;
thus v + w = a + b .= b + a
.= w + v;
end;
hence thesis by A1,A2,A3;
end;
theorem
for F being Field, a being Element of F holds a+0.F = a & 0.F+a = a;
theorem Th3:
for F being AbGroup, a being Element of F ex b being Element of F
st a+b = 0.F & b+a = 0.F
proof
let F be AbGroup, a be Element of F;
consider b being Element of F such that
A1: a+b = 0.F by ALGSTR_0:def 11;
take b;
thus a+b = 0.F by A1;
thus thesis by A1;
end;
theorem Th4:
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)
proof
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a,b,c be Element of
NonZero F;
set B = suppf1(F)\{0.F};
set P = omf(F)!(suppf1(F),0.F);
A1: B = NonZero F;
then reconsider e = 1.F as Element of B by STRUCT_0:2;
reconsider D = addLoopStr(#B,P,e#) as strict AbGroup by A1,Def4;
reconsider a,b,c as Element of D;
reconsider x=a, y=b, z=c as Element of F;
A2: omf(F)||(suppf1(F)\{0.F}) is Function of [:suppf1(F)\{0.F},suppf1(F)\{0.
F}:], (suppf1(F)\{0.F}) by REALSET1:7;
then
A3: dom(omf(F)||(suppf1(F)\{0.F})) = [:suppf1(F)\{0.F},suppf1(F)\{0.F}:] by
FUNCT_2:def 1;
A4: for x,y being Element of suppf1(F)\{0.F} holds omf(F).(x,y) = (the addF
of D).(x,y)
proof
let x,y be Element of suppf1(F)\{0.F};
[x,y] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
hence thesis by A3,FUNCT_1:47;
end;
A5: for s,t being Element of (suppf1(F)\{0.F}) holds (the addF of D).(s,t)
is Element of (suppf1(F)\{0.F}) & omf(F).(s,t) is Element of (suppf1(F)\{0.F})
proof
let s,t be Element of (suppf1(F)\{0.F});
A6: [s,t] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
consider W being Function of [:suppf1(F)\{0.F},suppf1(F)\{0.F}:], (suppf1(
F)\{0.F}) such that
A7: W = omf(F)||(suppf1(F)\{0.F}) by A2;
W.(s,t) is Element of (suppf1(F)\{0.F});
hence thesis by A3,A6,A7,FUNCT_1:47;
end;
A8: for x,y,z being Element of suppf1(F)\{0.F} holds omf(F).((the addF of D
).(x,y),z) = (the addF of D).((the addF of D).(x,y),z) & (the addF of D).(x,omf
(F).(y,z)) = omf(F).(x,omf(F).(y,z))
proof
let x,y,z be Element of suppf1(F)\{0.F};
A9: omf(F).(y,z) is Element of suppf1(F)\{0.F} by A5;
(the addF of D).(x,y) is Element of suppf1(F)\{0.F} by A5;
hence thesis by A4,A9;
end;
(x*y)*z = omf(F).((the addF of D).(a,b),c) by A4
.= a+b+c by A8
.= a+(b+c) by RLVECT_1:def 3
.= (the addF of D).(a,omf(F).(b,c)) by A4
.= x*(y*z) by A8;
hence thesis;
end;
theorem Th5:
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
proof
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a,b be Element of NonZero
F;
set B = suppf1(F)\{0.F};
set P = omf(F)!(suppf1(F),0.F);
A1: B = NonZero F;
then reconsider e = 1.F as Element of B by STRUCT_0:2;
reconsider D = addLoopStr(#B,P,e#) as strict AbGroup by A1,Def4;
reconsider a,b as Element of D;
reconsider x = a, y = b as Element of F;
omf(F)||(suppf1(F)\{0.F}) is Function of [:suppf1(F)\{0.F},suppf1(F)\{0.
F}:], (suppf1(F)\{0.F}) by REALSET1:7;
then
A2: dom(omf(F)||(suppf1(F)\{0.F})) = [:suppf1(F)\{0.F},suppf1(F)\{0.F}:] by
FUNCT_2:def 1;
A3: for x,y being Element of suppf1(F)\{0.F} holds omf(F).(x,y) = (the addF
of D).(x,y)
proof
let x,y be Element of suppf1(F)\{0.F};
[x,y] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
hence thesis by A2,FUNCT_1:47;
end;
then x*y = a+b .= b+a
.= y*x by A3;
hence thesis;
end;
theorem Th6:
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
proof
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a be Element of NonZero F;
set B = suppf1(F)\{0.F};
set P = omf(F)!(suppf1(F),0.F);
A1: B = NonZero F;
then reconsider e = 1.F as Element of B by STRUCT_0:2;
reconsider D = addLoopStr(#B,P,e#) as strict AbGroup by A1,Def4;
reconsider a as Element of D;
omf(F)||(suppf1(F)\{0.F}) is Function of [:suppf1(F)\{0.F},suppf1(F)\{0.
F}:], (suppf1(F)\{0.F}) by REALSET1:7;
then
A2: dom(omf(F)||(suppf1(F)\{0.F})) = [:suppf1(F)\{0.F},suppf1(F)\{0.F}:] by
FUNCT_2:def 1;
A3: for x,y being Element of suppf1(F)\{0.F} holds omf(F).(x,y) = (the addF
of D).(x,y)
proof
let x,y be Element of suppf1(F)\{0.F};
[x,y] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
hence thesis by A2,FUNCT_1:47;
end;
then
A4: omf(F).(1.F,a) = 0.D + a .= a;
omf(F).(a,1.F) = a + 0.D by A3
.= a;
hence thesis by A4;
end;
theorem Th7:
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
proof
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a be Element of NonZero F;
set B = suppf1(F)\{0.F};
set P = omf(F)!(suppf1(F),0.F);
A1: B = NonZero F;
then reconsider e = 1.F as Element of B by STRUCT_0:2;
addLoopStr(#B,P,e#) is AbGroup by A1,Def4;
then consider D being strict AbGroup such that
A2: D = addLoopStr(#B,P,e#);
reconsider a as Element of D by A2;
consider b being Element of D such that
A3: a+b = 0.D and
A4: b+a = 0.D by Th3;
reconsider b as Element of NonZero F by A2;
take b;
omf(F)||(suppf1(F)\{0.F}) is Function of [:suppf1(F)\{0.F},suppf1(F)\{0.
F}:], (suppf1(F)\{0.F}) by REALSET1:7;
then
A5: dom(omf(F)||(suppf1(F)\{0.F})) = [:suppf1(F)\{0.F},suppf1(F)\{0.F}:] by
FUNCT_2:def 1;
for x,y being Element of suppf1(F)\{0.F} holds omf(F).(x,y) = (the addF
of D).(x,y)
proof
let x,y be Element of suppf1(F)\{0.F};
[x,y] in [:suppf1(F)\{0.F},suppf1(F)\{0.F}:];
hence thesis by A2,A5,FUNCT_1:47;
end;
hence thesis by A2,A3,A4;
end;
theorem
for F being Field, x,y being Element of F holds x+y = 0.F implies y =
(comp F).x
proof
let F be Field, x,y be Element of F;
assume x+y = 0.F;
then y = -x by RLVECT_1:6;
hence thesis by VECTSP_1:def 13;
end;
theorem
for F being Field, x being Element of F holds x = (comp F).((comp F).x )
proof
let F be Field, x be Element of F;
thus x = --x
.= (comp F).-x by VECTSP_1:def 13
.= (comp F).((comp F).x) by VECTSP_1:def 13;
end;
theorem
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
for F being Field, a,b,c being Element of F holds a*(b-c) = a*b-a*c by
VECTSP_1:11;
theorem
for F being Field, a,b,c being Element of F holds (a-b)*c = a*c-b*c by
VECTSP_1:13;
theorem
for F being Field, a being Element of F holds a*0.F = 0.F;
theorem
for F being Field, a being Element of F holds 0.F*a = 0.F;
theorem
for F being Field, a,b being Element of F holds -(a*b) = a*-b by VECTSP_1:8;
theorem
for F being Field holds 1.F*0.F = 0.F;
theorem
for F being Field holds 0.F*1.F = 0.F;
theorem
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 Th19:
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)
proof
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a,b,c be Element of
suppf1(F);
a = 0.F or b = 0.F or c = 0.F or a is Element of NonZero F & b is
Element of NonZero F & c is Element of NonZero F by ZFMISC_1:56;
hence thesis by Th4;
end;
theorem Th20:
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
proof
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a,b be Element of suppf1(
F);
a = 0.F or b = 0.F or a is Element of NonZero F & b is Element of
NonZero F by ZFMISC_1:56;
hence thesis by Th5;
end;
theorem Th21:
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
proof
let F be Field-like Abelian distributive add-associative right_zeroed
right_complementable non degenerated doubleLoopStr, a be Element of suppf1(F);
per cases by ZFMISC_1:56;
suppose
A1: a = 0.F;
hence a*1.F = a;
thus thesis by A1;
end;
suppose
a is Element of NonZero F;
hence thesis by Th6;
end;
end;
definition
let F be Field;
func revf(F) -> UnOp of NonZero F means
:Def6:
for x being Element of NonZero F holds omf(F).(x,it.x) = 1.F;
existence
proof
defpred Z[object,object] means omf(F).($1,$2) = 1.F;
A1: for x being object st x in suppf1(F)\{0.F}
ex y being object st y in suppf1(F)\{0.F} & Z[x,y]
proof
let x be object;
assume x in suppf1(F)\{0.F};
then reconsider x as Element of NonZero F;
consider y being Element of suppf1(F)\{0.F} such that
A2: x*y = 1.F and
y*x = 1.F by Th7;
reconsider y as set;
take y;
thus thesis by A2;
end;
ex C being Function of suppf1(F)\{0.F},suppf1(F)\{0.F} st for x being
object st x in suppf1(F)\{0.F} holds Z[x,C.x] from FUNCT_2:sch 1 (A1);
then consider C being UnOp of NonZero F such that
A3: for x being object st x in suppf1(F)\{0.F} holds omf(F).(x,C.x) = 1.F;
take C;
thus thesis by A3;
end;
uniqueness
proof
let C1,C2 be UnOp of NonZero F such that
A4: for x being Element of NonZero F holds omf(F).(x,C1.x) = 1.F and
A5: for x being Element of NonZero F holds omf(F).(x,C2.x) = 1.F;
for x being object st x in suppf1(F)\{0.F} holds C1.x = C2.x
proof
let x be object;
assume
A6: x in suppf1(F)\{0.F};
then
A7: C1.x is Element of NonZero F by FUNCT_2:5;
then reconsider a=x, C1a = C1.x as Element of F by A6;
A8: C2.x is Element of NonZero F by A6,FUNCT_2:5;
then reconsider C2a = C2.x as Element of F;
C1.x = (C1a)*1.F
.= C1a*(a*C2a) by A5,A6
.= (a*C1a)*C2a by A6,A7,A8,Th4
.= 1.F*(C2a) by A4,A6
.= C2.x;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem
for F being Field, x,y being Element of NonZero F holds x*y = 1.F
implies y = revf(F).x
proof
let F be Field, x,y be Element of NonZero F;
assume
A1: x*y = 1.F;
reconsider rx = revf(F).x as Element of F by XBOOLE_0:def 5;
y = y*1.F
.= omf(F).(y,1.F)
.= y*(x*rx) by Def6
.= 1.F*rx by A1,Th4
.= revf(F).x;
hence thesis;
end;
theorem
for F being Field, x being Element of NonZero F holds x =revf(F).(revf (F).x)
proof
let F be Field, x be Element of NonZero F;
reconsider rx = revf(F).x as Element of F by XBOOLE_0:def 5;
reconsider rrx = revf(F).(revf(F).x) as Element of F by XBOOLE_0:def 5;
x =x*1.F
.= omf(F).(x,1.F)
.= x*(rx*rrx) by Def6
.= x*rx*rrx by Th4
.= omf(F).(1.F,revf(F).(revf(F).x)) by Def6
.= 1.F*rrx
.= revf(F).(revf(F).x);
hence thesis;
end;
theorem
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
proof
let F be Field, a,b be Element of NonZero F;
[a,b] in [:NonZero F,NonZero F:];
hence thesis by REALSET1:def 6;
end;
theorem
for F being Field, a,b,c being Element of F holds a+b = a+c implies b
= c by RLVECT_1:8;
theorem
for F being Field, a being Element of NonZero F, b,c being Element of
(the carrier of F)holds a*b = a*c implies b = c
proof
let F be Field, a be Element of NonZero F, b,c be Element of suppf1(F);
reconsider x=a as Element of F;
assume
A1: a*b = a*c;
reconsider ra = revf(F).a as Element of F by XBOOLE_0:def 5;
b = 1.F*b
.= omf(F).(1.F,b)
.= (x*ra)*b by Def6
.= ra*(x*c) by A1,Th19
.= (x*ra)*c by Th19
.= omf(F).(1.F,c) by Def6
.= 1.F*c
.= c;
hence thesis;
end;
registration
cluster Field-like Abelian distributive add-associative right_zeroed
right_complementable -> commutative associative well-unital
almost_left_invertible for non degenerated doubleLoopStr;
coherence
proof
let L be non degenerated doubleLoopStr;
assume
A1: L is Field-like Abelian distributive add-associative right_zeroed
right_complementable;
then for x,y being Element of L holds x*y = y*x by Th20;
hence L is commutative by GROUP_1:def 12;
for x,y,z being Element of L holds (x*y)*z = x*(y*z) by A1,Th19;
hence L is associative by GROUP_1:def 3;
for x being Element of L holds x * 1.L = x & 1.L * x = x by A1,Th21;
hence L is well-unital;
let x being Element of L;
assume x <> 0.L;
then not x in {0.L} by TARSKI:def 1;
then reconsider x as Element of NonZero L by XBOOLE_0:def 5;
consider y being Element of NonZero L such that
x*y = 1.L and
A2: y*x = 1.L by A1,Th7;
take y;
thus thesis by A2;
end;
end;