:: On the Intersection of Fields $F$ with $F[X]$
:: by Christoph Schwarzweller
::
:: Received August 29, 2019
:: Copyright (c) 2019-2026 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 VECTSP_1, ALGSTR_0, STRUCT_0, SUBSET_1, SUPINF_2, BINOP_1,
CARD_1, MESFUNC1, POLYNOM1, FUNCSDOM, HURWITZ, RLVECT_1, FINSEQ_1,
FUNCT_1, RELAT_1, XBOOLE_0, NUMBERS, AFINSQ_1, ARYTM_1, IDEAL_1, RAT_1,
ARYTM_3, GROUP_2, XXREAL_0, QUOFIELD, ZFMISC_1, PARTFUN1, TARSKI,
EQREL_1, BINOP_2, INT_3, MOD_4, MCART_1, RING_3, WELLORD1, GROUP_1,
NAT_1, INT_1, FDIFF_1, ORDINAL1, FUNCT_2, MSSUBFAM, FUNCT_7, XCMPLX_0,
FINSET_1, ALGSEQ_1, POLYNOM3, REAL_1, LATTICES, PREFER_1, CLASSES1,
GAUSSINT, WAYBEL20, ARYTM_2, FIELD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, CLASSES1,
RELSET_1, FUNCT_1, FUNCT_2, NUMBERS, PARTFUN1, XTUPLE_0, RAT_1, XCMPLX_0,
XXREAL_0, XREAL_0, ARYTM_2, ARYTM_3, BINOP_1, STRUCT_0, NAT_1, INT_1,
GR_CY_1, INT_3, GAUSSINT, POLYNOM3, POLYNOM5, ALGSEQ_1, GROUP_1, GROUP_6,
ALGSTR_0, IDEAL_1, EQREL_1, RLVECT_1, HURWITZ, VECTSP_1, RINGCAT1, MOD_4,
RING_1, RING_3, RING_4;
constructors HURWITZ, XBOOLE_0, RELSET_1, ARYTM_3, ABIAN, QUOFIELD, PARTFUN1,
RLVECT_1, FUNCT_7, FINSET_1, GAUSSINT, ALGSEQ_1, RATFUNC1, GROUP_6,
RAT_1, BINOP_2, CLASSES1, REALSET1, ALGSTR_2, INT_3, RINGCAT1, MEMBERED,
MOD_4, GR_CY_1, NAT_D, IDEAL_1, EQREL_1, ARYTM_2, RLVECT_5, RING_1,
RING_3, RING_4, GROUP_4, CARD_2, POLYNOM1, ORDINAL2, INT_1, POLYNOM5;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, CARD_2, NAT_1, INT_1,
MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, FUNCT_2, XREAL_0, ALGSTR_0,
RING_1, RLVECT_1, PARTFUN1, RATFUNC1, XTUPLE_0, FINSET_1, GAUSSINT,
POLYNOM4, INT_3, CARD_1, RING_2, RING_3, RING_4, RING_5, POLYNOM1,
POLYNOM3, RINGCAT1, SUBSET_1, POLYNOM5, RAT_1;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities STRUCT_0, ALGSTR_0, ARYTM_3, VECTSP_1;
expansions VECTSP_1, TARSKI, FUNCT_1, FUNCT_2, GROUP_1;
theorems VECTSP_1, FUNCT_2, TARSKI, FUNCT_1, RATFUNC1, POLYNOM5, RING_4,
HURWITZ, XBOOLE_0, POLYNOM3, NAT_1, ZFMISC_1, BINOP_1, EQREL_1, RING_1,
QUOFIELD, VECTSP_2, GROUP_1, ORDINAL1, CARD_1, INT_3, RING_2, MOD_4,
GR_CY_1, SUBSET_1, INT_1, PEPIN, ARYTM_2, GROUP_6, CARD_2, ALGSEQ_1,
NUMBERS, ALGSTR_0, CLASSES1, STRUCT_0, ARYTM_3, RAT_1, NAT_2, RLVECT_1,
XTUPLE_0, XREAL_0, RELAT_1, GAUSSINT, AXIOMS;
schemes NAT_1, BINOP_1, FUNCT_2;
begin :: Preliminaries
Th1:
for n being Nat holds n = { m where m is Nat : m < n } by AXIOMS:4;
theorem
for n being Nat, x being object st n = {x} holds x = 0
proof
let n be Nat, x be object;
assume
A1: n = {x}; then
card n = 1 by CARD_1:30; then
x in {0} by A1,CARD_1:49,TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem Th3:
for n being Nat, x,y being object st n = {x,y} & x <> y
holds (x = 0 & y = 1) or (x = 1 & y = 0)
proof
let n be Nat, x,y be object;
assume
A1: n = {x,y} & x <> y; then
card n = 2 by CARD_2:57; then
A2: x in {0,1} & y in {0,1} by A1,CARD_1:50,TARSKI:def 2;
per cases by A2,TARSKI:def 2;
suppose x = 0;
hence thesis by A1,A2,TARSKI:def 2;
end;
suppose x = 1;
hence thesis by A1,A2,TARSKI:def 2;
end;
end;
theorem Th4:
for n being Nat st 1 < n holds 0.(Z/n) = 0
proof
let n be Nat;
Z/n = doubleLoopStr(#Segm(n),addint(n),multint(n),In(1,Segm(n)),
In(0,Segm(n))#) by INT_3:def 12;
hence thesis by NAT_1:44,SUBSET_1:def 8;
end;
theorem Th5:
1.(Z/2) + 1.(Z/2) = 0.(Z/2)
proof
A1: Z/2 =
doubleLoopStr(#Segm(2),addint(2),multint(2),In(1,Segm(2)), In(0,Segm(2))#)
by INT_3:def 12;
1.(Z/2) = 1 by INT_3:14;
hence 1.(Z/2) + 1.(Z/2) = (1+1) mod 2 by A1,GR_CY_1:def 4
.= 0 by INT_1:50 .= 0.(Z/2) by Th4;
end;
theorem Th6:
for R being Ring, n being non zero Nat holds power(R).(0.R,n) = 0.R
proof
let R be Ring, n be non zero Nat;
defpred P[Nat] means power(R).(0.R,$1) = 0.R;
power(R).(0.R,0+1) = power(R).(0.R,0) * 0.R by GROUP_1:def 7 .= 0.R; then
A1: P[1];
A2: now let k be non zero Nat;
assume P[k];
power(R).(0.R,k+1) = power(R).(0.R,k) * 0.R by GROUP_1:def 7 .= 0.R;
hence P[k + 1];
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A1,A2);
hence thesis;
end;
registration
cluster Z/3 -> non degenerated almost_left_invertible;
coherence by PEPIN:41;
end;
registration
cluster finite for Field;
existence
proof
take Z/3;
thus thesis;
end;
cluster infinite for Field;
existence
proof
take F_Real;
thus thesis;
end;
end;
definition
let L be non empty doubleLoopStr;
attr L is almost_trivial means
:Def1:
for a being Element of L holds a = 1.L or a = 0.L;
end;
registration
cluster degenerated -> almost_trivial for Ring;
coherence
proof
let R be Ring;
assume
A1: R is degenerated;
now let a be Element of R;
a = a * 1.R .= a * 0.R by A1,STRUCT_0:def 8 .= 0.R;
hence a = 1.R or a = 0.R;
end;
hence thesis;
end;
cluster non almost_trivial for Field;
existence
proof
take F = Z/3;
A2: Z/3 = doubleLoopStr(#Segm(3),addint(3),multint(3),In(1,Segm(3)),
In(0,Segm(3))#) by INT_3:def 12; then
reconsider t = 2 as Element of [#]F by NAT_1:44;
A3: t <> 0.F by A2,NAT_1:44,SUBSET_1:def 8;
t <> 1.F by A2,NAT_1:44,SUBSET_1:def 8;
hence thesis by A3;
end;
end;
theorem
for R being Ring holds
R is almost_trivial iff (R is degenerated or R,Z/2 are_isomorphic)
proof
let R be Ring;
A1: Z/2 =
doubleLoopStr(#Segm(2),addint(2),multint(2),In(1,Segm(2)),In(0,Segm(2))#)
by INT_3:def 12;
A2: now assume R is degenerated or R,Z/2 are_isomorphic; then
per cases;
suppose R is degenerated;
hence R is almost_trivial;
end;
suppose R,Z/2 are_isomorphic; then
consider f being Function of R,(Z/2) such that
A4: f is isomorphism by QUOFIELD:def 23;
f is monomorphism onto by A4,MOD_4:def 12; then
A5: f is linear one-to-one by MOD_4:def 8;
now let a be Element of R;
A6: dom f = [#]R by FUNCT_2:def 1;
A7: [#]INT.Ring(2) = 2 by A1,ORDINAL1:def 17;
per cases by A7,CARD_1:50,TARSKI:def 2;
suppose f.a = 0; then
f.a = 0.(Z/2) by A1 .= f.(0.R) by A5,RING_2:6;
hence a = 1.R or a = 0.R by A5,A6;
end;
suppose f.a = 1; then
f.a = 1_(Z/2) by INT_3:14
.= f.(1_R) by A5,GROUP_1:def 13 .= f.(1.R);
hence a = 1.R or a = 0.R by A5,A6;
end;
end;
hence R is almost_trivial;
end;
end;
set A = the carrier of R, B = the carrier of (Z/2);
now assume that
A8: R is almost_trivial and
A9: R is non degenerated;
set f = {[0.R,0.(Z/2)],[1.R,1.(Z/2)]};
now let o be object;
assume o in f; then
per cases by TARSKI:def 2;
suppose o = [0.R,0.(Z/2)];
hence o in [:A,B:] by ZFMISC_1:def 2;
end;
suppose o = [1.R,1.(Z/2)];
hence o in [:A,B:] by ZFMISC_1:def 2;
end;
end; then
reconsider f as Subset of [:A,B:] by TARSKI:def 3;
reconsider f as Relation of A,B;
now let x,y1,y2 be object;
assume
A11: [x,y1] in f & [x,y2] in f; then
per cases by TARSKI:def 2;
suppose
A12: [x,y1] = [0.R,0.(Z/2)];
A13: y1 = [0.R,0.(Z/2)]`2 by A12.= 0.(Z/2);
A14: x = [0.R,0.(Z/2)]`1 by A12 .= 0.R;
per cases by A11,TARSKI:def 2;
suppose [x,y2] = [0.R,0.(Z/2)]; then
y2 = [0.R,0.(Z/2)]`2 .= 0.(Z/2);
hence y1 = y2 by A13;
end;
suppose [x,y2] = [1.R,1.(Z/2)]; then
x = [1.R,1.(Z/2)]`1 .= 1.R;
hence y1 = y2 by A14,A9;
end;
end;
suppose
A15: [x,y1] = [1.R,1.(Z/2)]; then
A16: y1 = [1.R,1.(Z/2)]`2 .= 1.(Z/2);
A17: x = [1.R,1.(Z/2)]`1 by A15 .= 1.R;
per cases by A11,TARSKI:def 2;
suppose [x,y2] = [0.R,0.(Z/2)]; then
x = [0.R,0.(Z/2)]`1 .= 0.R;
hence y1 = y2 by A17,A9;
end;
suppose [x,y2] = [1.R,1.(Z/2)]; then
y2 = [1.R,1.(Z/2)]`2 .= 1.(Z/2);
hence y1 = y2 by A16;
end;
end;
end; then
reconsider f as PartFunc of A,B by FUNCT_1:def 1;
A18: dom f c= A;
now let o be object;
assume o in A; then
reconsider a = o as Element of R;
per cases by A8;
suppose a = 0.R; then
[a,0.(Z/2)] in f by TARSKI:def 2;
hence o in dom f by FUNCT_1:1;
end;
suppose a = 1.R; then
[a,1.(Z/2)] in f by TARSKI:def 2;
hence o in dom f by FUNCT_1:1;
end;
end; then
A19: dom f = A by A18,TARSKI:2;
reconsider f as Function of A,B by A19,FUNCT_2:def 1;
A20: f.(0.R) = 0.(Z/2) & f.(1.R) = 1.(Z/2)
proof
[0.R,0.(Z/2)] in f by TARSKI:def 2;
hence f.(0.R) = 0.(Z/2) by A19,FUNCT_1:def 2;
[1.R,1.(Z/2)] in f by TARSKI:def 2;
hence f.(1.R) = 1.(Z/2) by A19,FUNCT_1:def 2;
end;
A21: now let a,b be Element of R;
per cases by A8;
suppose a = 0.R;
hence f.(a+b) = f.a + f.b by A20;
end;
suppose
A22: a = 1.R;
per cases by A8;
suppose b = 0.R;
hence f.(a+b) = f.a + f.b by A20;
end;
suppose
A23: b = 1.R;
now assume
A24: a + b = 1.R;
consider y being Element of R such that
A25: a + y = 0.R by ALGSTR_0:def 11;
per cases by A8;
suppose y = 0.R;
hence contradiction by A20,A22,A25;
end;
suppose y = 1.R;
hence contradiction by A24,A25,A23,A20;
end;
end;
hence f.(a+b) = f.a + f.b by A8,A20,Th5,A23,A22;
end;
end;
end;
now let a,b be Element of R;
per cases by A8;
suppose a = 0.R;
hence f.(a*b) = f.a * f.b by A20;
end;
suppose a = 1.R;
hence f.(a*b) = f.a * f.b by A20;
end;
end; then
A28: f is additive multiplicative unity-preserving
by A20,A21,GROUP_6:def 6;
now let x,y be object;
assume
A29: x in A & y in A & f.x = f.y; then
reconsider a = x, b = y as Element of R;
per cases by A8;
suppose a = 0.R;
hence x = y by A8,A20,A29;
end;
suppose a = 1.R;
hence x = y by A8,A20,A29;
end;
end; then
f is one-to-one by FUNCT_2:19; then
A30: f is monomorphism by A28,MOD_4:def 8;
A31: now let o be object;
assume o in rng f; then
consider x being object such that
A32: x in dom f & o = f.x by FUNCT_1:def 3;
reconsider a = x as Element of R by A32;
per cases by A8;
suppose a = 0.R;
hence o in B by A20,A32;
end;
suppose a = 1.R;
hence o in B by A20,A32;
end;
end;
now let o be object;
assume o in B; then
A33: o in 2 by A1,ORDINAL1:def 17;
per cases by A33,CARD_1:50,TARSKI:def 2;
suppose o = 0; then
o=f.(0.R)
by A1,A20,NAT_1:44,SUBSET_1:def 8;
hence o in rng f by A19,FUNCT_1:def 3;
end;
suppose o = 1; then
o=f.(1.R)
by A20,A1,NAT_1:44,SUBSET_1:def 8;
hence o in rng f by A19,FUNCT_1:def 3;
end;
end; then
f is onto by A31,TARSKI:2;
hence R,Z/2 are_isomorphic
by A30,MOD_4:def 12,QUOFIELD:def 23;
end;
hence thesis by A2;
end;
definition
let R be Ring;
let a be Element of R;
attr a is trivial means
:Def2:
a = 1.R or a = 0.R;
end;
registration
let R be non almost_trivial Ring;
cluster non trivial for Element of R;
existence
proof
consider a being Element of R such that
A1: a <> 1.R & a <> 0.R by Def1;
take a;
thus thesis by A1;
end;
end;
definition
let R be Ring;
attr R is polynomial_disjoint means
:Def3:
[#]R /\ [#]Polynom-Ring R = {};
end;
begin :: Some Negative Results
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
func carr(x,o) -> non empty set equals
([#]R \ {x}) \/ {o};
coherence;
end;
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
let a,b be Element of carr(x,o);
func addR(a,b) -> Element of carr(x,o) equals
:Def4:
(the addF of R).(x,x) if a = o & b = o & (the addF of R).(x,x) <> x,
(the addF of R).(a,x) if a <> o & b = o & (the addF of R).(a,x) <> x,
(the addF of R).(x,b) if a = o & b <> o & (the addF of R).(x,b) <> x,
(the addF of R).(a,b) if a <> o & b <> o & (the addF of R).(a,b) <> x
otherwise o;
coherence
proof
A1: now assume a = o & b = o & (the addF of R).(x,x) <> x; then
not (the addF of R).(x,x) in {x} by TARSKI:def 1; then
(the addF of R).(x,x) in [#]R \ {x} by XBOOLE_0:def 5;
hence (the addF of R).(x,x) is Element of carr(x,o) by XBOOLE_0:def 3;
end;
A2: now assume
A3: a <> o & b= o & (the addF of R).(a,x) <> x; then
not a in {o} by TARSKI:def 1; then
a in [#]R \ {x} by XBOOLE_0:def 3; then
reconsider a1 = a as Element of [#]R;
not (the addF of R).(a,x) in {x} by A3,TARSKI:def 1; then
(the addF of R).(a1,x) in [#]R \ {x} by XBOOLE_0:def 5;
hence (the addF of R).(a,x) is Element of carr(x,o) by XBOOLE_0:def 3;
end;
A4: now assume
A5: a = o & b <> o & (the addF of R).(x,b) <> x; then
not b in {o} by TARSKI:def 1; then
b in [#]R \ {x} by XBOOLE_0:def 3; then
reconsider b1 = b as Element of [#]R;
not (the addF of R).(x,b) in {x} by A5,TARSKI:def 1; then
(the addF of R).(x,b1) in [#]R \ {x} by XBOOLE_0:def 5;
hence (the addF of R).(x,b) is Element of carr(x,o) by XBOOLE_0:def 3;
end;
A6: now assume
A7: a <> o & b <> o & (the addF of R).(a,b) <> x; then
not a in {o} by TARSKI:def 1; then
a in [#]R \ {x} by XBOOLE_0:def 3; then
reconsider a1 = a as Element of [#]R;
not b in {o} by A7,TARSKI:def 1; then
b in [#]R \ {x} by XBOOLE_0:def 3; then
reconsider b1 = b as Element of [#]R;
not (the addF of R).(a,b) in {x} by A7,TARSKI:def 1; then
(the addF of R).(a1,b1) in [#]R \ {x} by XBOOLE_0:def 5;
hence (the addF of R).(a,b) is Element of carr(x,o) by XBOOLE_0:def 3;
end;
o in {o} by TARSKI:def 1;
hence thesis by A1,A2,A4,A6,XBOOLE_0:def 3;
end;
consistency;
end;
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
func addR(x,o) -> BinOp of carr(x,o) means
:Def5:
for a,b being Element of carr(x,o) holds it.(a,b) = addR(a,b);
existence
proof
deffunc O(Element of carr(x,o),Element of carr(x,o)) = addR($1,$2);
consider F being BinOp of carr(x,o) such that
A1: for a,b being Element of carr(x,o) holds F.(a,b)=O(a,b) from BINOP_1:sch 4;
take F;
let a,b be Element of carr(x,o);
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be BinOp of carr(x,o) such that
A2: for a,b being Element of carr(x,o) holds F1.(a,b) = addR(a,b) and
A3: for a,b being Element of carr(x,o) holds F2.(a,b) = addR(a,b);
now let a,b be Element of carr(x,o);
thus F1.(a,b) = addR(a,b) by A2 .= F2.(a,b) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
let a,b be Element of carr(x,o);
func multR(a,b) -> Element of carr(x,o) equals
:Def6:
(the multF of R).(x,x) if a = o & b = o & (the multF of R).(x,x) <> x,
(the multF of R).(a,x) if a <> o & b = o & (the multF of R).(a,x) <> x,
(the multF of R).(x,b) if a = o & b <> o & (the multF of R).(x,b) <> x,
(the multF of R).(a,b) if a <> o & b <> o & (the multF of R).(a,b) <> x
otherwise o;
coherence
proof
A1: now assume a = o & b = o & (the multF of R).(x,x) <> x; then
not (the multF of R).(x,x) in {x} by TARSKI:def 1; then
(the multF of R).(x,x) in [#]R \ {x} by XBOOLE_0:def 5;
hence (the multF of R).(x,x) is Element of carr(x,o) by XBOOLE_0:def 3;
end;
A2: now assume
A3: a <> o & b = o & (the multF of R).(a,x) <> x; then
not a in {o} by TARSKI:def 1; then
a in [#]R \ {x} by XBOOLE_0:def 3; then
reconsider a1 = a as Element of [#]R;
not (the multF of R).(a,x) in {x} by A3,TARSKI:def 1; then
(the multF of R).(a1,x) in ([#]R) \ {x} by XBOOLE_0:def 5;
hence (the multF of R).(a,x) is Element of carr(x,o) by XBOOLE_0:def 3;
end;
A4: now assume
A5: a = o & b <> o & (the multF of R).(x,b) <> x; then
not b in {o} by TARSKI:def 1; then
b in [#]R \ {x} by XBOOLE_0:def 3; then
reconsider b1 = b as Element of [#]R;
not (the multF of R).(x,b) in {x} by A5,TARSKI:def 1; then
(the multF of R).(x,b1) in [#]R \ {x} by XBOOLE_0:def 5;
hence (the multF of R).(x,b) is Element of carr(x,o) by XBOOLE_0:def 3;
end;
A6: now assume
A7: a <> o & b <> o & (the multF of R).(a,b) <> x; then
not a in {o} by TARSKI:def 1; then
a in [#]R \ {x} by XBOOLE_0:def 3; then
reconsider a1 = a as Element of [#]R;
not b in {o} by A7,TARSKI:def 1; then
b in [#]R \ {x} by XBOOLE_0:def 3; then
reconsider b1 = b as Element of [#]R;
not (the multF of R).(a,b) in {x} by A7,TARSKI:def 1; then
(the multF of R).(a1,b1) in ([#]R) \ {x} by XBOOLE_0:def 5;
hence (the multF of R).(a,b) is Element of carr(x,o) by XBOOLE_0:def 3;
end;
o in {o} by TARSKI:def 1;
hence thesis by A1,A2,A4,A6,XBOOLE_0:def 3;
end;
consistency;
end;
definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object;
func multR(x,o) -> BinOp of carr(x,o) means
:Def7:
for a,b being Element of carr(x,o) holds it.(a,b) = multR(a,b);
existence
proof
deffunc O(Element of carr(x,o),Element of carr(x,o)) = multR($1,$2);
consider F being BinOp of carr(x,o) such that
A1: for a,b being Element of carr(x,o) holds F.(a,b) = O(a,b)
from BINOP_1:sch 4;
take F;
let a,b be Element of carr(x,o);
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be BinOp of carr(x,o) such that
A2: for a,b being Element of carr(x,o) holds F1.(a,b) = multR(a,b) and
A3: for a,b being Element of carr(x,o) holds F2.(a,b) = multR(a,b);
now let a,b be Element of carr(x,o);
thus F1.(a,b) = multR(a,b) by A2 .= F2.(a,b) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
func ExField(x,o) -> strict doubleLoopStr means
:Def8:
the carrier of it = carr(x,o) &
the addF of it = addR(x,o) &
the multF of it = multR(x,o) &
the OneF of it = 1.F &
the ZeroF of it = 0.F;
existence
proof
1.F <> x by Def2; then
not 1.F in {x} by TARSKI:def 1; then
1.F in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider e = 1.F as Element of carr(x,o) by XBOOLE_0:def 3;
0.F <> x by Def2; then
not 0.F in {x} by TARSKI:def 1; then
0.F in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider u = 0.F as Element of carr(x,o) by XBOOLE_0:def 3;
take doubleLoopStr(#carr(x,o),addR(x,o),multR(x,o),e,u#);
thus thesis;
end;
uniqueness;
end;
registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
cluster ExField(x,o) -> non degenerated;
coherence
proof
0.(ExField(x,o)) = 0.F & 1.(ExField(x,o)) = 1.F by Def8;
hence thesis by STRUCT_0:def 8;
end;
end;
registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
cluster ExField(x,o) -> Abelian;
coherence
proof
set R = F;
A1: [#]ExField(x,o) = carr(x,o) by Def8;
now let a,b be Element of ExField(x,o);
per cases;
suppose
A2: b = o; then
b in {o} by TARSKI:def 1; then
reconsider b1 = b as Element of carr(x,o) by XBOOLE_0:def 3;
per cases;
suppose
A3: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of carr(x,o) by XBOOLE_0:def 3;
thus a + b = b + a by A2,A3;
end;
suppose
A4: a <> o; then
not a in {o} by TARSKI:def 1; then
A5: a in [#]R \ {x} by A1,XBOOLE_0:def 3;
reconsider a1 = a as Element of carr(x,o) by Def8;
reconsider aR = a as Element of R by A5;
A6: (the addF of R).(a1,x)=aR + x .=x + aR .=(the addF of R).(x,a1);
per cases;
suppose
A7: (the addF of R).(a,x) <> x;
thus
a + b = (addR(x,o)).(a1,b1) by Def8 .= addR(a1,b1) by Def5
.= (the addF of R).(a,x) by A7,A4,A2,Def4
.= addR(b1,a1) by A2,A4,A6,A7,Def4
.= (addR(x,o)).(b1,a1) by Def5
.= b + a by Def8;
end;
suppose
A8: (the addF of R).(a,x) = x;
thus
a + b = (addR(x,o)).(a1,b1) by Def8 .= addR(a1,b1) by Def5
.= o by A8,A4,A2,Def4 .= addR(b1,a1) by A6,A8,A4,A2,Def4
.= (addR(x,o)).(b1,a1) by Def5 .= b + a by Def8;
end;
end;
end;
suppose
A9: b <> o; then
not b in {o} by TARSKI:def 1; then
A10: b in [#]R \ {x} by A1,XBOOLE_0:def 3;
reconsider b1 = b as Element of carr(x,o) by Def8;
per cases;
suppose
A11: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of carr(x,o) by XBOOLE_0:def 3;
reconsider bR = b as Element of R by A10;
A12: (the addF of R).(x,b1) =x + bR .=bR + x
.=(the addF of R).(b1,x);
per cases;
suppose
A13: (the addF of R).(x,b) <> x;
thus a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5
.= (the addF of R).(x,b) by A13,A11,A9,Def4
.= addR(b1,a1) by A9,A11,A12,A13,Def4
.= (addR(x,o)).(b1,a1) by Def5 .= b + a by Def8;
end;
suppose
A14: (the addF of R).(x,b) = x;
thus a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5 .= o by A9,A11,A14,Def4
.= addR(b1,a1) by A9,A11,A12,A14,Def4
.= (addR(x,o)).(b1,a1) by Def5 .= b + a by Def8;
end;
end;
suppose
A15: a <> o; then
not a in {o} by TARSKI:def 1; then
A16: a in [#]R\{x} by A1,XBOOLE_0:def 3;
reconsider a1 = a as Element of carr(x,o) by Def8;
reconsider aR=a,bR=b as Element of [#]R by A10,A16;
A17: (the addF of R).(a,b) = aR + bR .= bR + aR
.= (the addF of R).(b,a);
per cases;
suppose
A18: (the addF of R).(a,b) <> x;
thus a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5
.= (the addF of R).(a,b) by A9,A15,A18,Def4
.= addR(b1,a1) by A9,A15,A17,A18,Def4
.= (addR(x,o)).(b1,a1) by Def5
.= b + a by Def8;
end;
suppose
A19: (the addF of R).(a,b) = x;
thus a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5 .= o by A9,A15,A19,Def4
.= addR(b1,a1) by A9,A15,A17,A19,Def4
.= (addR(x,o)).(b1,a1) by Def5 .= b + a by Def8;
end;
end;
end;
end;
hence ExField(x,o) is Abelian by RLVECT_1:def 2;
end;
end;
reserve o for object;
reserve F for non almost_trivial Field;
reserve x,a for Element of F;
theorem Th7:
for x being non trivial Element of F, o being object st
not o in [#]F holds ExField(x,o) is right_zeroed right_complementable
proof
let x be non trivial Element of F, o be object;
assume a1: not o in [#]F; then
A1: a <> o;
set C = carr(x,o);
set ADDR = the addF of F;
consider xi being Element of F such that
A2: x+xi = 0.F by ALGSTR_0:def 11;
A3: [#]ExField(x,o) = C by Def8;
o in {o} by TARSKI:def 1; then
reconsider u1 = o as Element of C by XBOOLE_0:def 3;
reconsider u = u1 as Element of ExField(x,o) by Def8;
now let a be Element of ExField(x,o);
A4: 0.(ExField(x,o)) = 0.F by Def8;
0.F <> x by Def2; then
not 0.F in {x} by TARSKI:def 1; then
0.F in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider u = 0.F as Element of C by XBOOLE_0:def 3;
A5: o <> u by a1;
per cases;
suppose
A6: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of C by XBOOLE_0:def 3;
A7: (the addF of F).(x,0.F) = x + 0.F .= x;
thus
a + 0.(ExField(x,o)) = (addR(x,o)).(a1,u) by A4,Def8
.= addR(a1,u) by Def5 .= a by A5,A6,A7,Def4;
end;
suppose
A8: a <> o; then
not a in {o} by TARSKI:def 1; then
A9: a in [#]F \ {x} by A3,XBOOLE_0:def 3;
reconsider a1 = a as Element of C by Def8;
reconsider aR = a as Element of [#]F by A9;
A10: (the addF of F).(a,u) = aR + 0.F .= aR;
not aR in {x} by A9,XBOOLE_0:def 5; then
A11: (the addF of F).(a,u) <> x by A10,TARSKI:def 1;
thus
a + 0.(ExField(x,o)) = (addR(x,o)).(a1,u) by A4,Def8
.= addR(a1,u) by Def5 .= aR + 0.F by A8,A5,A11,Def4 .= a;
end;
end;
hence ExField(x,o) is right_zeroed by RLVECT_1:def 4;
now let a be Element of ExField(x,o);
per cases;
suppose
A12: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A13: xi = x; then
A14: (the addF of F).(x,x) <> x by A2,Def2;
a + u = (addR(x,o)).(a1,u1) by Def8 .= addR(a1,u1) by Def5
.= (the addF of F).(x,xi) by A12,A13,A14,Def4
.= 0.(ExField(x,o)) by A2,Def8;
hence a is right_complementable by ALGSTR_0:def 11;
end;
suppose xi <> x; then
not xi in {x} by TARSKI:def 1; then
xi in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider x1i = xi as Element of carr(x,o) by XBOOLE_0:def 3;
reconsider b = x1i as Element of ExField(x,o) by Def8;
A15: (the addF of F).(x,b) <> x by A2,Def2;
a + b = (addR(x,o)).(a1,x1i) by Def8 .= addR(a1,x1i) by Def5
.= (the addF of F).(x,xi) by A1,A12,A15,Def4
.= 0.(ExField(x,o)) by A2,Def8;
hence a is right_complementable by ALGSTR_0:def 11;
end;
end;
suppose
A16: a <> o; then
not a in {o} by TARSKI:def 1; then
A17: a in [#]F \ {x} by A3,XBOOLE_0:def 3;
reconsider a1 = a as Element of C by Def8;
reconsider aR = a as Element of [#]F by A17;
consider aRi being Element of F such that
A18: aR + aRi = 0.F by ALGSTR_0:def 11;
per cases;
suppose
A19: aRi = x; then
A20: (the addF of F).(a,x) <> x by A18,Def2;
a + u = (addR(x,o)).(a1,u1) by Def8 .= addR(a1,u1) by Def5
.= (the addF of F).(aR,aRi) by A16,A19,A20,Def4
.= 0.(ExField(x,o)) by A18,Def8;
hence a is right_complementable by ALGSTR_0:def 11;
end;
suppose aRi <> x; then
not aRi in {x} by TARSKI:def 1; then
aRi in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider a1i = aRi as Element of C by XBOOLE_0:def 3;
reconsider b = a1i as Element of ExField(x,o) by Def8;
A21: (the addF of F).(a,b) <> x by A18,Def2;
A22: aR <> o & aRi <> o by a1;
a + b = (addR(x,o)).(a1,aRi) by Def8 .= addR(a1,a1i) by Def5
.= (the addF of F).(aR,aRi) by A21,A22,Def4
.= 0.(ExField(x,o)) by A18,Def8;
hence a is right_complementable by ALGSTR_0:def 11;
end;
end;
end;
hence ExField(x,o) is right_complementable by ALGSTR_0:def 16;
end;
theorem Th8:
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is add-associative
proof
let x be non trivial Element of F, o be object;
assume a1: not o in [#]F; then
A1: a <> o;
set C = carr(x,o), E = ExField(x,o);
set ADDR = the addF of F;
A2: [#]E = C by Def8;
now let a,b,c be Element of E;
per cases;
suppose
A3: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A4: b = o; then
b in {o} by TARSKI:def 1; then
reconsider b1 = b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A5: (ADDR).(x,x) <> x;
A6: a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5 .= x + x by A3,A4,A5,Def4;
not x + x in {x} by A5,TARSKI:def 1; then
x + x in [#]F\{x} by XBOOLE_0:def 5; then
reconsider xx = x + x as Element of C by XBOOLE_0:def 3;
A7: xx <> o by a1;
per cases;
suppose
A8: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A9: (a + b) + c = (addR(x,o)).(a+b,c1) by Def8
.= addR(xx,c1) by A6,Def5;
A10: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5 .= x + x by A4,A5,A8,Def4;
per cases;
suppose
A11: (ADDR).(xx,x) <> x;
A12: (ADDR).(x,xx) = x + (x + x) .= (x + x) + x;
thus (a + b) + c = (x + x) + x by A1,A8,A9,A11,Def4
.= addR(a1,xx) by A1,A3,A11,A12,Def4
.= (addR(x,o)).(a1,xx) by Def5
.= a + (b + c) by A10,Def8;
end;
suppose
A13: (ADDR).(xx,x) = x;
A14: (ADDR).(x,xx) = x + (x + x) .= (x + x) + x;
thus (a + b) + c = o by A7,A8,A9,A13,Def4
.= addR(a1,xx) by A3,A7,A13,A14,Def4
.= (addR(x,o)).(a1,xx) by Def5
.= a + (b + c) by A10,Def8;
end;
end;
suppose
A15: c <> o; then
not c in {o} by TARSKI:def 1; then
c in [#]F\{x} by A2,XBOOLE_0:def 3; then
reconsider cR = c as Element of F;
reconsider c1 = c as Element of C by Def8;
A16: (a + b) + c = (addR(x,o)).(a+b,c1) by Def8
.= addR(xx,c1) by A6,Def5;
A17: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5; then
reconsider bc = b + c as Element of C;
per cases;
suppose
A18: (ADDR).(x,c1) <> x; then
A19: b + c = x + cR by A4,A15,A17,Def4; then
A20: b + c <> o by a1;
per cases;
suppose (ADDR).(xx,c1) <> x; then
A21: (a + b) + c = (x + x) + cR by A7,A15,A16,Def4
.= x + (x + cR) by RLVECT_1:def 3
.= (ADDR).(x,b+c) by A4,A15,A17,A18,Def4;
per cases;
suppose (ADDR).(x,bc) <> x;
hence (a + b) + c = addR(a1,bc) by A1,A3,A19,A21,Def4
.= (addR(x,o)).(a1,b+c) by Def5 .= a + (b + c) by Def8;
end;
suppose
A22: (ADDR).(x,bc) = x;
A23: (ADDR).(x,bc) = x + (x + cR) by A4,A15,A17,A18,Def4
.=(x + x) + cR by RLVECT_1:def 3.=(ADDR).(xx,c1);
thus
(a + b) + c = o by A7,A15,A16,A22,A23,Def4
.= addR(a1,bc) by A3,A20,A22,Def4
.= (addR(x,o)).(a1,b+c) by Def5 .= a + (b + c) by Def8;
end;
end;
suppose
A24: (ADDR).(xx,c1) = x; then
A25: (a + b) + c = o by A7,A15,A16,Def4;
per cases;
suppose (ADDR).(x,bc) <> x;
A26: (ADDR).(x,bc) = x + (x + cR) by A4,A15,A17,A18,Def4
.= (x + x) + cR by RLVECT_1:def 3
.= (ADDR).(xx,c1);
thus
(a + b) + c = addR(a1,bc) by A3,A20,A26,A24,A25,Def4
.= (addR(x,o)).(a1,b+c) by Def5 .= a + (b + c) by Def8;
end;
suppose
A27: (ADDR).(x,bc) = x;
(ADDR).(x,bc) = x + (x + cR) by A4,A15,A17,A18,Def4
.= (x + x) + cR by RLVECT_1:def 3
.= (ADDR).(xx,c1);
hence (a + b) + c = o by A7,A15,A16,A27,Def4
.= addR(a1,bc) by A3,A20,A27,Def4
.= (addR(x,o)).(a1,b+c) by Def5 .= a + (b + c) by Def8;
end;
end;
end;
suppose
A29: (ADDR).(x,c1) = x; then
x + cR = x; then
A30: c1 = 0.F by RLVECT_1:9;
A31: b + c = o by A4,A29,A15,A17,Def4;
per cases;
suppose (ADDR).(xx,c1) <> x;
hence (a + b) + c =(x + x)+ cR by A7,A15,A16,Def4
.= addR(a1,bc) by A3,A5,A30,A31,Def4
.= (addR(x,o)).(a1,b+c) by Def5
.= a + (b + c) by Def8;
end;
suppose (ADDR).(xx,c1) = x; then
x = (x + x) + cR .= x + x by A30;
hence (a + b) + c = a + (b + c) by A5;
end;
end;
end;
end;
suppose
A33: (ADDR).(x,x) = x;
A34: a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5.= o by A3,A4,A33,Def4;then
a + b in {o} by TARSKI:def 1; then
reconsider ab = a + b as Element of C by XBOOLE_0:def 3;
per cases;
suppose c = o;
hence (a + b) + c = a + (b + c) by A3;
end;
suppose
A36: c <> o; then
not c in {o} by TARSKI:def 1; then
c in [#]F\{x} by A2,XBOOLE_0:def 3; then
reconsider cR = c as Element of F;
reconsider c1 = c as Element of C by Def8;
per cases;
suppose
A37: (ADDR).(x,c1) = x;
A38: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5 .= o by A4,A36,A37,Def4;then
b + c in {o} by TARSKI:def 1; then
reconsider bc = b + c as Element of C by XBOOLE_0:def 3;
thus
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5 .= o by A36,A34,A37,Def4
.= addR(a1,bc) by A3,A33,A38,Def4
.= (addR(x,o)).(a1,b+c) by Def5 .= a + (b + c) by Def8;
end;
suppose
A39: (ADDR).(x,c1) <> x;
A40: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5 .= x + cR by A4,A36,A39,Def4;
reconsider bc = b+c as Element of C by Def8;
A41: (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5 .= (ADDR).(x,c1)
by A34,A36,A39,Def4;
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (x + x) + cR by A33,A34,A36,A39,Def4
.= x + (x + cR) by RLVECT_1:def 3
.= (ADDR).(x,bc) by A40;
hence (a + b) + c = addR(a1,bc) by A1,A3,A39,A40,A41,Def4
.= (addR(x,o)).(a1,b+c) by Def5 .= a + (b + c) by Def8;
end;
end;
end;
end;
suppose
A42: b <> o; then
not b in {o} by TARSKI:def 1; then
b in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider bR = b as Element of F;
reconsider b1 = b as Element of C by Def8;
A43: (ADDR).(x,b) = x + bR .= bR + x
.= (ADDR).(b,x);
per cases;
suppose
A44: (ADDR).(x,b) <> x;
A45: a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5
.= x + bR by A3,A42,A44,Def4; then
A46: a + b <> o by A1; then
not a + b in {o} by TARSKI:def 1; then
a + b in [#]F\{x} by A2,XBOOLE_0:def 3; then
reconsider abR = a + b as Element of F;
reconsider ab = a+b as Element of C by Def8;
per cases;
suppose
A47: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A48: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + x by A42,A43,A44,A47,Def4;
A49: b + c <> o by A1,A48; then
not b + c in {o} by TARSKI:def 1; then
b + c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider bcR = b + c as Element of F;
reconsider bc = b+c as Element of C by Def8;
A50: (ADDR).(ab,x) = (x + bR) + x by A45 .= x + (bR + x);
per cases;
suppose
A51: (ADDR).(ab,x) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (ADDR).(x,bc) by A1,A3,A47,A48,A50,A51,Def4
.= addR(a1,bc) by A1,A3,A48,A50,A51,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A52: (ADDR).(ab,x) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5 .= o by A46,A47,A52,Def4
.= addR(a1,bc) by A3,A48,A49,A50,A52,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
suppose
A53: c <> o; then
not c in {o} by TARSKI:def 1; then
c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider cR = c as Element of F;
reconsider c1 = c as Element of C by Def8;
A54: (ADDR).(ab,c) = (x + bR) + cR by A45
.= x + (bR + cR) by RLVECT_1:def 3;
per cases;
suppose
A55: (ADDR).(b,c) <> x;
A56: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + cR by A42,A53,A55,Def4;
A57: b + c <> o by A1,A56; then
not b + c in {o} by TARSKI:def 1; then
b + c in [#]F\{x} by A2,XBOOLE_0:def 3; then
reconsider bcR = b + c as Element of F;
reconsider bc = b+c as Element of C by Def8;
per cases;
suppose
A58: (ADDR).(ab,c1) <> x;
thus (a + b) + c =(addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (x + bR) + cR by A45,A58,A53,A46,Def4
.= x + (bR + cR) by RLVECT_1:def 3
.= addR(a1,bc) by A1,A3,A54,A58,A56,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A59: (ADDR).(ab,c1) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5 .= o by A59,A53,A46,Def4
.= addR(a1,bc) by A3,A54,A59,A56,A57,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
suppose
A60: (ADDR).(b,c) = x;
A61: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A60,A53,A42,Def4; then
b + c in {o} by TARSKI:def 1;then
reconsider bc = b + c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A62: (ADDR).(ab,c1) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (x + bR) + cR by A45,A46,A53,A62,Def4
.= x + (bR + cR) by RLVECT_1:def 3
.= addR(a1,bc) by A60,A3,A54,A62,A61,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A63: (ADDR).(ab,c1) = x;
thus (a + b)+ c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5 .= o by A63,A53,A46,Def4
.= addR(a1,bc) by A60,A3,A54,A63,A61,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
end;
end;
suppose
A64: (ADDR).(x,b) = x;
A65: a + b=(addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5
.= o by A64,A42,A3,Def4; then
a + b in {o} by TARSKI:def 1;then
reconsider ab = a + b as Element of C by XBOOLE_0:def 3;
per cases;
suppose c = o;
hence (a + b) + c = a + (b + c) by A3;
end;
suppose
A68: c <> o; then
not c in {o} by TARSKI:def 1; then
A69: c in [#]F\{x} by A2,XBOOLE_0:def 3; then
reconsider cR = c as Element of F;
reconsider c1 = c as Element of C by Def8;
A70: now assume (ADDR).(b,c) = x; then
bR + cR = x + bR by A64 .= bR + x; then
x = cR by ALGSTR_0:def 4;then
c in {x} by TARSKI:def 1;
hence contradiction by A69,XBOOLE_0:def 5;
end;
A72: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + cR by A70,A68,A42,Def4;
A73: b + c <> o by A72,A1; then
not b + c in {o} by TARSKI:def 1; then
b + c in [#]F\{x} by A2,XBOOLE_0:def 3; then
reconsider bcR = b + c as Element of F;
reconsider bc = b+c as Element of C by Def8;
A74: x + (bR + cR) = (x + bR) + cR by RLVECT_1:def 3
.= x + cR by A64;
per cases;
suppose
A75: (ADDR).(x,c1) <> x;
thus (a + b)+ c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (ADDR).(x,c1) by A65,A75,A68,Def4
.= addR(a1,bc) by A74,A3,A75,A72,A1,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A76: (ADDR).(x,c1) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A76,A68,A65,Def4
.= addR(a1,bc) by A73,A76,A74,A3,A72,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
end;
end;
end;
suppose
A77: a <> o;
not a in {o} by A77,TARSKI:def 1; then
A78: a in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider aR = a as Element of F;
reconsider a1 = a as Element of C by Def8;
per cases;
suppose
A79: b = o;
b in {o} by A79,TARSKI:def 1; then
reconsider b1 = b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A80: (ADDR).(a1,x) = x;
A81: a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5
.= o by A80,A79,A77,Def4; then
a + b in {o} by TARSKI:def 1; then
reconsider ab = a + b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A81a: c = o;
c in {o} by A81a,TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A82: (ADDR).(x,x) = x;
A83: b + c =(addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A81a,A79,A82,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc = b + c as Element of C by XBOOLE_0:def 3;
thus
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A81,A81a,A82,Def4
.= addR(a1,bc) by A80,A77,A83,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A84: (ADDR).(x,x) <> x;
A85: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= x + x by A84,A79,A81a,Def4; then
A86: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A87: b + c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bcR = b + c as Element of F by A87;
reconsider bc = b+c as Element of C by Def8;
A88: (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + x) + x by A80,A81,A81a,A84,Def4;
now assume (ADDR).(a1,bc) = x; then
aR + bcR = aR + x by A80; then
bcR = x by ALGSTR_0:def 4; then
b + c in {x} by TARSKI:def 1;
hence contradiction by A87,XBOOLE_0:def 5;
end; then
(ADDR).(a1,bc) = addR(a1,bc) by A77,A86,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
hence a + (b + c) = aR + (x + x) by A85
.= (a + b) + c by A88,RLVECT_1:def 3;
end;
end;
suppose
A90: c <> o;
not c in {o} by A90,TARSKI:def 1; then
A91: c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A91;
per cases;
suppose
A92: (ADDR).(x,c) = x;
A93: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A92,A90,A79,Def4;
then
b + c in {o} by TARSKI:def 1; then
reconsider bc = b + c as Element of C by XBOOLE_0:def 3;
thus
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.=addR(ab,c1) by Def5
.= o by A81,A90,A92,Def4
.= addR(a1,bc) by A80,A77,A93,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A94: (ADDR).(x,c) <> x;
A95: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= x + cR by A94,A90,A79,Def4; then
A96: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A97: b + c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b + c as Element of C by Def8;
reconsider bcR = b + c as Element of F by A97;
A98: now assume (ADDR).(a1,bc) = x; then
aR + bcR = aR + x by A80; then
bcR = x by ALGSTR_0:def 4; then
b + c in {x} by TARSKI:def 1;
hence contradiction by A97,XBOOLE_0:def 5;
end;
thus
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + x) + cR by A80,A81,A90,A94,Def4
.= aR + (x + cR) by RLVECT_1:def 3
.= addR(a1,bc) by A98,A96,A77,A95,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
end;
suppose
A100: (ADDR).(a1,x) <> x;
A101: a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5
.= aR + x by A79,A77,A100,Def4; then
A102: a + b <> o by A1; then
not a + b in {o} by TARSKI:def 1; then
A103: a + b in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider ab = a + b as Element of C by Def8;
reconsider abR = a + b as Element of F by A103;
per cases;
suppose
A104: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A105: (ADDR).(x,x) = x;
A106: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A105,A104,A79,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc = b + c as Element of C by XBOOLE_0:def 3;
A107: now assume (ADDR).(ab,x) = x; then
x = (aR + x) + x by A101
.= aR + (x + x) by RLVECT_1:def 3
.= aR + x by A105;
hence contradiction by A100;
end;
thus (a+b)+c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + x) + x by A101,A1,A104,A107,Def4
.= aR + (x + x) by RLVECT_1:def 3
.= addR(a1,bc) by A105,A100,A77,A106,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A109: (ADDR).(x,x) <> x;
A110: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= x + x by A109,A104,A79,Def4; then
A111: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A112: b + c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b + c as Element of C by Def8;
reconsider bcR = b + c as Element of F by A112;
A113: (ADDR).(a,bc)=aR + (x + x) by A110
.= (aR + x) + x by RLVECT_1:def 3
.= (ADDR).(ab,x) by A101;
per cases;
suppose
A114: (ADDR).(ab,x) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A102,A104,A114,Def4
.= addR(a1,bc) by A114,A77,A113,A111,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A115: (ADDR).(ab,x) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (ADDR).(ab,x) by A101,A1,A104,A115,Def4
.= addR(a1,bc) by A115,A77,A113,A111,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
end;
suppose
A116: c <> o; then
not c in {o} by TARSKI:def 1; then
A117: c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A117;
per cases;
suppose
A118: (ADDR).(x,c) = x;
A119: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A118,A116,A79,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc = b + c as Element of C by XBOOLE_0:def 3;
A120: (ADDR).(ab,c) = (aR + x) + cR by A101
.= aR + (x + cR) by RLVECT_1:def 3
.= (ADDR).(a,x) by A118;
per cases;
suppose
A121: (ADDR).(ab,c1) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A102,A116,A121,Def4
.= addR(a1,bc) by A121,A77,A119,A120,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A122: (ADDR).(ab,c1) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + x) + cR by A101,A102,A116,A122,Def4
.= aR + (x + cR) by RLVECT_1:def 3
.= addR(a1,bc) by A119,A100,A77,A118,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
suppose
A123: (ADDR).(x,c) <> x;
A124: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= x + cR by A123,A116,A79,Def4; then
A125: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A126: b + c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b + c as Element of C by Def8;
reconsider bcR = b + c as Element of F by A126;
A127: (ADDR).(a,bc) = aR + (x + cR) by A124
.= (aR + x) + cR by RLVECT_1:def 3
.= (ADDR).(ab,c) by A101;
per cases;
suppose
A128: (ADDR).(ab,c1) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A102,A116,A128,Def4
.= addR(a1,bc) by A128,A77,A125,A127,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A129: (the addF of F).(ab,c1) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + x) + cR by A101,A102,A116,A129,Def4
.= aR + (x + cR) by RLVECT_1:def 3
.= addR(a1,bc) by A129,A77,A124,A127,A125,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
end;
end;
end;
suppose
A130: b <> o; then
not b in {o} by TARSKI:def 1; then
A131: b in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider b1 = b as Element of C by Def8;
reconsider bR = b as Element of F by A131;
A132: now assume x = x + x; then
x = 0.F by RLVECT_1:9;
hence contradiction by Def2;
end;
per cases;
suppose
A134: (ADDR).(a,b) = x;
A135: a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5
.= o by A134,A130,A77,Def4; then
a + b in {o} by TARSKI:def 1; then
reconsider ab = a + b as Element of C by XBOOLE_0:def 3;
A136: now assume bR + x = x; then
A138: bR + x = aR + bR by A134
.= bR + aR;
x = aR by A138,ALGSTR_0:def 4; then
a in {x} by TARSKI:def 1;
hence contradiction by A78,XBOOLE_0:def 5;
end;
per cases;
suppose
A139: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A140: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + x by A136,A139,A130,Def4; then
A141: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A142: b + c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b + c as Element of C by Def8;
reconsider bcR = b + c as Element of F by A142;
A143: now assume (ADDR).(a,bc) = x; then
x = aR + (bR + x) by A140
.= (aR + bR) + x by RLVECT_1:def 3
.= x + x by A134;
hence contradiction by A132;
end;
thus
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + bR) + x by A134,A135,A139,A132,Def4
.= aR + (bR + x) by RLVECT_1:def 3
.= addR(a1,bc) by A77,A141,A140,A143,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A145: c <> o; then
not c in {o} by TARSKI:def 1; then
A146: c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A146;
per cases;
suppose
A147: (ADDR).(b,c) <> x;
A148: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + cR by A145,A130,A147,Def4; then
A149: b + c <> o by A1;
not b + c in {o} by A149,TARSKI:def 1; then
A150: b + c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b+c as Element of C by Def8;
reconsider bcR = b+c as Element of F by A150;
per cases;
suppose
A151: (ADDR).(x,c) <> x;
A152: now assume (ADDR).(a,bc) = x; then
x = aR + (bR + cR) by A148
.=(aR + bR) + cR by RLVECT_1:def 3
.= x + cR by A134;
hence contradiction by A151;
end;
thus
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + bR) + cR by A134,A135,A145,A151,Def4
.= aR + (bR + cR) by RLVECT_1:def 3
.= addR(a1,bc) by A77,A148,A149,A152,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A154: (ADDR).(x,c) = x;
A155: aR + (bR + cR) = (aR + bR) + cR by RLVECT_1:def 3
.= x by A134,A154;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A154,A135,A145,Def4
.= addR(a1,bc) by A155,A77,A149,A148,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
suppose
A156: (ADDR).(b,c) = x; then
A157: bR + cR = aR + bR by A134 .= bR + aR;
A158: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A130,A145,A156,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc = b+c as Element of C by XBOOLE_0:def 3;
A159: x + cR = aR + x by A157,ALGSTR_0:def 4
.= (ADDR).(a,x);
per cases;
suppose
A160: (ADDR).(x,c) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= x + cR by A135,A145,A160,Def4
.= addR(a1,bc) by A77,A159,A160,A158,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A161: (ADDR).(x,c) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A135,A145,A161,Def4
.= addR(a1,bc) by A77,A159,A161,A158,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
end;
end;
suppose
A162: (ADDR).(a,b) <> x;
A163: a + b = (addR(x,o)).(a1,b1) by Def8
.= addR(a1,b1) by Def5
.= aR + bR by A162,A130,A77,Def4; then
A164: a + b <> o by A1; then
not a + b in {o} by TARSKI:def 1; then
A165: a + b in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider ab = a + b as Element of C by Def8;
reconsider abR = a + b as Element of F by A165;
per cases;
suppose
A166: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A167: (ADDR).(b,x) <> x;
A168: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + x by A166,A130,A167,Def4; then
A169: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1;then
A170: b + c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b+c as Element of C by Def8;
reconsider bcR = b+c as Element of F by A170;
A171: (ADDR).(ab,x)=(aR + bR) + x by A163
.= aR + (bR + x) by RLVECT_1:def 3
.= (the addF of F).(a,bc) by A168;
per cases;
suppose
A172: (ADDR).(ab,x) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + bR) + x by A1,A163,A166,A172,Def4
.= aR + (bR + x) by RLVECT_1:def 3
.= addR(a1,bc) by A77,A168,A169,A171,A172,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A173: (ADDR).(ab,x) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A164,A166,A173,Def4
.= addR(a1,bc) by A77,A173,A169,A171,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
suppose
A174: (ADDR).(b,x) = x;
A175: b + c =(addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A166,A130,A174,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc = b+c as Element of C by XBOOLE_0:def 3;
A176: (aR + bR) + x = aR + (bR + x) by RLVECT_1:def 3
.= (the addF of F).(a,x) by A174;
per cases;
suppose
A177: (ADDR).(ab,x) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + bR) + x by A163,A1,A166,A177,Def4
.= addR(a1,bc) by A163,A77,A177,A175,A176,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A178: (ADDR).(ab,x) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A164,A166,A178,Def4
.= addR(a1,bc) by A163,A77,A178,A175,A176,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
end;
suppose
A179: c <> o; then
not c in {o} by TARSKI:def 1; then
A180: c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A180;
per cases;
suppose
A181: (ADDR).(b,c) <> x;
A182: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + cR by A179,A130,A181,Def4; then
A183: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A184: b + c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b+c as Element of C by Def8;
reconsider bcR = b+c as Element of F by A184;
A185: (ADDR).(ab,c) = (aR + bR) + cR by A163
.= aR + (bR + cR) by RLVECT_1:def 3
.= (ADDR).(a,bc) by A182;
per cases;
suppose
A186: (ADDR).(ab,c) <> x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + bR) + cR by A163,A164,A179,A186,Def4
.= aR + (bR + cR) by RLVECT_1:def 3
.= addR(a1,bc) by A183,A77,A186,A182,A185,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A187: (ADDR).(ab,c) = x;
thus (a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A164,A179,A187,Def4
.= addR(a1,bc) by A183,A77,A187,A185,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
suppose
A188: (ADDR).(b,c) = x;
A189: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A130,A179,A188,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc = b+c as Element of C by XBOOLE_0:def 3;
A190: (aR + bR) + cR = aR + (bR + cR) by RLVECT_1:def 3
.= (ADDR).(a,x) by A188;
per cases;
suppose
A191: (ADDR).(ab,c) <> x;
thus
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= (aR + bR) + cR by A163,A164,A179,A191,Def4
.= addR(a1,bc) by A77,A163,A189,A190,A191,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
suppose
A192: (ADDR).(ab,c) = x;
thus
(a + b) + c = (addR(x,o)).(ab,c1) by Def8
.= addR(ab,c1) by Def5
.= o by A164,A179,A192,Def4
.= addR(a1,bc) by A163,A77,A192,A189,A190,Def4
.= (addR(x,o)).(a,bc) by Def5
.= a + (b + c) by Def8;
end;
end;
end;
end;
end;
end;
end;
hence ExField(x,o) is add-associative
by RLVECT_1:def 3;
end;
registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
cluster ExField(x,o) -> commutative;
coherence
proof
A1: [#]ExField(x,o) = carr(x,o) by Def8;
now let a,b be Element of ExField(x,o);
per cases;
suppose
A2: b = o; then
b in {o} by TARSKI:def 1; then
reconsider b1 = b as Element of carr(x,o) by XBOOLE_0:def 3;
per cases;
suppose
A3: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of carr(x,o) by XBOOLE_0:def 3;
thus
a * b = b * a by A3,A2;
end;
suppose
A4: a <> o; then
not a in {o} by TARSKI:def 1; then
A5: a in [#]F \ {x} by A1,XBOOLE_0:def 3;
reconsider a1 = a as Element of carr(x,o) by Def8;
reconsider aR = a as Element of F by A5;
A6: (the multF of F).(a1,x) = aR * x
.= x * aR by GROUP_1:def 12
.= (the multF of F).(x,a1);
per cases;
suppose
A7: (the multF of F).(a,x) <> x;
thus a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= (the multF of F).(a,x) by A7,A4,A2,Def6
.= multR(b1,a1) by A6,A7,A4,A2,Def6
.= (multR(x,o)).(b1,a1) by Def7
.= b * a by Def8;
end;
suppose
A8: (the multF of F).(a,x) = x;
thus a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= o by A8,A4,A2,Def6
.= multR(b1,a1) by A6,A8,A4,A2,Def6
.= (multR(x,o)).(b1,a1) by Def7
.= b * a by Def8;
end;
end;
end;
suppose
A9: b <> o; then
not b in {o} by TARSKI:def 1; then
A10: b in [#]F \ {x} by A1,XBOOLE_0:def 3;
reconsider b1 = b as Element of carr(x,o) by Def8;
per cases;
suppose
A11: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of carr(x,o) by XBOOLE_0:def 3;
reconsider bR = b as Element of F by A10;
A12: (the multF of F).(x,b1) = x*bR .= bR*x by GROUP_1:def 12
.= (the multF of F).(b1,x);
per cases;
suppose
A13: (the multF of F).(x,b) <> x;
thus a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= (the multF of F).(x,b) by A13,A11,A9,Def6
.= multR(b1,a1) by A12,A13,A11,A9,Def6
.= (multR(x,o)).(b1,a1) by Def7
.= b * a by Def8;
end;
suppose
A14: (the multF of F).(x,b) = x;
thus a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= o by A14,A11,A9,Def6
.= multR(b1,a1) by A12,A14,A11,A9,Def6
.= (multR(x,o)).(b1,a1) by Def7
.= b * a by Def8;
end;
end;
suppose
A15: a <> o; then
not a in {o} by TARSKI:def 1; then
A16: a in [#]F \ {x} by A1,XBOOLE_0:def 3;
reconsider a1 = a as Element of carr(x,o) by Def8;
reconsider aR = a, bR = b as Element of [#]F by A10,A16;
A17: (the multF of F).(a,b) = aR * bR
.= bR * aR by GROUP_1:def 12
.= (the multF of F).(b,a);
per cases;
suppose
A18: (the multF of F).(a,b) <> x;
thus a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= (the multF of F).(a,b) by A18,A15,A9,Def6
.= multR(b1,a1) by A17,A18,A15,A9,Def6
.= (multR(x,o)).(b1,a1) by Def7
.= b * a by Def8;
end;
suppose
A19: (the multF of F).(a,b) = x;
thus a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= o by A19,A15,A9,Def6
.= multR(b1,a1) by A17,A19,A15,A9,Def6
.= (multR(x,o)).(b1,a1) by Def7
.= b * a by Def8;
end;
end;
end;
end;
hence thesis;
end;
end;
theorem Th9:
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is well-unital
proof
let x be non trivial Element of F;
let u be object;
assume not u in [#]F; then
A1: for a being Element of F holds a <> u;
set C = carr(x,u);
set E = ExField(x,u);
A2: [#]E = C by Def8;
now let a be Element of E;
A3: 1.E = 1.F by Def8;
1.F <> x by Def2; then
not 1.F in {x} by TARSKI:def 1; then
1.F in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider o = 1.F as Element of C by XBOOLE_0:def 3;
A4: o <> u by A1;
per cases;
suppose
A5: a = u; then
a in {u} by TARSKI:def 1; then
reconsider a1 = a as Element of C by XBOOLE_0:def 3;
A6: (the multF of F).(x,1.F) = x * 1.F .= x;
thus a * 1.E = (multR(x,u)).(a1,o) by A3,Def8
.= multR(a1,o) by Def7 .= a by A6,A4,A5,Def6;
A7: (the multF of F).(1.F,x) = 1.F * x .= x;
thus 1.E * a = (multR(x,u)).(o,a1) by A3,Def8
.= multR(o,a1) by Def7 .= a by A7,A4,A5,Def6;
end;
suppose
A8: a <> u; then
not a in {u} by TARSKI:def 1; then
A9: a in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider a1 = a as Element of C by Def8;
reconsider aR = a as Element of [#]F by A9;
A10: (the multF of F).(a,o) = aR * 1.F .= aR;
A11: not aR in {x} by A9,XBOOLE_0:def 5; then
A12: (the multF of F).(a,o) <> x by A10,TARSKI:def 1;
thus
a * 1.E = (multR(x,u)).(a1,o) by A3,Def8 .= multR(a1,o) by Def7
.= aR * 1.F by A12,A4,A8,Def6 .= a;
(the multF of F).(o,a) = 1.F * aR .= aR; then
A13: (the multF of F).(o,a) <> x by A11,TARSKI:def 1;
thus
1.E * a = (multR(x,u)).(o,a1) by A3,Def8 .= multR(o,a1) by Def7
.= 1.F * aR by A13,A4,A8,Def6 .= a;
end;
end;
hence ExField(x,u) is well-unital;
end;
theorem Th10:
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is associative
proof
let x be non trivial Element of F;
let o be object;
assume not o in [#]F; then
A1: a <> o;
set C = carr(x,o), E = ExField(x,o);
set MULTR = the multF of F;
A2: [#]E = C by Def8;
now let a,b,c be Element of E;
per cases;
suppose
A3: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A4: b = o; then
b in {o} by TARSKI:def 1; then
reconsider b1 = b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A5: (MULTR).(x,x) <> x;
A6: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= x * x by A5,A4,A3,Def6;
not x * x in {x} by A5,TARSKI:def 1; then
x * x in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider xx = x * x as Element of C by XBOOLE_0:def 3;
A7: xx <> o by A1;
per cases;
suppose
A8: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A9: (a * b) * c = (multR(x,o)).(a*b,c1) by Def8
.= multR(xx,c1) by A6,Def7;
A10: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7 .= x * x by A4,A5,A8,Def6;
A11: (MULTR).(x,xx) = x * (x * x)
.= (x * x) * x by GROUP_1:def 3;
per cases;
suppose
A12: (MULTR).(xx,x) <> x;
hence (a * b) * c = (x * x) * x by A8,A1,A9,Def6
.= multR(a1,xx) by A3,A11,A12,A1,Def6
.= (multR(x,o)).(a1,xx) by Def7
.= a * (b * c) by A10,Def8;
end;
suppose
A13: (MULTR).(xx,x) = x;
hence (a * b) * c = o by A9,A7,A8,Def6
.= multR(a1,xx) by A7,A11,A13,A3,Def6
.= (multR(x,o)).(a1,xx) by Def7
.= a * (b * c) by A10,Def8;
end;
end;
suppose
A14: c <> o; then
not c in {o} by TARSKI:def 1; then
c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider cR = c as Element of F;
reconsider c1 = c as Element of C by Def8;
A15: (a * b) * c = (multR(x,o)).(a*b,c1) by Def8
.= multR(xx,c1) by A6,Def7;
A16: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7; then
reconsider bc = b * c as Element of C;
per cases;
suppose
A17: (MULTR).(x,c1) <> x; then
A18: b * c = x * cR by A16,A14,A4,Def6; then
A19: b * c <> o by A1;
per cases;
suppose (MULTR).(xx,c1) <> x; then
A20: (a * b) * c = (x * x) * cR by A7,A15,A14,Def6
.= x * (x * cR) by GROUP_1:def 3
.= (MULTR).(x,b*c) by A17,A16,A14,A4,Def6;
per cases;
suppose (MULTR).(x,bc) <> x;
hence (a * b) * c = multR(a1,bc) by A18,A1,A3,Def6,A20
.= (multR(x,o)).(a1,b*c) by Def7
.= a * (b * c) by Def8;
end;
suppose
A21: (MULTR).(x,bc) = x;
A22: (MULTR).(x,bc) = x * (x * cR) by A17,A16,A14,A4,Def6
.= (x * x) * cR by GROUP_1:def 3
.= (MULTR).(xx,c1);
thus
(a * b) * c = o by A15,A7,A14,A22,A21,Def6
.= multR(a1,bc) by A3,A19,A21,Def6
.= (multR(x,o)).(a1,b*c) by Def7
.= a * (b * c) by Def8;
end;
end;
suppose
A23: (MULTR).(xx,c1) = x; then
A24: (a * b) * c = o by A7,A15,A14,Def6;
per cases;
suppose (MULTR).(x,bc) <> x;
A25: (MULTR).(x,bc) = x * (x * cR) by A17,A16,A14,A4,Def6
.= (x * x) * cR by GROUP_1:def 3
.= (MULTR).(xx,c1);
thus
(a * b) * c = multR(a1,bc) by A25,A23,A19,A3,Def6,A24
.= (multR(x,o)).(a1,b*c) by Def7 .= a * (b * c) by Def8;
end;
suppose
A26: (MULTR).(x,bc) = x;
A27: (MULTR).(x,bc) = x * (x * cR) by A17,A16,A14,A4,Def6
.= (x * x) * cR by GROUP_1:def 3
.= (MULTR).(xx,c1);
thus
(a * b) * c = o by A15,A7,A14,A27,A26,Def6
.= multR(a1,bc) by A19,A26,A3,Def6
.= (multR(x,o)).(a1,b*c) by Def7 .= a * (b * c) by Def8;
end;
end;
end;
suppose
A28: (MULTR).(x,c1) = x;
A29: x <> 0.F by Def2;
A30: x = x * cR by A28 .= cR * x by GROUP_1:def 12;
A31: cR = cR * 1_F .= cR * (x * x") by A29,VECTSP_2:9
.= x * x" by A30,GROUP_1:def 3 .= 1_F by A29,VECTSP_2:9;
A32: b * c = o by A28,A16,A14,A4,Def6;
per cases;
suppose (MULTR).(xx,c1) <> x;
hence (a * b) * c = (x * x) * cR by A15,A7,A14,Def6
.= multR(a1,bc) by A31,A32,A5,A3,Def6
.= (multR(x,o)).(a1,b*c) by Def7 .= a * (b * c) by Def8;
end;
suppose (MULTR).(xx,c1) = x; then
x = (x * x) * cR .= x * x by A31;
hence (a * b) * c = a * (b * c) by A5;
end;
end;
end;
end;
suppose
A34: (MULTR).(x,x) = x;
A35: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= o by A34,A4,A3,Def6; then
a * b in {o} by TARSKI:def 1; then
reconsider ab = a * b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A36: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A37: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7 .= o by A34,A36,A4,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b * c as Element of C by XBOOLE_0:def 3;
thus
(a * b) * c = a * (b * c) by A35,A36,A37,A3;
end;
suppose
A38: c <> o; then
not c in {o} by TARSKI:def 1; then
c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider cR = c as Element of F;
reconsider c1 = c as Element of C by Def8;
per cases;
suppose
A39: (MULTR).(x,c1) = x;
A40: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7 .= o by A39,A38,A4,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b * c as Element of C by XBOOLE_0:def 3;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A39,A35,A38,Def6
.= multR(a1,bc) by A40,A34,A3,Def6
.= (multR(x,o)).(a1,b*c) by Def7 .= a * (b * c) by Def8;
end;
suppose
A41: (MULTR).(x,c1) <> x;
A42: b * c = (multR(x,o)).(b1,c1) by Def8.= multR(b1,c1) by Def7
.= x * cR by A41,A38,A4,Def6; then
b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
b * c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider bcR = b * c as Element of F;
reconsider bc = b*c as Element of C by Def8;
A43: (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (MULTR).(x,c1) by A35,A38,A41,Def6;
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (x * x) * cR by A34,A35,A38,A41,Def6
.= x * (x * cR) by GROUP_1:def 3 .= (MULTR).(x,bc) by A42;
hence
(a * b) * c = multR(a1,bc) by A41,A43,A42,A1,A3,Def6
.= (multR(x,o)).(a1,b*c) by Def7 .= a * (b * c) by Def8;
end;
end;
end;
end;
suppose
A44: b <> o; then
not b in {o} by TARSKI:def 1; then
b in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider bR = b as Element of F;
reconsider b1 = b as Element of C by Def8;
A45: (MULTR).(x,b) = x * bR .= bR * x by GROUP_1:def 12
.= (MULTR).(b,x);
per cases;
suppose
A46: (MULTR).(x,b) <> x;
A47: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= x * bR by A46,A44,A3,Def6; then
A48: a * b <> o by A1; then
not a * b in {o} by TARSKI:def 1; then
a * b in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider abR = a * b as Element of F;
reconsider ab = a*b as Element of C by Def8;
per cases;
suppose
A49: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A50: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= bR * x by A45,A46,A49,A44,Def6; then
A51: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
b * c in [#]F \ {x} by A2,XBOOLE_0:def 3;then
reconsider bcR = b * c as Element of F;
reconsider bc = b*c as Element of C by Def8;
A52: (MULTR).(ab,x) = (x * bR) * x by A47
.= x * (bR * x) by GROUP_1:def 3;
per cases;
suppose
A53: (MULTR).(ab,x) <> x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (MULTR).(ab,x) by A47,A1,Def6,A49,A53
.= multR(a1,bc) by A53,A52,A50,A1,A3,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
suppose
A54: (MULTR).(ab,x) = x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A48,A49,A54,Def6
.= multR(a1,bc) by A54,A52,A50,A51,A3,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
end;
suppose
A55: c <> o; then
not c in {o} by TARSKI:def 1; then
c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider cR = c as Element of F;
reconsider c1 = c as Element of C by Def8;
A56: (MULTR).(ab,c) = (x * bR) * cR by A47
.= x * (bR * cR) by GROUP_1:def 3;
per cases;
suppose
A57: (MULTR).(b,c) <> x;
A58: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= bR * cR by A57,A55,A44,Def6; then
A59: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
b * c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider bcR = b * c as Element of F;
reconsider bc = b*c as Element of C by Def8;
per cases;
suppose
A60: (MULTR).(ab,c1) <> x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (x * bR) * cR by A47,A60,A55,A48,Def6
.= x * (bR * cR) by GROUP_1:def 3
.= multR(a1,bc) by A3,A56,A60,A58,A1,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
suppose
A61: (MULTR).(ab,c1) = x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A61,A55,A48,Def6
.= multR(a1,bc) by A3,A56,A61,A58,A59,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
end;
suppose
A62: (MULTR).(b,c) = x;
A63: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= o by A62,A55,A44,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b * c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A64: (MULTR).(ab,c1) <> x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (x * bR) * cR by A47,A64,A55,A48,Def6
.= x * (bR * cR) by GROUP_1:def 3
.= multR(a1,bc) by A62,A3,A56,A64,A63,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
suppose
A65: (MULTR).(ab,c1) = x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A65,A55,A48,Def6
.= multR(a1,bc) by A62,A3,A56,A65,A63,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
end;
end;
end;
suppose
A66: (MULTR).(x,b) = x;
A67: x <> 0.F by Def2;
A68: x = x * bR by A66 .= bR * x by GROUP_1:def 12;
A69: bR = bR * 1_F .= bR * (x * x") by A67,VECTSP_2:9
.= x * x" by A68,GROUP_1:def 3 .= 1_F by A67,VECTSP_2:9;
A70: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= o by A66,A44,A3,Def6; then
a * b in {o} by TARSKI:def 1; then
reconsider ab = a * b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A71: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A72: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= o by A45,A66,A71,A44,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b * c as Element of C by XBOOLE_0:def 3;
thus
(a * b) * c = a * (b * c) by A70,A71,A72,A3;
end;
suppose
A73: c <> o; then
not c in {o} by TARSKI:def 1; then
A74: c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider cR = c as Element of F;
reconsider c1 = c as Element of C by Def8;
A75: bR <> 0.F by A69;
A76: now assume (MULTR).(b,c) = x; then
bR * cR = x * bR by A66 .= bR * x by GROUP_1:def 12; then
cR = x by A75,ALGSTR_0:def 36,ALGSTR_0:def 20; then
c in {x} by TARSKI:def 1;
hence contradiction by A74,XBOOLE_0:def 5;
end;
A78: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7 .= bR * cR by A76,A73,A44,Def6; then
A79: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
b * c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider bcR = b * c as Element of F;
reconsider bc = b*c as Element of C by Def8;
A80: x * (bR * cR) = (x * bR) * cR by GROUP_1:def 3
.= x * cR by A66;
per cases;
suppose
A81: (MULTR).(x,c1) <> x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (MULTR).(x,c1) by A70,A81,A73,Def6
.= multR(a1,bc) by A80,A3,A81,A78,A1,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
suppose
A82: (MULTR).(x,c1) = x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A82,A73,A70,Def6
.= multR(a1,bc) by A79,A82,A80,A3,A78,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
end;
end;
end;
end;
suppose
A83: a <> o; then
not a in {o} by TARSKI:def 1; then
A84: a in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider aR = a as Element of F;
reconsider a1 = a as Element of C by Def8;
per cases;
suppose
A85: b = o; then
b in {o} by TARSKI:def 1; then
reconsider b1 = b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A86: (MULTR).(a1,x) = x;
A87: x <> 0.F by Def2;
aR = aR * 1_F .= aR * (x * x") by A87,VECTSP_2:9
.= (aR * x) * x" by GROUP_1:def 3
.= 1_F by A86,A87,VECTSP_2:9; then
A88: aR <> 0.F;
A89: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= o by A86,A85,A83,Def6; then
a * b in {o} by TARSKI:def 1; then
reconsider ab = a * b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A90: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A91: (MULTR).(x,x) = x;
A92: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= o by A90,A85,A91,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b * c as Element of C by XBOOLE_0:def 3;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A89,A90,A91,Def6
.= multR(a1,bc) by A86,A83,A92,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A93: (MULTR).(x,x) <> x;
A94: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= x * x by A93,A90,A85,Def6; then
A95: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
A96: b * c in [#]F \ {x} by A2,XBOOLE_0:def 3; then
reconsider bcR = b * c as Element of F;
reconsider bc = b*c as Element of C by Def8;
A97: (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (aR * x) * x by A86,A89,A90,A93,Def6;
now assume (MULTR).(a1,bc) = x; then
aR * bcR = aR * x by A86; then
bcR = x by A88,ALGSTR_0:def 36,ALGSTR_0:def 20; then
b * c in {x} by TARSKI:def 1;
hence contradiction by A96,XBOOLE_0:def 5;
end; then
(MULTR).(a1,bc) = multR(a1,bc) by A83,A95,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
hence a * (b * c) = aR * (x * x) by A94
.= (a * b) * c by A97,GROUP_1:def 3;
end;
end;
suppose
A99: c <> o; then
not c in {o} by TARSKI:def 1; then
A100: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A100;
per cases;
suppose
A101: (MULTR).(x,c) = x;
A102: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= o by A101,A99,A85,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b * c as Element of C by XBOOLE_0:def 3;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A89,A99,A101,Def6
.= multR(a1,bc) by A86,A83,A102,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A103: (MULTR).(x,c) <> x;
A104: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= x * cR by A103,A99,A85,Def6; then
A105: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
A106: b * c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc = b * c as Element of C by Def8;
reconsider bcR = b * c as Element of F by A106;
A107: now assume (MULTR).(a1,bc) = x; then
aR * bcR = aR * x by A86; then
bcR = x by A88,ALGSTR_0:def 36,ALGSTR_0:def 20; then
b * c in {x} by TARSKI:def 1;
hence contradiction by A106,XBOOLE_0:def 5;
end;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (aR * x) * cR by A86,A89,A99,A103,Def6
.= aR * (x * cR) by GROUP_1:def 3
.= multR(a1,bc) by A107,A105,A83,A104,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
end;
suppose
A109: (MULTR).(a1,x) <> x;
A110: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= aR * x by A85,A83,A109,Def6; then
A111: a * b <> o by A1; then
not a * b in {o} by TARSKI:def 1; then
A112: a * b in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ab = a * b as Element of C by Def8;
reconsider abR = a * b as Element of F by A112;
per cases;
suppose
A113: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A114: (MULTR).(x,x) = x;
A115: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= o by A114,A113,A85,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b * c as Element of C by XBOOLE_0:def 3;
A116: now assume (MULTR).(ab,x) = x; then
x = (aR * x) * x by A110
.= aR * (x * x) by GROUP_1:def 3
.= aR * x by A114;
hence contradiction by A109;
end;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (aR * x) * x by A110,A1,A113,A116,Def6
.= aR * (x * x) by GROUP_1:def 3
.= multR(a1,bc) by A114,A109,A83,A115,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
suppose
A118: (MULTR).(x,x) <> x;
A119: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= x * x by A118,A113,A85,Def6; then
A120: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
A121: b * c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc = b * c as Element of C by Def8;
reconsider bcR = b * c as Element of F by A121;
A122: (MULTR).(a,bc) = aR * (x * x) by A119
.= (aR * x) * x by GROUP_1:def 3 .= (MULTR).(ab,x) by A110;
per cases;
suppose
A123: (MULTR).(ab,x) = x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A111,A113,A123,Def6
.= multR(a1,bc) by A123,A83,A122,A120,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A124: (MULTR).(ab,x) <> x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (MULTR).(ab,x) by A110,A1,A113,A124,Def6
.= multR(a1,bc) by A124,A83,A122,A120,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
end;
suppose
A125: c <> o; then
not c in {o} by TARSKI:def 1; then
A126: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A126;
per cases;
suppose
A127: (MULTR).(x,c) = x;
A128: b * c = (multR(x,o)).(b1,c1) by Def8 .= multR(b1,c1) by Def7
.= o by A127,A125,A85,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b * c as Element of C by XBOOLE_0:def 3;
A129: (MULTR).(ab,c) = (aR * x) * cR by A110
.= aR * (x * cR) by GROUP_1:def 3 .= (MULTR).(a,x) by A127;
per cases;
suppose
A130: (MULTR).(ab,c1) = x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A111,A125,A130,Def6
.= multR(a1,bc) by A130,A83,A128,A129,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A131: (MULTR).(ab,c1) <> x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= (aR * x) * cR
by A110,A111,A125,A131,Def6
.= aR * (x * cR) by GROUP_1:def 3
.= multR(a1,bc) by A127,A109,A83,A128,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
suppose
A132: (MULTR).(x,c) <> x;
A133: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= x * cR by A132,A125,A85,Def6; then
A134: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
A135: b * c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc = b * c as Element of C by Def8;
reconsider bcR = b * c as Element of F by A135;
A136: (MULTR).(a,bc) = aR * (x * cR) by A133
.= (aR * x) * cR by GROUP_1:def 3
.= (MULTR).(ab,c) by A110;
per cases;
suppose
A137: (MULTR).(ab,c1) = x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A111,A125,A137,Def6
.= multR(a1,bc) by A137,A83,A136,A134,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A138: (MULTR).(ab,c1) <> x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= (aR * x) * cR
by A110,A111,A125,A138,Def6
.= aR * (x * cR) by GROUP_1:def 3
.= multR(a1,bc) by A138,A83,A133,A136,A134,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
end;
end;
end;
end;
suppose
A139: b <> o; then
not b in {o} by TARSKI:def 1; then
A140: b in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider b1 = b as Element of C by Def8;
reconsider bR = b as Element of F by A140;
A141: now assume
A142: x = x * x;
x <> 0.F by Def2; then
A143: x is left_mult-cancelable by ALGSTR_0:def 36;
x * x = x * 1.F by A142;
hence contradiction by A143,ALGSTR_0:def 20,Def2;
end;
per cases;
suppose
A144: (MULTR).(a,b) = x;
A145: a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= o by A144,A139,A83,Def6; then
a * b in {o} by TARSKI:def 1; then
reconsider ab = a * b as Element of C by XBOOLE_0:def 3;
A146: now assume bR = 0.F; then
aR * 0.F = x by A144;
hence contradiction by Def2;
end;
A148: now assume bR * x = x; then
bR * x = aR * bR by A144
.= bR * aR by GROUP_1:def 12; then
x = aR by A146,ALGSTR_0:def 36,ALGSTR_0:def 20; then
a in {x} by TARSKI:def 1;
hence contradiction by A84,XBOOLE_0:def 5;
end;
per cases;
suppose
A150: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A151: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= bR * x by A148,A150,A139,Def6; then
A152: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
A153: b * c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc = b * c as Element of C by Def8;
reconsider bcR = b * c as Element of F by A153;
A154: now assume (MULTR).(a,bc) = x; then
x = aR * (bR * x) by A151
.= (aR * bR) * x by GROUP_1:def 3
.= x * x by A144;
hence contradiction by A141;
end;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= (aR * bR) * x
by A144,A145,A150,A141,Def6
.= aR * (bR * x) by GROUP_1:def 3 .= multR(a1,bc)
by A83,A152,A151,A154,Def6
.= (multR(x,o)).(a,bc) by Def7 .= a * (b * c) by Def8;
end;
suppose
A156: c <> o; then
not c in {o} by TARSKI:def 1; then
A157: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A157;
per cases;
suppose
A158: (MULTR).(b,c) <> x;
A159: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= bR * cR by A156,A139,A158,Def6; then
A160: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
A161: b * c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b*c as Element of C by Def8;
reconsider bcR = b*c as Element of F by A161;
per cases;
suppose
A162: (MULTR).(x,c) <> x;
A163: now assume (MULTR).(a,bc) = x; then
x = aR * (bR * cR) by A159
.= (aR * bR) * cR by GROUP_1:def 3
.= x * cR by A144;
hence contradiction by A162;
end;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= (aR * bR) * cR
by A144,A145,A156,A162,Def6
.= aR * (bR * cR) by GROUP_1:def 3
.= multR(a1,bc) by A83,A163,A159,A160,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A164: (MULTR).(x,c) = x;
A165: aR * (bR * cR) = (aR * bR) * cR by GROUP_1:def 3
.= x by A144,A164;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A164,A145,A156,Def6
.= multR(a1,bc) by A165,A83,A160,A159,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
suppose
A166: (MULTR).(b,c) = x; then
bR * cR = aR * bR by A144
.= bR * aR by GROUP_1:def 12; then
A167: cR = aR by A146,ALGSTR_0:def 36,ALGSTR_0:def 20;
A168: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= o by A156,A139,A166,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b*c as Element of C by XBOOLE_0:def 3;
A169: x * cR = aR * x by A167,GROUP_1:def 12
.= (MULTR).(a,x);
per cases;
suppose
A170: (MULTR).(x,c) <> x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= x * cR by A145,A156,A170,Def6
.= multR(a1,bc) by A83,A169,A170,A168,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A171: (MULTR).(x,c) = x;
thus (a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7 .= o by A145,A156,A171,Def6
.= multR(a1,bc) by A83,A169,A171,A168,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
end;
end;
suppose
A172: (MULTR).(a,b) <> x;
A173: a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= aR * bR by A172,A139,A83,Def6; then
A174: a * b <> o by A1; then
not a * b in {o} by TARSKI:def 1; then
A175: a * b in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ab = a * b as Element of C by Def8;
reconsider abR = a * b as Element of F by A175;
per cases;
suppose
A176: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A177: (MULTR).(b,x) <> x;
A178: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= bR * x by A176,A139,A177,Def6; then
A179: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
A180: b * c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc = b*c as Element of C by Def8;
reconsider bcR = b*c as Element of F by A180;
A181: (MULTR).(ab,x) = (aR * bR) * x by A173
.= aR * (bR * x) by GROUP_1:def 3
.= (MULTR).(a,bc) by A178;
per cases;
suppose
A182: (MULTR).(ab,x) <> x;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (aR * bR) * x by A173,A1,A176,A182,Def6
.= aR * (bR * x) by GROUP_1:def 3
.= multR(a1,bc) by A83,A182,A181,A178,A179,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A183: (MULTR).(ab,x) = x;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= o by A174,A176,A183,Def6
.= multR(a1,bc) by A83,A183,A181,A179,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
suppose
A184: (MULTR).(b,x) = x;
A185: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= o by A176,A139,A184,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b*c as Element of C by XBOOLE_0:def 3;
A186: (aR * bR) * x = aR * (bR * x) by GROUP_1:def 3
.= (MULTR).(a,x) by A184;
per cases;
suppose
A187: (MULTR).(ab,x) <> x;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (aR * bR) * x by A173,A1,A176,A187,Def6
.= multR(a1,bc) by A173,A83,A187,A185,A186,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A188: (MULTR).(ab,x) = x;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= o by A174,A176,A188,Def6
.= multR(a1,bc) by A173,A83,A188,A185,A186,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
end;
suppose
A189: c <> o; then
not c in {o} by TARSKI:def 1; then
A190: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A190;
per cases;
suppose
A191: (MULTR).(b,c) <> x;
A192: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= bR * cR by A189,A139,A191,Def6; then
A193: b * c <> o by A1; then
not b * c in {o} by TARSKI:def 1; then
A194: b * c in [#]F\{x} by A2,XBOOLE_0:def 3;
reconsider bc = b*c as Element of C by Def8;
reconsider bcR = b*c as Element of F by A194;
A195: (MULTR).(ab,c) = (aR * bR) * cR by A173
.= aR * (bR * cR) by GROUP_1:def 3
.= (MULTR).(a,bc) by A192;
per cases;
suppose
A196: (MULTR).(ab,c) <> x;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (aR * bR) * cR by A173,A174,A189,A196,Def6
.= aR * (bR * cR) by GROUP_1:def 3
.= multR(a1,bc)
by A193,A83,A196,A192,A195,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A197: (MULTR).(ab,c) = x;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= o by A174,A189,A197,Def6
.= multR(a1,bc) by A193,A83,A197,A195,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
suppose
A198: (MULTR).(b,c) = x;
A199: b * c = (multR(x,o)).(b1,c1) by Def8
.= multR(b1,c1) by Def7
.= o by A189,A139,A198,Def6; then
b * c in {o} by TARSKI:def 1; then
reconsider bc = b*c as Element of C by XBOOLE_0:def 3;
A200: (aR * bR) * cR
= aR * (bR * cR) by GROUP_1:def 3
.= (MULTR).(a,x) by A198;
per cases;
suppose
A201: (MULTR).(ab,c) <> x;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= (aR * bR) * cR by A173,A174,A189,A201,Def6
.= multR(a1,bc)
by A173,A83,A201,A199,A200,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
suppose
A202: (MULTR).(ab,c) = x;
thus
(a * b) * c = (multR(x,o)).(ab,c1) by Def8
.= multR(ab,c1) by Def7
.= o by A174,A189,A202,Def6
.= multR(a1,bc)
by A173,A83,A202,A199,A200,Def6
.= (multR(x,o)).(a,bc) by Def7
.= a * (b * c) by Def8;
end;
end;
end;
end;
end;
end;
end;
hence ExField(x,o) is associative;
end;
theorem Th11:
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is distributive
proof
let x be non trivial Element of F;
let o be object;
assume not o in [#]F; then
A1: a <> o;
set C = carr(x,o), E = ExField(x,o);
A2: [#]E = C by Def8;
A3: now assume x + x = x; then
x = 0.F by RLVECT_1:9;
hence contradiction by Def2;
end; then
not x + x in {x} by TARSKI:def 1; then
x + x in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider xpx = x + x as Element of C by XBOOLE_0:def 3;
A4: x <> 0.F by Def2; then
A5: x is left_mult-cancelable by ALGSTR_0:def 36;
A6: now assume x * x = x; then
x * x = x * 1.F;
hence contradiction by A5,ALGSTR_0:def 20,Def2;
end; then
not x * x in {x} by TARSKI:def 1; then
x * x in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider xmx = x * x as Element of C by XBOOLE_0:def 3;
A7: x * x <> o by A1;
A8: now assume x * x + x = x; then
x * x = 0.F by RLVECT_1:9; then
x = 0.F by VECTSP_2:def 1;
hence contradiction by Def2;
end; then
not x * x + x in {x} by TARSKI:def 1; then
x * x + x in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider xmxpx = x * x + x as Element of C by XBOOLE_0:def 3;
A9: now let a,b,c be Element of E;
per cases;
suppose
A10: a = o; then
a in {o} by TARSKI:def 1; then
reconsider a1 = a as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A11: b = o; then
b in {o} by TARSKI:def 1; then
reconsider b1 = b as Element of C by XBOOLE_0:def 3;
A12: a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7 .= x * x by A10,A11,A6,Def6;
per cases;
suppose
A13: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A14: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5 .= x + x by A13,A11,A3,Def4;
A15: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= x * x by A13,A10,A6,Def6;
A16: (x * x) + (x * x) = x * (x + x) by VECTSP_1:def 2;
per cases;
suppose
A17: (x * x) + (x * x) <> x;
A18: xpx <> o & xmx <> o by A1;
thus (a * b) + (a * c) = (addR(x,o)).(xmx,xmx) by A15,A12,Def8
.= addR(xmx,xmx) by Def5 .= (x * x) + (x * x) by A18,A17,Def4
.= multR(a1,xpx) by A1,A17,A10,A16,Def6
.= (multR(x,o)).(a1,xpx) by Def7 .= a * (b + c) by A14,Def8;
end;
suppose
A19: (x * x) + (x * x) = x;
A20: xpx <> o & xmx <> o by A1;
thus
(a * b) + (a * c) = (addR(x,o)).(xmx,xmx) by A15,A12,Def8
.= addR(xmx,xmx) by Def5 .= o by A20,A19,Def4
.= multR(a1,xpx) by A20,A19,A10,A16,Def6
.= (multR(x,o)).(a1,xpx) by Def7 .= a * (b + c) by A14,Def8;
end;
end;
suppose
A21: c <> o; then
not c in {o} by TARSKI:def 1; then
A22: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A22;
per cases;
suppose
A23: x + cR = x; then
A24: cR = 0.F by RLVECT_1:9;
A25: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= o by A23,A21,A11,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc1 = b + c as Element of C by XBOOLE_0:def 3;
A26: x * cR <> x by A24,Def2;
A27: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7 .= x * cR by A26,A21,A10,Def6; then
A28: a * c <> o by A1;
reconsider ac1 = a * c as Element of C by Def8;
A29: now assume x * x + x * cR = x; then
x * (x + cR) = x * 1.F by VECTSP_1:def 2; then
x + cR = 1.F by A4,VECTSP_2:8;
hence contradiction by A23,Def2;
end;
thus
(a * b) + (a * c) = (addR(x,o)).(xmx,ac1) by A12,Def8
.= addR(xmx,ac1) by Def5
.= x * x + x * cR by A7,A28,A27,A29,Def4
.= x * x by A23,VECTSP_1:def 2
.= multR(a1,bc1) by A10,A25,A6,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A30: x + cR <> x;
A31: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= x + cR by A30,A21,A11,Def4; then
A32: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A33: b + c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc1 = b + c as Element of C by Def8;
reconsider bcR = b + c as Element of F by A33;
per cases;
suppose
A34: x * cR = x;
A35: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= o by A34,A21,A10,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a * c as Element of C by XBOOLE_0:def 3;
A36: x * (x + cR) <> x by A34,A8,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(xmx,ac1) by A12,Def8
.= addR(xmx,ac1) by Def5 .= x * x + x by A8,A1,A35,Def4
.= x * (x + cR) by A34,VECTSP_1:def 2
.= multR(a1,bc1) by A10,A31,A1,A36,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A37: x * cR <> x;
A38: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7 .= x * cR by A37,A21,A10,Def6; then
A39: a * c <> o by A1; then
not a * c in {o} by TARSKI:def 1; then
A40: a * c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of C by Def8;
reconsider acR = a * c as Element of F by A40;
per cases;
suppose
A41: x * x + x * cR <> x; then
A42: x * (x + cR) <> x by VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(xmx,ac1) by A12,Def8
.= addR(xmx,ac1) by Def5
.= x * x + x * cR by A41,A7,A38,A39,Def4
.= x * (x + cR) by VECTSP_1:def 2
.= multR(a1,bc1) by A42,A10,A31,A1,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A43: x * x + x * cR = x; then
A44: x * (x + cR) = x by VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(xmx,ac1) by A12,Def8
.= addR(xmx,ac1) by Def5 .= o by A43,A7,A38,A39,Def4
.= multR(a1,bc1) by A44,A10,A31,A32,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
end;
end;
suppose
A45: b <> o; then
not b in {o} by TARSKI:def 1; then
A46: b in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider b1 = b as Element of C by Def8;
reconsider bR = b as Element of F by A46;
per cases;
suppose
A47: x * bR = x;
A48: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= o by A10,A45,A47,Def6; then
a * b in {o} by TARSKI:def 1; then
reconsider ab1 = a * b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A49: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A50: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= x * x by A10,A49,A6,Def6;
A51: now assume bR + x = x; then
bR = 0.F by RLVECT_1:9;
hence contradiction by A47,Def2;
end;
A52: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= bR + x by A51,A49,A45,Def4; then
b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A53: b + c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc1 = b + c as Element of C by Def8;
A54: x * (bR + x) = x + x * x by A47,VECTSP_1:def 2;
reconsider bcR = b + c as Element of F by A53;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,xmx) by A50,Def8
.= addR(ab1,xmx) by Def5 .= x + x * x by A8,A48,A1,Def4
.= multR(a1,bc1) by A10,A52,A8,A54,A1,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A55: c <> o; then
not c in {o} by TARSKI:def 1; then
A56: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A56;
per cases;
suppose
A57: bR + cR = x;
A58: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= o by A45,A55,A57,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A59: x * cR = x;
A60: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= o by A10,A55,A59,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a*c as Element of C by XBOOLE_0:def 3;
A61: x * x = x + x
proof
A62: x <> 0.F by Def2;
x * bR = x * 1.F by A47; then
A63: bR = 1.F by A62,VECTSP_2:8;
A64: x * cR = x * 1.F by A59;
A65: x = 1.F + 1.F by A57,A62,A63,A64,VECTSP_2:8;
hence x * x = 1.F * (1.F+1.F) + 1.F * (1.F+1.F)
by VECTSP_1:def 3
.= x + x by A65;
end;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5 .= x + x by A60,A48,A3,Def4
.= multR(a1,bc1) by A61,A10,A58,A6,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A66: x * cR <> x;
A67: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= x * cR by A10,A55,A66,Def6; then
a * c <> o by A1; then
not a*c in {o} by TARSKI:def 1; then
A68: a*c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ac1 = a*c as Element of C by Def8;
reconsider acR = a*c as Element of F by A68;
A69: x * x = x + x * cR by A47,A57,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x + x * cR by A1,A67,A48,A69,A6,Def4
.= multR(a1,bc1) by A69,A10,A58,A6,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
suppose
A70: bR + cR <> x;
A71: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= bR + cR by A45,A55,A70,Def4; then
A72: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A73: b+c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc1 = b+c as Element of C by Def8;
reconsider bcR = b+c as Element of F by A73;
per cases;
suppose
A74: x * cR = x;
A75: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= o by A10,A55,A74,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a*c as Element of C by XBOOLE_0:def 3;
A76: now assume
A77: x * (bR + cR) = x;
A78: x <> 0.F by Def2;
x * 1.F = x * 1.F + x * cR by A47,A77,VECTSP_1:def 2
.= x * (1.F + cR) by VECTSP_1:def 2; then
1.F = 1.F + cR by A78,VECTSP_2:8; then
cR = 0.F by RLVECT_1:9;
hence contradiction by A74,Def2;
end;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5 .= x + x by A3,A75,A48,Def4
.= x * (bR + cR) by A74,A47,VECTSP_1:def 2
.= multR(a1,bc1) by A76,A10,A1,A71,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A79: x * cR <> x;
A80: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= x * cR by A10,A55,A79,Def6; then
A81: a * c <> o by A1; then
not a * c in {o} by TARSKI:def 1; then
A82: a*c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ac1=a*c as Element of C by Def8;
reconsider acR=a*c as Element of F by A82;
A83: x * (bR + cR) = x + x * cR by A47,VECTSP_1:def 2;
per cases;
suppose
A84: x + x * cR = x;
thus (a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A81,A80,A48,A84,Def4
.= multR(a1,bc1) by A84,A83,A10,A71,A72,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A85: x + x * cR <> x;
thus (a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x + x * cR by A1,A80,A48,A85,Def4
.= multR(a1,bc1) by A85,A83,A10,A71,A1,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
end;
end;
suppose
A86: x * bR <> x;
A87: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= x * bR by A10,A45,A86,Def6; then
A88: a * b <> o by A1; then
not a * b in {o} by TARSKI:def 1; then
A89: a * b in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ab1 = a * b as Element of C by Def8;
reconsider abR = a * b as Element of F by A89;
per cases;
suppose
A90: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A91: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= x * x by A10,A90,A6,Def6; then
A92: a * c <> o by A1; then
not a * c in {o} by TARSKI:def 1; then
A93: a * c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of C by Def8;
reconsider acR = a * c as Element of F by A93;
per cases;
suppose
A94: bR + x = x;
A95: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= o by A45,A90,A94,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
A96: x * bR + x * x = x * x by A94,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x * bR + x * x by A87,A88,A91,A92,A96,A6,Def4
.= multR(a1,bc1) by A10,A95,A96,A6,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A97: bR + x <> x;
A98: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= bR + x by A45,A90,A97,Def4; then
A99: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A100: b+c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc1 = b+c as Element of C by Def8;
reconsider bcR = b+c as Element of F by A100;
per cases;
suppose
A101: x * bR + x * x <> x;
A102: x * bR + x * x = x * (bR + x) by VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x * bR + x * x by A87,A88,A91,A92,A101,Def4
.= multR(a1,bc1) by A10,A98,A1,A101,A102,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A103: x * bR + x * x = x;
A104: x * bR + x * x = x * (bR + x) by VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A87,A88,A91,A92,A103,Def4
.= multR(a1,bc1) by A10,A98,A99,A103,A104,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
suppose
A105: c <> o; then
not c in {o} by TARSKI:def 1; then
A106: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A106;
per cases;
suppose
A107: bR + cR = x;
A108: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= o by A45,A105,A107,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
A109: x * bR + x * cR = x * x by A107,VECTSP_1:def 2;
per cases;
suppose
A110: x * cR <> x;
A111: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= x * cR by A10,A105,A110,Def6; then
A112: a * c <> o by A1; then
not a * c in {o} by TARSKI:def 1; then
A113: a*c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ac1=a*c as Element of C by Def8;
reconsider acR=a*c as Element of F by A113;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x * bR + x * cR by A87,A88,A111,A112,A109,A6,Def4
.= multR(a1,bc1) by A10,A108,A6,A109,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A114: x * cR = x;
A115: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= o by A10,A105,A114,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a*c as Element of C by XBOOLE_0:def 3;
A116: now assume x * bR + x = x; then
A117: x * 1.F = x * (bR + cR) by A114,VECTSP_1:def 2;
x <> 0.F by Def2; then
bR + cR = 1.F by A117,VECTSP_2:8;
hence contradiction by A107,Def2;
end;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x * bR + x by A87,A1,A115,A116,Def4
.= multR(a1,bc1) by A10,A108,A6,A109,A114,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
suppose
A118: bR + cR <> x;
A119: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= bR + cR by A45,A105,A118,Def4; then
A120: b + c <> o by A1; then
not b + c in {o} by TARSKI:def 1; then
A121: b+c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider bc1 = b+c as Element of C by Def8;
reconsider bcR = b+c as Element of F by A121;
A122: x * bR + x * cR = x * (bR + cR) by VECTSP_1:def 2;
per cases;
suppose
A123: x * cR <> x;
A124: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= x * cR by A10,A105,A123,Def6; then
A125: a * c <> o by A1; then
not a * c in {o} by TARSKI:def 1; then
A126: a*c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ac1=a*c as Element of C by Def8;
reconsider acR=a*c as Element of F by A126;
per cases;
suppose
A127: x * bR + x * cR <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x * bR + x * cR by A87,A88,A124,A125,A127,Def4
.= multR(a1,bc1) by A10,A119,A1,A127,A122,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A128: x * bR + x * cR = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A87,A88,A124,A125,A128,Def4
.= multR(a1,bc1) by A10,A119,A120,A128,A122,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
suppose
A129: x * cR = x;
A130: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= o by A10,A105,A129,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a*c as Element of C by XBOOLE_0:def 3;
A131: x * bR + x = x * (bR + cR) by A129,VECTSP_1:def 2;
per cases;
suppose
A132: x * bR + x <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x * bR + x by A87,A1,A130,A132,Def4
.= multR(a1,bc1) by A10,A119,A1,A132,A131,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A133: x * bR + x = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A87,A88,A130,A133,Def4
.= multR(a1,bc1) by A10,A119,A120,A133,A131,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
end;
end;
end;
end;
suppose
A134: a <> o; then
not a in {o} by TARSKI:def 1; then
A135: a in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider a1 = a as Element of carr(x,o) by Def8;
reconsider aR = a as Element of [#]F by A135;
per cases;
suppose
A136: b = o; then
b in {o} by TARSKI:def 1; then
reconsider b1 = b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A137: aR * x = x;
A138: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= o by A134,A136,A137,Def6; then
a * b in {o} by TARSKI:def 1; then
reconsider ab1 = a*b as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A139: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A140: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= o by A134,A139,A137,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a*c as Element of C by XBOOLE_0:def 3;
A141: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= x + x by A136,A139,A3,Def4; then
A142: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
A143: aR * (x + x) = x + x by A137,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5 .= x + x by A140,A138,A3,Def4
.= multR(a1,bc1) by A143,A142,A134,A141,A3,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A144: c <> o; then
not c in {o} by TARSKI:def 1; then
A145: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of carr(x,o) by Def8;
reconsider cR = c as Element of [#]F by A145;
A146: now assume
A147: aR * cR = x;
aR <> 0.F by A137,Def2; then
cR = x by A137,A147,VECTSP_2:8; then
cR in {x} by TARSKI:def 1;
hence contradiction by A145,XBOOLE_0:def 5;
end;
A148: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= aR * cR by A134,A144,A146,Def6; then
A149: a * c <> o by A1;
reconsider ac1 = a*c as Element of C by Def8;
per cases;
suppose
A150: x + cR = x; then
A151: aR * x + aR * cR = aR * x by VECTSP_1:def 2;
A152: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= o by A144,A136,A150,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A137,A138,A148,A149,A151,Def4
.= multR(a1,bc1) by A134,A152,A137,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A153: x + cR <> x;
A154: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= x + cR by A136,A144,A153,Def4; then
A155: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
A156: now assume x + aR * cR = x; then
A158: aR * x = aR * (x + cR) by A137,VECTSP_1:def 2;
aR <> 0.F by A137,Def2;
hence contradiction by A153,A158,VECTSP_2:8;
end;
A159: x + aR * cR = aR * (x + cR) by A137,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x + aR * cR by A138,A148,A1,A156,Def4
.= multR(a1,bc1) by A134,A154,A155,A156,A159,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
suppose
A160: aR * x <> x;
A161: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= aR * x by A134,A136,A160,Def6; then
A162: a * b <> o by A1; then
not a * b in {o} by TARSKI:def 1; then
A163: a*b in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ab1 = a * b as Element of C by Def8;
reconsider abR = a * b as Element of F by A163;
per cases;
suppose
A164: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A165: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= aR * x by A134,A164,A160,Def6; then
A166: a * c <> o by A1;
reconsider ac1 = a*c as Element of C by Def8;
A167: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= x + x by A136,A164,A3,Def4; then
A168: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
A169: aR * (x + x) = aR * x + aR * x by VECTSP_1:def 2;
per cases;
suppose
A170: aR * x + aR * x <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= aR * x + aR * x by A161,A165,A166,A170,Def4
.= multR(a1,bc1) by A134,A170,A169,A168,A167,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A171: aR * x + aR * x = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5 .= o by A161,A165,A166,A171,Def4
.= multR(a1,bc1) by A134,A171,A169,A168,A167,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
suppose
A172: c <> o; then
not c in {o} by TARSKI:def 1; then
A173: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of carr(x,o) by Def8;
reconsider cR = c as Element of [#]F by A173;
per cases;
suppose
A174: aR * cR = x;
A175: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= o by A134,A172,A174,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a*c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A176: x + cR = x;
A177: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= o by A136,A172,A176,Def4; then
b+c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
A178: aR * x + x = aR * x by A176,A174,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= aR * x + x by A160,A161,A1,A175,A178,Def4
.= multR(a1,bc1) by A134,A177,A178,A160,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A179: x + cR <> x;
A180: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= x + cR by A136,A172,A179,Def4; then
A181: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
A182: aR * x + x = aR * (x + cR) by A174,VECTSP_1:def 2;
per cases;
suppose
A183: aR * x + x <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= aR * x + x by A161,A1,A175,A183,Def4
.= multR(a1,bc1) by A134,A180,A181,A183,A182,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A184: aR * x + x = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A161,A162,A175,A184,Def4
.= multR(a1,bc1) by A134,A180,A181,A184,A182,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
suppose
A185: aR * cR <> x;
A186: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= aR * cR by A134,A172,A185,Def6; then
A187: a * c <> o by A1;
reconsider ac1 = a*c as Element of C by Def8;
per cases;
suppose
A188: x + cR = x;
A189: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= o by A136,A172,A188,Def4; then
b+c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
A190: aR * x + aR * cR = aR * x by A188,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= aR * x + aR * cR by A160,A161,A162,A186,A187,A190,Def4
.= multR(a1,bc1) by A160,A134,A189,A190,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A191: x + cR <> x;
A192: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= x + cR by A136,A172,A191,Def4; then
A193: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
A194: aR * x + aR * cR = aR * (x + cR) by VECTSP_1:def 2;
per cases;
suppose
A195: aR * x + aR * cR = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A161,A162,A186,A187,A195,Def4
.= multR(a1,bc1) by A134,A192,A193,A195,A194,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A196: aR * x + aR * cR <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= aR * x + aR * cR by A161,A162,A186,A187,A196,Def4
.= multR(a1,bc1) by A134,A192,A193,A196,A194,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
end;
end;
end;
suppose
A197: b <> o; then
not b in {o} by TARSKI:def 1; then
A198: b in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider b1 = b as Element of carr(x,o) by Def8;
reconsider bR = b as Element of [#]F by A198;
per cases;
suppose
A199: aR * bR = x;
A200: a * b = (multR(x,o)).(a1,b1) by Def8 .= multR(a1,b1) by Def7
.= o by A134,A197,A199,Def6; then
a * b in {o} by TARSKI:def 1; then
reconsider ab1 = a * b as Element of C by XBOOLE_0:def 3;
A201: aR * (bR + x) = x + aR * x by A199,VECTSP_1:def 2;
A202: now assume bR + x = x; then
bR = 0.F by RLVECT_1:9;
hence contradiction by A199,Def2;
end;
A203: now assume aR * x = x; then
A205: x * aR = x * 1.F by GROUP_1:def 12;
x <> 0.F by Def2; then
aR = 1.F by A205,VECTSP_2:8; then
bR in {x} by A199,TARSKI:def 1;
hence contradiction by A198,XBOOLE_0:def 5;
end;
per cases;
suppose
A206: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
A207: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= bR + x by A197,A206,A202,Def4; then
A208: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
reconsider bcR = b+c as Element of F by A207;
A209: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= aR * x by A134,A206,A203,Def6; then
A210: a * c <> o by A1; then
not a * c in {o} by TARSKI:def 1; then
A211: a*c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ac1 = a*c as Element of C by Def8;
reconsider acR = a*c as Element of F by A211;
per cases;
suppose
A212: x + aR * x = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5 .= o by A200,A209,A210,A212,Def4
.= multR(a1,bc1) by A201,A134,A207,A208,A212,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A213: x + aR * x <> x;
thus (a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x + aR * x by A200,A209,A1,A213,Def4
.= multR(a1,bc1) by A201,A134,A207,A208,A213,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
suppose
A214: c <> o; then
not c in {o} by TARSKI:def 1; then
A215: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A215;
per cases;
suppose
A216: bR + cR = x;
A217: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= o by A197,A214,A216,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A218: aR * cR = x;
A219: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= o by A134,A214,A218,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a * c as Element of C by XBOOLE_0:def 3;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5 .= x + x by A200,A219,A3,Def4
.= aR * x by A216,A218,A199,VECTSP_1:def 2
.= multR(a1,bc1) by A134,A217,A203,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A220: aR * cR <> x;
A221: a * c = (multR(x,o)).(a1,c1) by Def8 .= multR(a1,c1) by Def7
.= aR * cR by A134,A214,A220,Def6; then
not a * c = o by A1; then
not a * c in {o} by TARSKI:def 1; then
A222: a*c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider ac1 = a * c as Element of C by Def8;
reconsider acR = a * c as Element of F by A222;
A223: x + aR * cR = aR * x by A216,A199,VECTSP_1:def 2;
per cases;
suppose x + aR * cR = x;
hence (a * b)+(a * c) = a * (b + c)
by A203,A216,A199,VECTSP_1:def 2;
end;
suppose
A225: x + aR * cR <> x;
thus (a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x + aR * cR by A200,A221,A1,A225,Def4
.= multR(a1,bc1) by A134,A217,A225,A223,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
suppose
A226: bR + cR <> x;
A227: b + c = (addR(x,o)).(b1,c1) by Def8 .= addR(b1,c1) by Def5
.= bR + cR by A197,A214,A226,Def4; then
A228: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
per cases;
suppose
A229: aR * cR = x;
A230: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7 .= o by A134,A214,A229,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a * c as Element of C by XBOOLE_0:def 3;
A231: aR * (bR + cR) = x + x by A229,A199,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5 .= x + x by A200,A230,A3,Def4
.= multR(a1,bc1) by A3,A231,A134,A228,A227,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A232: aR * cR <> x;
A233: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= aR * cR by A134,A214,A232,Def6; then
A234: not a * c = o by A1;
reconsider ac1 = a * c as Element of C by Def8;
A235: x + aR * cR = aR * (bR + cR) by A199,VECTSP_1:def 2;
per cases;
suppose
A236: x + aR * cR = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A200,A233,A234,A236,Def4
.= multR(a1,bc1) by A134,A227,A228,A236,A235,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
suppose
A237: x + aR * cR <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= x + aR * cR by A200,A233,A1,A237,Def4
.= multR(a1,bc1) by A134,A227,A228,A237,A235,Def6
.= (multR(x,o)).(a1,bc1) by Def7 .= a * (b + c) by Def8;
end;
end;
end;
end;
end;
suppose
A238: aR * bR <> x;
A239: a * b = (multR(x,o)).(a1,b1) by Def8
.= multR(a1,b1) by Def7
.= aR * bR by A134,A197,A238,Def6; then
A240: a * b <> o by A1;
reconsider ab1 = a * b as Element of C by Def8;
reconsider abR = a * b as Element of F by A239;
per cases;
suppose
A241: c = o; then
c in {o} by TARSKI:def 1; then
reconsider c1 = c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A242: bR + x <> x;
A243: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + x by A197,A241,A242,Def4; then
A244: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
per cases;
suppose
A245: aR * x <> x;
A246: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= aR * x by A134,A241,A245,Def6; then
A247: a * c <> o by A1;
reconsider ac1 = a * c as Element of C by Def8;
A248: aR * bR + aR * x = aR * (bR + x) by VECTSP_1:def 2;
per cases;
suppose
A249: aR * bR + aR * x <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= aR * bR + aR * x by A240,A239,A246,A247,A249,Def4
.= multR(a1,bc1) by A134,A243,A244,A249,A248,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
suppose
A250: aR * bR + aR * x = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A240,A239,A246,A247,A250,Def4
.= multR(a1,bc1) by A134,A243,A244,A250,A248,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
end;
suppose
A251: aR * x = x;
A252: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= o by A134,A241,A251,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a * c as Element of C by XBOOLE_0:def 3;
A253: aR * bR + x = aR * (bR + x) by A251,VECTSP_1:def 2;
per cases;
suppose
A254: aR * bR + x <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= aR * bR + x by A1,A239,A252,A254,Def4
.= multR(a1,bc1) by A134,A243,A244,A254,A253,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
suppose
A255: aR * bR + x = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A240,A239,A252,A255,Def4
.= multR(a1,bc1) by A134,A243,A244,A255,A253,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
end;
end;
suppose
A256: bR + x = x;
A257: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A197,A241,A256,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A258: aR * x <> x;
A259: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= aR * x by A134,A241,A258,Def6; then
A260: a * c <> o by A1;
reconsider ac1 = a * c as Element of C by Def8;
A261: aR * bR + aR * x = aR * x by A256,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= aR * x by A240,A239,A259,A260,A258,A261,Def4
.= multR(a1,bc1) by A258,A134,A257,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
suppose
A262: aR * x = x;
A263: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= o by A134,A241,A262,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a * c as Element of C by XBOOLE_0:def 3;
A264: aR * bR + x = x by A256,A262,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A240,A239,A263,A264,Def4
.= multR(a1,bc1) by A262,A134,A257,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
end;
end;
suppose
A265: c <> o; then
not c in {o} by TARSKI:def 1; then
A266: c in [#]F \ {x} by A2,XBOOLE_0:def 3;
reconsider c1 = c as Element of C by Def8;
reconsider cR = c as Element of F by A266;
A267: aR * bR + aR * cR = aR * (bR + cR) by VECTSP_1:def 2;
per cases;
suppose
A268: bR + cR <> x;
A269: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= bR + cR by A197,A265,A268,Def4; then
A270: b + c <> o by A1;
reconsider bc1 = b+c as Element of C by Def8;
per cases;
suppose
A271: aR * cR <> x;
A272: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= aR * cR by A134,A265,A271,Def6; then
A273: a * c <> o by A1;
reconsider ac1 = a * c as Element of C by Def8;
per cases;
suppose
A274: aR * bR + aR * cR <> x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1)
by Def8
.= addR(ab1,ac1) by Def5
.= aR * bR + aR * cR
by A240,A239,A272,A273,A274,Def4
.= multR(a1,bc1)
by A134,A269,A270,A274,A267,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
suppose
A275: aR * bR + aR * cR = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1) by Def8
.= addR(ab1,ac1) by Def5
.= o by A240,A239,A272,A273,A275,Def4
.= multR(a1,bc1) by A134,A269,A270,A275,A267,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
end;
suppose
A276: aR * cR = x;
A277: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= o by A134,A265,A276,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a * c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A278: aR * bR + x <> x; then
A279: aR * (bR + cR) <> x by A276,VECTSP_1:def 2;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1)
by Def8
.= addR(ab1,ac1) by Def5
.= aR * bR + x by A1,A239,A277,A278,Def4
.= aR * (bR + cR) by A276,VECTSP_1:def 2
.= multR(a1,bc1) by A134,A269,A270,A279,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
suppose
A280: aR * bR + x = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1)
by Def8
.= addR(ab1,ac1) by Def5
.= o by A240,A239,A277,A280,Def4
.= multR(a1,bc1)
by A267,A276,A134,A269,A270,A280,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
end;
end;
suppose
A281: bR + cR = x;
A282: b + c = (addR(x,o)).(b1,c1) by Def8
.= addR(b1,c1) by Def5
.= o by A197,A265,A281,Def4; then
b + c in {o} by TARSKI:def 1; then
reconsider bc1 = b+c as Element of C by XBOOLE_0:def 3;
per cases;
suppose
A283: aR * cR <> x;
A284: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= aR * cR by A134,A265,A283,Def6; then
A285: a * c <> o by A1;
reconsider ac1 = a * c as Element of C by Def8;
per cases;
suppose
A286: aR * bR + aR * cR <> x;
thus
(a * b) + (a * c)= (addR(x,o)).(ab1,ac1)
by Def8
.= addR(ab1,ac1) by Def5
.= aR * bR + aR * cR
by A240,A239,A284,A285,A286,Def4
.= multR(a1,bc1)
by A286,A134,A281,A282,A267,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
suppose
A287: aR * bR + aR * cR = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1)
by Def8
.= addR(ab1,ac1) by Def5
.= o by A240,A239,A284,A285,A287,Def4
.= multR(a1,bc1)
by A287,A134,A281,A282,A267,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
end;
suppose
A288: aR * cR = x;
A289: a * c = (multR(x,o)).(a1,c1) by Def8
.= multR(a1,c1) by Def7
.= o by A134,A265,A288,Def6; then
a * c in {o} by TARSKI:def 1; then
reconsider ac1 = a * c as Element of C by XBOOLE_0:def 3;
A290: aR * bR + x =aR * (bR + cR)
by A288,VECTSP_1:def 2;
per cases;
suppose
A291: aR * bR + x <> x;
thus
(a * b) + (a * c)= (addR(x,o)).(ab1,ac1)
by Def8
.= addR(ab1,ac1) by Def5
.= aR * bR + x by A1,A239,A289,A291,Def4
.= multR(a1,bc1)
by A291,A134,A281,A282,A290,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
suppose
A292: aR * bR + x = x;
thus
(a * b) + (a * c) = (addR(x,o)).(ab1,ac1)
by Def8
.= addR(ab1,ac1) by Def5
.= o by A240,A239,A289,A292,Def4
.= multR(a1,bc1)
by A292,A134,A281,A282,A290,Def6
.= (multR(x,o)).(a1,bc1) by Def7
.= a * (b + c) by Def8;
end;
end;
end;
end;
end;
end;
end;
end;
now let a,b,c be Element of ExField(x,o);
thus
a * (b + c) = (a * b) + (a * c) by A9;
thus
(b + c) * a = a * (b + c) by GROUP_1:def 12
.= (a * b) + (a * c) by A9
.= (b * a) + (a * c) by GROUP_1:def 12
.= (b * a) + (c * a) by GROUP_1:def 12;
end;
hence ExField(x,o) is distributive;
end;
theorem Th12:
for x being non trivial Element of F, o being object st not o in [#]F
holds ExField(x,o) is almost_left_invertible
proof
let x be non trivial Element of F;
let v be object;
assume not v in [#]F; then
A1: a <> v;
x <> 0.F by Def2; then
consider xi being Element of F such that
A2: xi*x = 1.F by ALGSTR_0:def 39,ALGSTR_0:def 27;
A3: [#]ExField(x,v) = carr(x,v) by Def8;
v in {v} by TARSKI:def 1; then
reconsider u1 = v as Element of carr(x,v) by XBOOLE_0:def 3;
reconsider u = u1 as Element of ExField(x,v) by Def8;
now let a be Element of ExField(x,v);
assume
A4: a <> 0.ExField(x,v);
0.F <> x by Def2; then
not 0.F in {x} by TARSKI:def 1; then
0.F in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider o = 0.F as Element of carr(x,v) by XBOOLE_0:def 3;
per cases;
suppose
A5: a = v; then
a in {v} by TARSKI:def 1; then
reconsider a1 = a as Element of carr(x,v) by XBOOLE_0:def 3;
per cases;
suppose
A6: xi = x; then
A7: (the multF of F).(x,x) <> x by A2,Def2;
u * a = (multR(x,v)).(u1,a1) by Def8 .= multR(u1,a1) by Def7
.= (the multF of F).(xi,x) by A7,A6,A5,Def6
.= 1.(ExField(x,v)) by A2,Def8;
hence a is left_invertible by ALGSTR_0:def 27;
end;
suppose xi <> x; then
not xi in {x} by TARSKI:def 1; then
xi in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider x1i = xi as Element of carr(x,v) by XBOOLE_0:def 3;
reconsider b = x1i as Element of ExField(x,v) by Def8;
A8: (the multF of F).(b,x) <> x by A2,Def2;
b * a = (multR(x,v)).(x1i,a1) by Def8 .= multR(x1i,a1) by Def7
.= (the multF of F).(xi,x) by A1,A8,A5,Def6
.= 1.(ExField(x,v)) by A2,Def8;
hence a is left_invertible by ALGSTR_0:def 27;
end;
end;
suppose
A9: a <> v; then
not a in {v} by TARSKI:def 1; then
A10: a in [#]F \ {x} by A3,XBOOLE_0:def 3;
reconsider a1 = a as Element of carr(x,v) by Def8;
reconsider aR = a as Element of [#]F by A10;
aR <> 0.F by A4,Def8; then
consider aRi being Element of F such that
A11: aRi * aR = 1.F by ALGSTR_0:def 39,ALGSTR_0:def 27;
per cases;
suppose
A12: aRi = x; then
A13: (the multF of F).(x,a) <> x by A11,Def2;
u * a = (multR(x,v)).(u1,a1) by Def8 .= multR(u1,a1) by Def7
.= (the multF of F).(aRi,aR) by A13,A12,A9,Def6
.= 1.(ExField(x,v)) by A11,Def8;
hence a is left_invertible by ALGSTR_0:def 27;
end;
suppose aRi <> x; then
not aRi in {x} by TARSKI:def 1; then
aRi in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider a1i = aRi as Element of carr(x,v) by XBOOLE_0:def 3;
reconsider b = a1i as Element of ExField(x,v) by Def8;
A14: (the multF of F).(b,a) <> x by A11,Def2;
A15: aR <> v & aRi <> v by A1;
b * a = (multR(x,v)).(aRi,a1) by Def8 .= multR(a1i,a1) by Def7
.=(the multF of F).(aRi,aR) by A15,A14,Def6
.= 1.(ExField(x,v)) by A11,Def8;
hence a is left_invertible by ALGSTR_0:def 27;
end;
end;
end;
hence ExField(x,v) is almost_left_invertible by ALGSTR_0:def 27;
end;
theorem Th13:
for x being non trivial Element of F, P being Ring
st P = ExField(x,<%0.F,1.F%>) holds <%0.F,1.F%> in [#]P /\ [#]Polynom-Ring P
proof
let x be non trivial Element of F,P be Ring;
set C = carr(x,<%0.F,1.F%>), E = ExField(x,<%0.F,1.F%>);
assume
A1: P = E;
<%0.F,1.F%> in {<%0.F,1.F%>} by TARSKI:def 1; then
<%0.F,1.F%> in C by XBOOLE_0:def 3; then
A2: <%0.F,1.F%> in [#]E by Def8;
now let n be Element of NAT;
per cases by NAT_1:23;
suppose
A3: n = 0;
hence <%0.F,1.F%>.n = 0.F by POLYNOM5:38 .= 0.E by Def8
.= <%0.E,1.E%>.n by A3,POLYNOM5:38;
end;
suppose
A4: n = 1;
hence <%0.F,1.F%>.n = 1.F by POLYNOM5:38 .= 1.E by Def8
.= <%0.E,1.E%>.n by A4,POLYNOM5:38;
end;
suppose
A5: n >= 2;
hence <%0.F,1.F%>.n = 0.F by POLYNOM5:38 .= 0.E by Def8
.= <%0.E,1.E%>.n by A5,POLYNOM5:38;
end;
end; then
<%0.F,1.F%> = <%0.E,1.E%>; then
<%0.F,1.F%> in [#]Polynom-Ring P by A1,POLYNOM3:def 10;
hence thesis by A1,A2,XBOOLE_0:def 4;
end;
theorem Th14:
ex K being Field st [#]K /\ [#]Polynom-Ring K <> {}
proof
set F = the non almost_trivial Field;
set x = the non trivial Element of F;
reconsider o = <%0.F,1.F%> as object;
per cases;
suppose not o in [#]F; then
reconsider K = ExField(x,o) as Field by Th7,Th8,Th10,Th9,Th12,Th11;
take K;
thus thesis by Th13;
end;
suppose
A1: ex a being Element of F st a = <%0.F,1.F%>;
take F;
<%0.F,1.F%> in [#]Polynom-Ring F by POLYNOM3:def 10;
hence thesis by A1,XBOOLE_0:def 4;
end;
end;
reserve n for non zero Nat;
theorem
ex K being Field, p being Polynomial of K
st deg p = n & p in [#]K /\ [#]Polynom-Ring K
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
set F = the non almost_trivial Field;
set x = the non trivial Element of F;
reconsider o = rpoly(n,0.F) as object;
per cases;
suppose not o in [#]F; then
reconsider K = ExField(x,o) as Field by Th7,Th8,Th10,Th9,Th12,Th11;
set p = rpoly(n,0.K);
now let i be Element of NAT;
per cases;
suppose
A1: i = 0;
hence rpoly(n,0.F).i = -power(F).(0.F,n) by HURWITZ:25
.= -0.F by Th6
.= -0.K by Def8
.= -power(K).(0.K,n) by Th6
.= p.i by A1,HURWITZ:25;
end;
suppose
A2: i = n;
hence rpoly(n,0.F).i = 1_F by HURWITZ:25
.= 1_K by Def8
.= p.i by A2,HURWITZ:25;
end;
suppose
A3: i <> 0 & i <> n;
hence rpoly(n,0.F).i = 0.F by HURWITZ:26
.= 0.K by Def8
.= p.i by A3,HURWITZ:26;
end;
end; then
A4: rpoly(n,0.F) = rpoly(n,0.K);
take K;
take p = rpoly(n,0.K);
A5: p in [#]Polynom-Ring K by POLYNOM3:def 10;
p in {rpoly(n,0.F)} by A4,TARSKI:def 1; then
p in carr(x,rpoly(n,0.F)) by XBOOLE_0:def 3; then
p in [#]K by Def8;
hence thesis by A5,XBOOLE_0:def 4,HURWITZ:27;
end;
suppose
A6: ex a being Element of F st a = rpoly(n,0.F);
take F;
take x = rpoly(n,0.F);
x in [#]Polynom-Ring F by POLYNOM3:def 10;
hence thesis by A6,HURWITZ:27,XBOOLE_0:def 4;
end;
end;
theorem
ex K being Field, x being object st not x in rng(canHom K) &
x in [#]K /\ [#]Polynom-Ring K
proof
set F = the non almost_trivial Field;
set y = the non trivial Element of F;
reconsider o = <%0.F,1.F%> as object;
per cases;
suppose not o in [#]F; then
reconsider K = ExField(y,o) as Field by Th7,Th8,Th10,Th9,Th12,Th11;
take K;
take x = <%0.K,1.K%>;
now let n be Element of NAT;
per cases by NAT_1:23;
suppose
A1: n = 0;
hence <%0.F,1.F%>.n = 0.F by POLYNOM5:38 .= 0.K by Def8
.= <%0.K,1.K%>.n by A1,POLYNOM5:38;
end;
suppose
A2: n = 1;
hence <%0.F,1.F%>.n = 1.F by POLYNOM5:38 .= 1.K by Def8
.= <%0.K,1.K%>.n by A2,POLYNOM5:38;
end;
suppose
A3: n >= 2;
hence <%0.F,1.F%>.n = 0.F by POLYNOM5:38 .= 0.K by Def8
.= <%0.K,1.K%>.n by A3,POLYNOM5:38;
end;
end; then
A4: <%0.F,1.F%> = <%0.K,1.K%>; then
x in [#]K /\ [#]Polynom-Ring K by Th13;
then
reconsider x as Element of the carrier of Polynom-Ring K;
A5: deg x = len x - 1 by HURWITZ:def 2
.= 2 -1 by POLYNOM5:40;
now assume x in rng canHom K; then
consider a being object such that
A6: a in dom(canHom K) & x = (canHom K).a by FUNCT_1:def 3;
reconsider a as Element of [#]K by A6;
deg(a|K) <= 0 by RATFUNC1:def 2;
hence contradiction by A6,A5,RING_4:def 6;
end;
hence thesis by A4,Th13;
end;
suppose
A7: ex a being Element of F st a = <%0.F,1.F%>;
take F;
take x = <%0.F,1.F%>;
2 = len x by POLYNOM5:40; then
A8: deg x = 2-1 by HURWITZ:def 2;
A9: x in the carrier of Polynom-Ring F by POLYNOM3:def 10;
now assume x in rng(canHom F); then
consider a being object such that
A10: a in dom(canHom F) & x = (canHom F).a by FUNCT_1:def 3;
reconsider a as Element of [#]F by A10;
deg(a|F) <= 0 by RATFUNC1:def 2;
hence contradiction by A10,A8,RING_4:def 6;
end;
hence thesis by A7,A9,XBOOLE_0:def 4;
end;
end;
registration
cluster non polynomial_disjoint for Field;
existence
proof
consider F being Field such that
A1: [#]F /\ [#]Polynom-Ring F <> {} by Th14;
take F;
thus thesis by A1;
end;
end;
definition
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
func isoR(x,o) -> Function of F,ExField(x,o) means
:Def9:
it.x = o &
for a being Element of F st a <> x holds it.a = a;
existence
proof
A1: [#]ExField(x,o) = carr(x,o) by Def8;
defpred P[object,object] means
($1 = x & $2 = o) or ($1 <> x & $2 = $1);
A2: for u being object st u in [#]F
ex y being object st y in the carrier of ExField(x,o) & P[u,y]
proof
let u be object;
assume
A3: u in [#]F;
per cases;
suppose
A4: u = x;
take b = o;
o in {o} by TARSKI:def 1;
hence b in the carrier of ExField(x,o) by A1,XBOOLE_0:def 3;
thus thesis by A4;
end;
suppose
A5: u <> x;
take u;
not u in {x} by A5,TARSKI:def 1; then
u in [#]F \ {x} by A3,XBOOLE_0:def 5;
hence u in the carrier of ExField(x,o) by A1,XBOOLE_0:def 3;
thus thesis by A5;
end;
end;
consider g being Function of [#]F,the carrier of ExField(x,o)
such that
A6: for u being object st u in [#]F holds P[u,g.u]
from FUNCT_2:sch 1(A2);
reconsider g as Function of F,ExField(x,o);
take g;
thus
thesis by A6;
end;
uniqueness
proof
let g1,g2 be Function of F,ExField(x,o);
assume that
A7: g1.x = o &
for a being Element of F st a <> x holds g1.a = a and
A8: g2.x = o &
for a being Element of F st a <> x holds g2.a = a;
now let o be object;
assume o in [#]F; then
reconsider a = o as Element of F;
per cases;
suppose a = x;
hence g1.o = g2.o by A8,A7;
end;
suppose
A9: a <> x; then
g1.a = a by A7 .= g2.a by A9,A8;
hence g1.o = g2.o;
end;
end;
hence g1 = g2;
end;
end;
registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object;
cluster isoR(x,o) -> onto;
coherence
proof
set f = isoR(x,o);
A1: the carrier of ExField(x,o) = carr(x,o) by Def8;
A2: rng f c= the carrier of ExField(x,o) by RELAT_1:def 19;
now let u be object;
assume
A3: u in the carrier of ExField(x,o);
per cases;
suppose o = u; then
A4: f.x = u by Def9;
[#]F = dom f by FUNCT_2:def 1;
hence u in rng f by A4,FUNCT_1:def 3;
end;
suppose o <> u; then
not u in {o} by TARSKI:def 1; then
A5: u in [#]F \ {x} by A3,A1,XBOOLE_0:def 3; then
reconsider a = u as Element of F;
not u in {x} by A5,XBOOLE_0:def 5; then
x <> u by TARSKI:def 1; then
A6: f.a = a by Def9;
[#]F = dom f by FUNCT_2:def 1;
hence u in rng f by A6,FUNCT_1:def 3;
end;
end;
hence f is onto by A2,TARSKI:2;
end;
end;
theorem
for x being non trivial Element of F, o being object st not o in [#]F
holds isoR(x,o) is one-to-one
proof
let x be non trivial Element of F;
let o be object;
assume not o in [#]F; then
A1: a <> o;
set f = isoR(x,o);
now let x1,x2 be object;
assume
A2: x1 in dom f & x2 in dom f & f.x1 = f.x2;
per cases;
suppose
A3: x1 = x;
now assume
A4: x2 <> x;
reconsider a = x2 as Element of F by A2;
a = f.a by A4,Def9 .= o by A3,A2,Def9;
hence contradiction by A1;
end;
hence x1 = x2 by A3;
end;
suppose
A5: x1 <> x;
reconsider a = x1 as Element of F by A2;
A6: f.a = a by A5,Def9;
now assume
A7: x2 <> x1;
per cases;
suppose x2 = x;
hence contradiction by A6,A1,A2,Def9;
end;
suppose
A8: x2 <> x;
reconsider b = x2 as Element of F by A2;
thus contradiction by A2,A6,A8,A7,Def9;
end;
end;
hence x1 = x2;
end;
end;
hence f is one-to-one;
end;
theorem Th15:
for x being non trivial Element of F, u being object st not u in [#]F
holds isoR(x,u) is additive multiplicative unity-preserving
proof
let x be non trivial Element of F;
let u be object;
assume
A1: not u in [#]F; then
A2: a <> u;
set f = isoR(x,u);
u in {u} by TARSKI:def 1; then
reconsider o = u as Element of carr(x,u) by XBOOLE_0:def 3;
::::::::::::::::::::::::::::::
:: isoR(x,u) is additive
:::::::::::::::::::::::::::::
now let a,b be Element of F;
A3: a <> u & b <> u by A2;
per cases;
suppose
A4: a = x; then
A5: f.a = u by Def9;
per cases;
suppose
A6: b = x; then
A7: f.b = u by Def9;
per cases;
suppose
A8: (the addF of F).(x,x) <> x;
thus f.a + f.b = addR(x,u).(u,u) by A5,A7,Def8
.= addR(o,o) by Def5
.= a + b by A4,A6,A8,Def4
.= f.(a+b) by A4,A6,A8,Def9;
end;
suppose
A9: (the addF of F).(x,x) = x;
thus f.a + f.b = addR(x,u).(u,u) by A5,A7,Def8
.= addR(o,o) by Def5
.= u by A9,Def4
.= f.(a+b) by A4,A6,A9,Def9;
end;
end;
suppose
A10: b <> x; then
not b in {x} by TARSKI:def 1; then
b in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider b1 = b as Element of carr(x,u) by XBOOLE_0:def 3;
A11: f.b = b by A10,Def9;
per cases;
suppose
A12: (the addF of F).(x,b) <> x;
thus f.a + f.b = addR(x,u).(u,b) by A5,A11,Def8
.= addR(o,b1) by Def5
.= a + b by A2,A4,A12,Def4
.= f.(a+b) by A4,A12,Def9;
end;
suppose
A13: (the addF of F).(x,b) = x;
thus f.a + f.b = addR(x,u).(u,b) by A5,A11,Def8
.= addR(o,b1) by Def5
.= u by A3,A13,Def4
.= f.(a+b) by A4,A13,Def9;
end;
end;
end;
suppose
A14: a <> x; then
not a in {x} by TARSKI:def 1; then
a in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider a1 = a as Element of carr(x,u) by XBOOLE_0:def 3;
A15: f.a = a by A14,Def9;
per cases;
suppose
A16: b = x; then
A17: f.b = u by Def9;
per cases;
suppose
A18: (the addF of F).(a,x) <> x;
thus f.a + f.b = addR(x,u).(a,u) by A15,A17,Def8
.= addR(a1,o) by Def5
.= a + b by A16,A2,A18,Def4
.= f.(a+b) by A16,A18,Def9;
end;
suppose
A19: (the addF of F).(a,x) = x;
thus f.a + f.b = addR(x,u).(a,u) by A15,A17,Def8
.= addR(a1,o) by Def5
.= u by A3,A19,Def4
.= f.(a+b) by A16,A19,Def9;
end;
end;
suppose
A20: b <> x; then
not b in {x} by TARSKI:def 1; then
b in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider b1 = b as Element of carr(x,u) by XBOOLE_0:def 3;
A21: f.b = b by A20,Def9;
per cases;
suppose
A22: (the addF of F).(a,b) <> x;
thus f.a + f.b = addR(x,u).(a,b) by A15,A21,Def8
.= addR(a1,b1) by Def5
.= a + b by A3,A22,Def4
.= f.(a+b) by A22,Def9;
end;
suppose
A23: (the addF of F).(a,b) = x;
thus f.a + f.b = addR(x,u).(a,b) by A15,A21,Def8
.= addR(a1,b1) by Def5
.= u by A3,A23,Def4
.= f.(a+b) by A23,Def9;
end;
end;
end;
end;
hence f is additive;
::::::::::::::::::::::::::::::
:: isoR(x,u) is multiplicative
:::::::::::::::::::::::::::::
now let a,b be Element of F;
A24: a <> u & b <> u by A1;
per cases;
suppose
A25: a = x; then
A26: f.a = u by Def9;
per cases;
suppose
A27: b = x; then
A28: f.b = u by Def9;
per cases;
suppose
A29: (the multF of F).(x,x) <> x;
thus f.a * f.b = multR(x,u).(u,u) by A26,A28,Def8
.= multR(o,o) by Def7
.= a * b by A25,A27,A29,Def6
.= f.(a*b) by A25,A27,A29,Def9;
end;
suppose
A30: (the multF of F).(x,x) = x;
thus f.a * f.b = multR(x,u).(u,u) by A26,A28,Def8
.= multR(o,o) by Def7
.= u by A30,Def6
.= f.(a*b) by A25,A27,A30,Def9;
end;
end;
suppose
A31: b <> x; then
not b in {x} by TARSKI:def 1; then
b in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider b1 = b as Element of carr(x,u) by XBOOLE_0:def 3;
A32: f.b = b by A31,Def9;
per cases;
suppose
A33: (the multF of F).(x,b) <> x;
thus f.a * f.b = multR(x,u).(u,b) by A26,A32,Def8
.= multR(o,b1) by Def7
.= a * b by A2,A25,A33,Def6
.= f.(a*b) by A25,A33,Def9;
end;
suppose
A34: (the multF of F).(x,b) = x;
thus f.a * f.b = multR(x,u).(u,b) by A26,A32,Def8
.= multR(o,b1) by Def7
.= u by A24,A34,Def6
.= f.(a*b) by A25,A34,Def9;
end;
end;
end;
suppose
A35: a <> x; then
not a in {x} by TARSKI:def 1; then
a in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider a1 = a as Element of carr(x,u) by XBOOLE_0:def 3;
A36: f.a = a by A35,Def9;
per cases;
suppose
A37: b = x; then
A38: f.b = u by Def9;
per cases;
suppose
A39: (the multF of F).(a,x) <> x;
thus f.a * f.b = multR(x,u).(a,u) by A36,A38,Def8
.= multR(a1,o) by Def7
.= a * b by A2,A37,A39,Def6
.= f.(a*b) by A37,A39,Def9;
end;
suppose
A40: (the multF of F).(a,x) = x;
thus f.a * f.b = multR(x,u).(a,u) by A36,A38,Def8
.= multR(a1,o) by Def7
.= u by A24,A40,Def6
.= f.(a*b) by A37,A40,Def9;
end;
end;
suppose
A41: b <> x; then
not b in {x} by TARSKI:def 1; then
b in [#]F \ {x} by XBOOLE_0:def 5; then
reconsider b1 = b as Element of carr(x,u) by XBOOLE_0:def 3;
A42: f.b = b by A41,Def9;
per cases;
suppose
A43: (the multF of F).(a,b) <> x;
thus f.a * f.b = multR(x,u).(a,b) by A36,A42,Def8
.= multR(a1,b1) by Def7
.= a * b by A24,A43,Def6
.= f.(a*b) by A43,Def9;
end;
suppose
A44: (the multF of F).(a,b) = x;
thus f.a * f.b = multR(x,u).(a,b) by A36,A42,Def8
.= multR(a1,b1) by Def7
.= u by A24,A44,Def6
.= f.(a*b) by A44,Def9;
end;
end;
end;
end;
hence f is multiplicative by GROUP_6:def 6;
::::::::::::::::::::::::::::::
:: isoR(x,u) is unity-preserving
:::::::::::::::::::::::::::::
reconsider S = ExField(x,u) as well-unital Ring
by A1,Th7,Th10,Th8,Th9,Th11;
1.F <> x by Def2; then
f.(1_F) = 1.F by Def9 .= 1_S by Def8;
hence f is unity-preserving;
end;
theorem
for F being non almost_trivial Field
ex K being non polynomial_disjoint Field st K,F are_isomorphic
proof
let F be non almost_trivial Field;
set x = the non trivial Element of F;
reconsider o = <%0.F,1.F%> as object;
per cases;
suppose
A1: not o in [#]F; then
reconsider S = ExField(x,o) as Field
by Th7,Th8,Th9,Th10,Th11,Th12;
[#]S /\ [#]Polynom-Ring S <> {} by Th13; then
reconsider S as non polynomial_disjoint Field by Def3;
take S;
isoR(x,o) is additive multiplicative unity-preserving by A1,Th15;
hence thesis by MOD_4:def 12,QUOFIELD:def 23;
end;
suppose ex a being Element of F st a = <%0.F,1.F%>; then
consider a being Element of F such that
A2: a = <%0.F,1.F%>;
a in [#]Polynom-Ring(F) by A2,POLYNOM3:def 10; then
a in [#]F /\ [#]Polynom-Ring(F)
by XBOOLE_0:def 4; then
reconsider S = F as non polynomial_disjoint Field by Def3;
take S;
thus thesis;
end;
end;
theorem
for F being non almost_trivial Field holds
ex K being non polynomial_disjoint Field, p being Polynomial of K
st K,F are_isomorphic & deg p = n & p in [#]K /\ [#]Polynom-Ring K
proof
let F be non almost_trivial Field;
set x = the non trivial Element of F;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider o = rpoly(n,0.F) as object;
set x = the non trivial Element of F;
per cases;
suppose
A1: not o in [#]F; then
reconsider K = ExField(x,rpoly(n,0.F)) as Field
by Th7,Th8,Th10,Th9,Th12,Th11;
set p = rpoly(n,0.K);
now let i be Element of NAT;
per cases;
suppose
A2: i = 0;
hence rpoly(n,0.F).i = -power(F).(0.F,n) by HURWITZ:25
.= -0.F by Th6
.= -0.K by Def8
.= -power(K).(0.K,n) by Th6
.= p.i by A2,HURWITZ:25;
end;
suppose
A3: i = n;
hence rpoly(n,0.F).i = 1_F by HURWITZ:25
.= 1_K by Def8
.= p.i by A3,HURWITZ:25;
end;
suppose
A4: i <> 0 & i <> n;
hence rpoly(n,0.F).i = 0.F by HURWITZ:26
.= 0.K by Def8
.= p.i by A4,HURWITZ:26;
end;
end; then
A5: rpoly(n,0.F) = rpoly(n,0.K);
A6: p in [#]Polynom-Ring K by POLYNOM3:def 10;
p in {rpoly(n,0.F)} by A5,TARSKI:def 1; then
p in carr(x,rpoly(n,0.F)) by XBOOLE_0:def 3; then
A7: p in [#]K by Def8; then
p in [#]K /\ [#]Polynom-Ring K by A6,XBOOLE_0:def 4; then
reconsider K as non polynomial_disjoint Field by Def3;
take K;
take p = rpoly(n,0.K);
isoR(x,rpoly(n,0.F)) is
additive multiplicative unity-preserving by A1,Th15;
hence K,F are_isomorphic by MOD_4:def 12,QUOFIELD:def 23;
thus thesis by A7,A6,XBOOLE_0:def 4,HURWITZ:27;
end;
suppose
A8: ex a being Element of F st a = rpoly(n,0.F); then
consider a being Element of F such that
A9: a = rpoly(n,0.F);
a in the carrier of Polynom-Ring(F) by A9,POLYNOM3:def 10; then
a in [#]F /\ [#]Polynom-Ring(F) by XBOOLE_0:def 4;then
reconsider K = F as non polynomial_disjoint Field by Def3;
take K;
take x = rpoly(n,0.K);
x in the carrier of Polynom-Ring F by POLYNOM3:def 10;
hence thesis by A8,HURWITZ:27,XBOOLE_0:def 4;
end;
end;
begin :: An Intuitive "Solution"
definition
let R be Ring;
attr R is flat means
:Def10:
for a,b being Element of R holds the_rank_of a = the_rank_of b;
end;
registration
cluster flat for Ring;
existence
proof
set R = the trivial Ring;
take R;
thus thesis by STRUCT_0:def 10;
end;
end;
theorem Th16:
for R being flat Ring, p being Polynomial of R holds not p in [#]R
proof
let R be flat Ring, p be Polynomial of R;
now assume
A1: p in [#]R; then
reconsider a = p as Element of R;
A2: the_rank_of p = the_rank_of (p.0) by A1,Def10;
dom p = NAT by FUNCT_2:def 1; then
A3: [0,p.0] in p by FUNCT_1:def 2;
the_rank_of (p.0) in the_rank_of [0,p.0] by CLASSES1:84;
hence contradiction by A2,A3,CLASSES1:68;
end;
hence thesis;
end;
registration
cluster -> polynomial_disjoint for flat Ring;
coherence
proof
let R be flat Ring;
set M = [#]R /\ [#]Polynom-Ring R;
set x = the Element of M;
now assume R is non polynomial_disjoint; then
A1: x in [#]R & x in [#]Polynom-Ring R by XBOOLE_0:def 4; then
reconsider p = x as Polynomial of R by POLYNOM3:def 10;
p = x;
hence contradiction by A1,Th16;
end;
hence thesis;
end;
end;
theorem Th17:
for R being non degenerated Ring st 0 in the carrier of R
holds R is non flat
proof
let R be non degenerated Ring;
A1: the_rank_of 0 = 0 by CLASSES1:71;
assume
A2: 0 in the carrier of R;
per cases;
suppose 0 = 0.R; then
the_rank_of 1.R <> {} by CLASSES1:71;
hence R is non flat by A1,A2;
end;
suppose 0 = 1.R; then
the_rank_of 0.R <> {} by CLASSES1:71;
hence R is non flat by A1,A2;
end;
suppose 0 <> 0.R & 0 <> 1.R; then
the_rank_of 0.R <> {} by CLASSES1:71;
hence R is non flat by A1,A2;
end;
end;
registration
cluster INT.Ring -> non flat;
coherence by INT_3:def 3,Th17;
cluster F_Rat -> non flat;
coherence by GAUSSINT:def 14,Th17;
cluster F_Real -> non flat;
coherence by Th17;
end;
registration
let n be non trivial Nat;
cluster Z/n -> non flat;
coherence
proof
1 < n by NAT_2:19,NAT_2:def 1;then
0.(Z/n) = 0 by Th4;
hence thesis by Th17;
end;
end;
begin :: Some Positive Results
theorem Th18:
for R being Ring, p being Polynomial of R for n being Nat holds p <> n
proof
let R be Ring, p be Polynomial of R; let u be Nat;
reconsider n = u as Element of NAT by ORDINAL1:def 12;
now assume
A1: p = n;
dom p = NAT by FUNCT_2:def 1; then
consider i being Nat such that
A2: i = [n,p.n] & i < n by A1;
thus contradiction by A2;
end;
hence thesis;
end;
registration
let n be non trivial Nat;
cluster Z/n -> polynomial_disjoint;
coherence
proof
Z/n =
doubleLoopStr(#Segm(n),addint(n),multint(n),In(1,Segm(n)),In(0,Segm(n))#)
by INT_3:def 12; then
A1: [#]Z/n = n by ORDINAL1:def 17;
set M = [#]Z/n /\ [#]Polynom-Ring Z/n;
set x = the Element of M;
now assume Z/n is non polynomial_disjoint; then
A2: x in [#]Z/n & x in [#]Polynom-Ring Z/n by XBOOLE_0:def 4; then
reconsider p = x as Polynomial of Z/n by POLYNOM3:def 10;
x in { m where m is Nat : m < n } by A1,A2,Th1; then
consider m being Nat such that
A3: x = m & m < n;
m = p by A3;
hence contradiction by Th18;
end;
hence thesis;
end;
end;
registration
cluster polynomial_disjoint for finite Field;
existence
proof
take Z/2;
2 is non trivial by NAT_2:def 1;
hence thesis;
end;
end;
theorem Th19:
for R being Ring, p being Polynomial of R for i being Integer holds p <> i
proof
let R be Ring, p be Polynomial of R; let i be Integer;
A1: i in INT by INT_1:def 2;
now assume
A2: p = i;
per cases by A1,NUMBERS:def 4,XBOOLE_0:def 3;
suppose i in NAT; then
reconsider n = i as Element of NAT;
p = n by A2;
hence contradiction by Th18;
end;
suppose i in [:{0},NAT:]; then
consider x,y being object such that
A3: x in {0} & y in NAT & i = [x,y] by ZFMISC_1:def 2;
reconsider n = y as Element of NAT by A3;
A4: p = [0,n] by A2,A3,TARSKI:def 1 .= {{0,n},{0}} by TARSKI:def 5;
A5: dom p = NAT by FUNCT_2:def 1;
per cases by A4,A5;
suppose
A6: [0,p.0] = {0,n};
[0,p.0] = {{0,p.0},{0}} by TARSKI:def 5; then
A7: 0 in {{0,p.0},{0}} by A6,TARSKI:def 2;
per cases by A7;
suppose 0 = {0};
hence contradiction;
end;
suppose 0 = {0,p.0}; then
{} = {0,p.0};
hence contradiction;
end;
end;
suppose [0,p.0] = {0};
hence contradiction by CARD_1:49;
end;
end;
end;
hence thesis;
end;
registration
cluster INT.Ring -> polynomial_disjoint;
coherence
proof
set R = INT.Ring;
set M = [#]R /\ [#]Polynom-Ring R;
set x = the Element of M;
now assume R is non polynomial_disjoint; then
x in [#]R & x in [#]Polynom-Ring R by XBOOLE_0:def 4; then
reconsider p = x as Polynomial of R by POLYNOM3:def 10;
reconsider x as Integer;
p = x;
hence contradiction by Th19;
end;
hence thesis;
end;
end;
Lem2:
for R being Ring, p being Polynomial of R
for r being Rational holds r in RAT+ & p = r implies r = [1,2]
proof
let R be Ring, p be Polynomial of R; let r be Rational;
assume
A1: r in RAT+ & p = r;
A2: dom p = NAT by FUNCT_2:def 1;
not r in omega by A1,Th19; then
r in ({[i,j] where i,j is Element of omega: i,j are_coprime & j <> {}}
\ the set of all [k,1] where k is Element of omega)
by A1,XBOOLE_0:def 3; then
A3: r in {[i,j] where i,j is Element of omega: i,j are_coprime & j <> {}} &
not r in the set of all [k,1] where k is Element of omega
by XBOOLE_0:def 5; then
consider i,j being Element of omega such that
A4: r = [i,j] & i,j are_coprime & j <> {};
[i,p.i] in p by A2,FUNCT_1:def 2; then
{{i,p.i},{i}} in p by TARSKI:def 5; then
A5: {{i,p.i},{i}} in {{i,j},{i}} by A1,A4,TARSKI:def 5;
per cases by A5,TARSKI:def 2;
suppose
A6: {{i,p.i},{i}} = {i,j};
A7: j in {i,j} by TARSKI:def 2;
per cases by A6,A7,TARSKI:def 2;
suppose j = {i}; then
i = 0; then
j = 1 by A4,ARYTM_3:3;
hence r = [1,2] by A3,A4;
end;
suppose
A8: j = {i,p.i};
per cases;
suppose i = p.i; then
for o be object holds o in j iff o = i by A8,TARSKI:def 2;
then j = {i} by TARSKI:def 1; then
i = {}; then
j = 1 by A4,ARYTM_3:3;
hence r = [1,2] by A3,A4;
end;
suppose i <> p.i; then
per cases by A8,Th3;
suppose i = 1 & p.i = 0;
hence r = [1,2] by A8,A4,CARD_1:50;
end;
suppose i = 0 & p.i = 1; then
j = 1 by A4,ARYTM_3:3;
hence r = [1,2] by A3,A4;
end;
end;
end;
end;
suppose
A11: {{i,p.i},{i}} = {i};
{i,p.i} in {{i,p.i},{i}} by TARSKI:def 2; then
{i,p.i} = i by A11,TARSKI:def 1; then
i in i by TARSKI:def 2;
hence r = [1,2];
end;
end;
Lem3:
for R being Ring, p being Polynomial of R holds p <> [1,2]
proof
let R be Ring, p be Polynomial of R;
A1: dom p = NAT by FUNCT_2:def 1;
now assume p = [1,2]; then
A2: p = {{1,2},{1}} by TARSKI:def 5;
per cases by A2,A1;
suppose [3,p.3] = {1,2}; then
A3: {{3,p.3},{3}} = {1,2} by TARSKI:def 5;
A4: {3} in {{3,p.3},{3}} by TARSKI:def 2;
per cases by A3,A4;
suppose
1 = {3};
hence contradiction;
end;
suppose 2 = {3};
then per cases;
suppose 3 = 0;
hence contradiction;
end;
suppose 3 = 1;
hence contradiction;
end;
end;
end;
suppose [3,p.3] = {1}; then
A9: {{3,p.3},{3}} = {1} by TARSKI:def 5;
{3} in {{3,p.3},{3}} by TARSKI:def 2; then
A10: {3} = {0} by A9;
3 in {3} by TARSKI:def 1;
hence contradiction by A10,TARSKI:def 1;
end;
end;
hence thesis;
end;
theorem Th20:
for R being Ring, p being Polynomial of R for r being Rational holds p <> r
proof
let R be Ring, p be Polynomial of R; let r be Rational;
A1: r in RAT+ \/ [:{0},RAT+:] \ {[0,0]} by NUMBERS:def 3,RAT_1:def 2;
now assume
A2: p = r; then
not r in RAT+ by Lem2,Lem3; then
r in [:{0},RAT+:] by A1,XBOOLE_0:def 3; then
consider x,y being object such that
A3: x in {0} & y in RAT+ & r = [x,y] by ZFMISC_1:def 2;
dom p = NAT by FUNCT_2:def 1; then
[1,p.1] in p by FUNCT_1:def 2; then
A4: [1,p.1] in {{x,y},{x}} by A3,A2,TARSKI:def 5;
per cases by A4,TARSKI:def 2;
suppose [1,p.1] = {x,y}; then
A5: {{1,p.1},{1}} = {x,y} by TARSKI:def 5;
A6: x in {x,y} by TARSKI:def 2;
per cases by A5,A6,TARSKI:def 2;
suppose x = {1,p.1};
hence contradiction by A3,TARSKI:def 1;
end;
suppose x = {1};
hence contradiction by A3;
end;
end;
suppose [1,p.1] = {x};
hence contradiction by A3,TARSKI:def 1;
end;
end;
hence thesis;
end;
registration
cluster F_Rat -> polynomial_disjoint;
coherence
proof
set R = F_Rat,
x = the Element of [#]R /\ [#]Polynom-Ring R;
now assume R is non polynomial_disjoint; then
A1: x in [#]R & x in [#]Polynom-Ring R
by XBOOLE_0:def 4; then
reconsider p = x as Polynomial of R by POLYNOM3:def 10;
reconsider x as Rational by A1;
p = x;
hence contradiction by Th20;
end;
hence thesis;
end;
end;
Lem4:
for R being Ring, p being Polynomial of R for r being Real st r in REAL+
holds p <> r
proof
let R be Ring, p be Polynomial of R; let x be Real;
assume
A1: x in REAL+;
A2: dom p = NAT by FUNCT_2:def 1; then
A3: [0,p.0] in p & [1,p.1] in p by FUNCT_1:def 2;
now assume
A4: p = x;
per cases;
suppose x is Rational;
hence contradiction by A4,Th20;
end;
suppose not x is Rational; then
not x in RAT; then
(not x in RAT+ \/ [:{0},RAT+:]) or x in {[0,0]}
by NUMBERS:def 3,XBOOLE_0:def 5; then
per cases by XBOOLE_0:def 3;
suppose
A5: x in {[0,0]};
[0,0] = {{0},{0,0}} by TARSKI:def 5;
hence contradiction by A2,A4,A5;
end;
suppose not x in RAT+ & not x in [:{0},RAT+:]; then
x in DEDEKIND_CUTS by A1,ARYTM_2:def 2,XBOOLE_0:def 3; then
x in {A where A is Subset of RAT+ :
for r being Element of RAT+ holds r in A implies
(for s being Element of RAT+ st s <=' r holds s in A) &
ex s being Element of RAT+ st s in A & r < s }
& not x in {RAT+} by ARYTM_2:def 1,XBOOLE_0:def 5; then
consider A being Subset of RAT+ such that
A6: x = A & for r being Element of RAT+ holds r in A implies
(for s being Element of RAT+ st s <=' r holds s in A) &
ex s being Element of RAT+ st s in A & r < s;
consider u being Element of A such that
A7: u = [0,p.0] by A3,A4,A6;
u in A by A4,A6; then
reconsider u as Element of RAT+;
per cases by XBOOLE_0:def 3;
suppose u in omega; then
reconsider n = u as Element of omega;
n = {1,1} by A7;
hence contradiction by A7;
end;
suppose u in
{[i,j] where i,j is Element of omega: i,j are_coprime &
j <> {}}\the set of all [k,1] where k is Element of omega;
then
A8: u in
{[i,j] where i,j is Element of omega: i,j are_coprime &
j <> {}} & not u in the set of all [k,1] where
k is Element of omega by XBOOLE_0:def 5; then
consider i,j being Element of omega such that
A9: u = [i,j] & i,j are_coprime & j <> {};
i = 0 by A7,A9,XTUPLE_0:1; then
j = 1 by A9,ARYTM_3:3;
hence contradiction by A8,A9;
end;
end;
end;
end;
hence thesis;
end;
theorem Th21:
for R being Ring, p being Polynomial of R for r being Real holds p <> r
proof
let R be Ring, p be Polynomial of R; let r be Real;
A1: r in REAL+ \/ [:{0},REAL+:] \ {[0,0]} by XREAL_0:def 1,NUMBERS:def 1;
now assume
A2: p = r; then
not r in REAL+ by Lem4; then
r in [:{0},REAL+:] by A1,XBOOLE_0:def 3; then
consider x,y being object such that
A3: x in {0} & y in REAL+ & r = [x,y] by ZFMISC_1:def 2;
dom p = NAT by FUNCT_2:def 1; then
[1,p.1] in p by FUNCT_1:def 2; then
A4: [1,p.1] in {{x,y},{x}} by A3,A2,TARSKI:def 5;
per cases by A4,TARSKI:def 2;
suppose [1,p.1] = {x,y}; then
A5: {{1,p.1},{1}} = {x,y} by TARSKI:def 5;
x in {x,y} by TARSKI:def 2; then
per cases by A5,TARSKI:def 2;
suppose x = {1,p.1}; then
x <> {};
hence contradiction by A3,TARSKI:def 1;
end;
suppose x = {1}; then
x <> {};
hence contradiction by A3,TARSKI:def 1;
end;
end;
suppose [1,p.1] = {x};
hence contradiction by A3,TARSKI:def 1,CARD_1:49;
end;
end;
hence thesis;
end;
registration
cluster F_Real -> polynomial_disjoint;
coherence
proof
set R = F_Real,
x = the Element of [#]R /\ [#]Polynom-Ring R;
now assume R is non polynomial_disjoint; then
x in [#]R & x in [#]Polynom-Ring R by XBOOLE_0:def 4; then
reconsider p = x as Polynomial of R by POLYNOM3:def 10;
reconsider x as Real;
p = x;
hence contradiction by Th21;
end;
hence thesis;
end;
end;
registration
cluster polynomial_disjoint for infinite Field;
existence
proof
take F_Rat;
thus thesis;
end;
end;
registration
let R be polynomial_disjoint Ring;
cluster Polynom-Ring R -> polynomial_disjoint;
coherence
proof
set RX = Polynom-Ring R,
x = the Element of [#]RX /\ [#]Polynom-Ring RX;
now assume RX is non polynomial_disjoint; then
A1: x in [#]RX & x in [#]Polynom-Ring RX by XBOOLE_0:def 4; then
reconsider p1 = x as Polynomial of RX by POLYNOM3:def 10;
reconsider p2 = x as Polynomial of R by A1,POLYNOM3:def 10;
p2.0 in [#]R; then
p1.0 in [#]R /\ [#]Polynom-Ring R by XBOOLE_0:def 4;
hence contradiction by Def3;
end;
hence thesis;
end;
end;
registration
let F be Field, p be Element of [#]Polynom-Ring F;
cluster (Polynom-Ring F)/({p}-Ideal) -> polynomial_disjoint;
coherence
proof
set FX = Polynom-Ring F, I = {p}-Ideal;
set K = (Polynom-Ring F)/({p}-Ideal);
set x = the Element of [#]K /\ [#]Polynom-Ring K;
now assume
A1: K is non polynomial_disjoint; then
A2: x in [#]K & x in [#]Polynom-Ring K by XBOOLE_0:def 4;
reconsider x as Element of K by A1,XBOOLE_0:def 4;
reconsider q = x as Polynomial of K by A2,POLYNOM3:def 10;
consider a being Element of FX such that
A3: x = Class(EqRel(FX,I),a) by RING_1:11;
reconsider p = a as Polynomial of F by POLYNOM3:def 10;
for o being object st o in q
ex n being Element of NAT, u being object st o = [n,u]
proof
let o be object; assume o in q; then
consider a,b being object such that
A4: a in NAT & b in [#]K & o = [a,b] by ZFMISC_1:def 2;
reconsider a as Element of NAT by A4;
take a,b;
thus thesis by A4;
end; then
consider n being Element of NAT, u being object such that
A5: p = [n,u] by A3,EQREL_1:20;
dom p = NAT by FUNCT_2:def 1; then
[n,p.n] in p by FUNCT_1:1; then
A6: [n,p.n] in {{n},{n,u}} by A5,TARSKI:def 5;
now let a,b be object;
assume [n,a] in {{n},{n,b}}; then
A7: {{n},{n,a}} in {{n},{n,b}} by TARSKI:def 5;
per cases by A7,TARSKI:def 2;
suppose
A8: {{n},{n,a}} = {n};
{n} in {{n},{n,a}} by TARSKI:def 2;
hence contradiction by A8;
end;
suppose
A9: {{n},{n,a}} = {n,b};
A10: n in {n,b} by TARSKI:def 2;
per cases by A10,A9,TARSKI:def 2;
suppose n = {n}; then
n in n;
hence contradiction;
end;
suppose n = {n,a}; then
n in n by TARSKI:def 2;
hence contradiction;
end;
end;
end;
hence contradiction by A6;
end;
hence thesis;
end;
end;
registration
let F be polynomial_disjoint Field;
let p be non constant Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring p -> polynomial_disjoint;
coherence
proof
set RX = Polynom-Ring p, FX = Polynom-Ring F;
set M = [#]RX /\ [#]Polynom-Ring RX;
set x = the Element of M;
A1: [#]RX = {q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
now assume RX is non polynomial_disjoint; then
A2: x in [#]RX & x in [#]Polynom-Ring RX by XBOOLE_0:def 4; then
consider q being Polynomial of F such that
A3: x = q & deg q < deg p by A1;
reconsider r = x as Polynomial of RX by A2,POLYNOM3:def 10;
now let o be object;
assume
A4: o in rng r;
rng r c= [#]RX by RELAT_1:def 19; then
o in [#]RX by A4; then
consider u being Polynomial of F such that
A5: o = u & deg u < deg p by A1;
thus o in [#]FX by A5,POLYNOM3:def 10;
end; then
rng r c= [#]FX; then
reconsider y = x as Function of NAT,FX by FUNCT_2:6;
ex n being Nat st for i being Nat st i >= n holds y.i = 0.FX
proof
consider n being Nat such that
A6: for i being Nat st i >= n holds r.i = 0.RX by ALGSEQ_1:def 1;
take n;
now let i be Nat;
assume i >= n;
hence y.i = 0.RX by A6
.= 0_.(F) by RING_4:def 8
.= 0.FX by POLYNOM3:def 10;
end;
hence thesis;
end; then
y is finite-Support by ALGSEQ_1:def 1; then
A8: x in [#]Polynom-Ring FX by POLYNOM3:def 10;
x in [#]Polynom-Ring F by A3,POLYNOM3:def 10; then
x in [#]FX /\ [#]Polynom-Ring FX by A8,XBOOLE_0:def 4;
hence contradiction by Def3;
end;
hence thesis;
end;
end;