let F be non almost_trivial Field; for x being non trivial Element of F
for o being object st not o in [#] F holds
ExField (x,o) is add-associative
let x be non trivial Element of F; for o being object st not o in [#] F holds
ExField (x,o) is add-associative
let o be object ; ( not o in [#] F implies ExField (x,o) is add-associative )
assume a1:
not o in [#] F
; ExField (x,o) is add-associative
then A1:
for a being Element of F holds a <> o
;
set C = carr (x,o);
set E = ExField (x,o);
set ADDR = the addF of F;
A2:
[#] (ExField (x,o)) = carr (x,o)
by Def8;
now for a, b, c being Element of (ExField (x,o)) holds (a + b) + c = a + (b + c)let a,
b,
c be
Element of
(ExField (x,o));
(b1 + b2) + b3 = b1 + (b2 + b3)per cases
( a = o or a <> o )
;
suppose A3:
a = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)then
a in {o}
by TARSKI:def 1;
then reconsider a1 =
a as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( b = o or b <> o )
;
suppose A4:
b = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( the addF of F . (x,x) <> x or the addF of F . (x,x) = x )
;
suppose A5:
the
addF of
F . (
x,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A7:
xx <> o
by a1;
per cases
( c = o or c <> o )
;
suppose A8:
c = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)then
c in {o}
by TARSKI:def 1;
then reconsider c1 =
c as
Element of
carr (
x,
o)
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
( the addF of F . (xx,x) <> x or the addF of F . (xx,x) = x )
;
suppose A11:
the
addF of
F . (
xx,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)A12: the
addF of
F . (
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
;
verum end; suppose A13:
the
addF of
F . (
xx,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)A14: the
addF of
F . (
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
;
verum end; end; suppose A15:
c <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
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
carr (
x,
o) ;
per cases
( the addF of F . (x,c1) <> x or the addF of F . (x,c1) = x )
;
suppose A18:
the
addF of
F . (
x,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)then A19:
b + c = x + cR
by A4, A15, A17, Def4;
then A20:
b + c <> o
by a1;
per cases
( the addF of F . (xx,c1) <> x or the addF of F . (xx,c1) = x )
;
suppose
the
addF of
F . (
xx,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)then A21:
(a + b) + c =
(x + x) + cR
by A7, A15, A16, Def4
.=
x + (x + cR)
by RLVECT_1:def 3
.=
the
addF of
F . (
x,
(b + c))
by A4, A15, A17, A18, Def4
;
per cases
( the addF of F . (x,bc) <> x or the addF of F . (x,bc) = x )
;
suppose A22:
the
addF of
F . (
x,
bc)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)A23: the
addF of
F . (
x,
bc) =
x + (x + cR)
by A4, A15, A17, A18, Def4
.=
(x + x) + cR
by RLVECT_1:def 3
.=
the
addF of
F . (
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
;
verum end; end; suppose A24:
the
addF of
F . (
xx,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)then A25:
(a + b) + c = o
by A7, A15, A16, Def4;
per cases
( the addF of F . (x,bc) <> x or the addF of F . (x,bc) = x )
;
suppose
the
addF of
F . (
x,
bc)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)A26: the
addF of
F . (
x,
bc) =
x + (x + cR)
by A4, A15, A17, A18, Def4
.=
(x + x) + cR
by RLVECT_1:def 3
.=
the
addF of
F . (
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
;
verum end; suppose A27:
the
addF of
F . (
x,
bc)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3) the
addF of
F . (
x,
bc) =
x + (x + cR)
by A4, A15, A17, A18, Def4
.=
(x + x) + cR
by RLVECT_1:def 3
.=
the
addF of
F . (
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
;
verum end; end; suppose A29:
the
addF of
F . (
x,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( the addF of F . (xx,c1) <> x or the addF of F . (xx,c1) = x )
;
suppose
the
addF of
F . (
xx,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose
the
addF of
F . (
xx,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)then x =
(x + x) + cR
.=
x + x
by A30
;
hence
(a + b) + c = a + (b + c)
by A5;
verum end; end; end; end; suppose A33:
the
addF of
F . (
x,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( c = o or c <> o )
;
suppose A36:
c <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( the addF of F . (x,c1) = x or the addF of F . (x,c1) <> x )
;
suppose A37:
the
addF of
F . (
x,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A39:
the
addF of
F . (
x,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
A41:
(a + b) + c =
(addR (x,o)) . (
ab,
c1)
by Def8
.=
addR (
ab,
c1)
by Def5
.=
the
addF of
F . (
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
.=
the
addF of
F . (
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
;
verum end; end; end; end; suppose A42:
b <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
A43: the
addF of
F . (
x,
b) =
x + bR
.=
bR + x
.=
the
addF of
F . (
b,
x)
;
per cases
( the addF of F . (x,b) <> x or the addF of F . (x,b) = x )
;
suppose A44:
the
addF of
F . (
x,
b)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( c = o or c <> o )
;
suppose A47:
c = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)then
c in {o}
by TARSKI:def 1;
then reconsider c1 =
c as
Element of
carr (
x,
o)
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
carr (
x,
o)
by Def8;
A50: the
addF of
F . (
ab,
x) =
(x + bR) + x
by A45
.=
x + (bR + x)
;
per cases
( the addF of F . (ab,x) <> x or the addF of F . (ab,x) = x )
;
suppose A51:
the
addF of
F . (
ab,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)thus (a + b) + c =
(addR (x,o)) . (
ab,
c1)
by Def8
.=
addR (
ab,
c1)
by Def5
.=
the
addF of
F . (
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
;
verum end; suppose A52:
the
addF of
F . (
ab,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; suppose A53:
c <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
A54: the
addF of
F . (
ab,
c) =
(x + bR) + cR
by A45
.=
x + (bR + cR)
by RLVECT_1:def 3
;
per cases
( the addF of F . (b,c) <> x or the addF of F . (b,c) = x )
;
suppose A55:
the
addF of
F . (
b,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( the addF of F . (ab,c1) <> x or the addF of F . (ab,c1) = x )
;
suppose A58:
the
addF of
F . (
ab,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A59:
the
addF of
F . (
ab,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; suppose A60:
the
addF of
F . (
b,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( the addF of F . (ab,c1) <> x or the addF of F . (ab,c1) = x )
;
suppose A62:
the
addF of
F . (
ab,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A63:
the
addF of
F . (
ab,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; end; suppose A64:
the
addF of
F . (
x,
b)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( c = o or c <> o )
;
suppose A68:
c <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
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
carr (
x,
o)
by Def8;
A74:
x + (bR + cR) =
(x + bR) + cR
by RLVECT_1:def 3
.=
x + cR
by A64
;
per cases
( the addF of F . (x,c1) <> x or the addF of F . (x,c1) = x )
;
suppose A75:
the
addF of
F . (
x,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)thus (a + b) + c =
(addR (x,o)) . (
ab,
c1)
by Def8
.=
addR (
ab,
c1)
by Def5
.=
the
addF of
F . (
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
;
verum end; suppose A76:
the
addF of
F . (
x,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; end; end; suppose A77:
a <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)
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
carr (
x,
o)
by Def8;
per cases
( b = o or b <> o )
;
suppose A79:
b = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)
b in {o}
by A79, TARSKI:def 1;
then reconsider b1 =
b as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( the addF of F . (a1,x) = x or the addF of F . (a1,x) <> x )
;
suppose A80:
the
addF of
F . (
a1,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( c = o or c <> o )
;
suppose A81a:
c = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)
c in {o}
by A81a, TARSKI:def 1;
then reconsider c1 =
c as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( the addF of F . (x,x) = x or the addF of F . (x,x) <> x )
;
suppose A82:
the
addF of
F . (
x,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A84:
the
addF of
F . (
x,
x)
<> x
;
b1 + (b2 + b3) = (b1 + b2) + b3A85:
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
carr (
x,
o)
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
;
then the
addF of
F . (
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
;
verum end; end; suppose A90:
c <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)
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
carr (
x,
o)
by Def8;
reconsider cR =
c as
Element of
F by A91;
per cases
( the addF of F . (x,c) = x or the addF of F . (x,c) <> x )
;
suppose A92:
the
addF of
F . (
x,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A94:
the
addF of
F . (
x,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A97;
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
;
verum end; end; suppose A100:
the
addF of
F . (
a1,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider abR =
a + b as
Element of
F by A103;
per cases
( c = o or c <> o )
;
suppose A104:
c = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)then
c in {o}
by TARSKI:def 1;
then reconsider c1 =
c as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( the addF of F . (x,x) = x or the addF of F . (x,x) <> x )
;
suppose A105:
the
addF of
F . (
x,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
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
;
verum end; suppose A109:
the
addF of
F . (
x,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A112;
A113: the
addF of
F . (
a,
bc) =
aR + (x + x)
by A110
.=
(aR + x) + x
by RLVECT_1:def 3
.=
the
addF of
F . (
ab,
x)
by A101
;
per cases
( the addF of F . (ab,x) = x or the addF of F . (ab,x) <> x )
;
suppose A114:
the
addF of
F . (
ab,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A115:
the
addF of
F . (
ab,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)thus (a + b) + c =
(addR (x,o)) . (
ab,
c1)
by Def8
.=
addR (
ab,
c1)
by Def5
.=
the
addF of
F . (
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
;
verum end; end; end; suppose A116:
c <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider cR =
c as
Element of
F by A117;
per cases
( the addF of F . (x,c) = x or the addF of F . (x,c) <> x )
;
suppose A118:
the
addF of
F . (
x,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A120: the
addF of
F . (
ab,
c) =
(aR + x) + cR
by A101
.=
aR + (x + cR)
by RLVECT_1:def 3
.=
the
addF of
F . (
a,
x)
by A118
;
per cases
( the addF of F . (ab,c1) = x or the addF of F . (ab,c1) <> x )
;
suppose A121:
the
addF of
F . (
ab,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A122:
the
addF of
F . (
ab,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; suppose A123:
the
addF of
F . (
x,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A126;
A127: the
addF of
F . (
a,
bc) =
aR + (x + cR)
by A124
.=
(aR + x) + cR
by RLVECT_1:def 3
.=
the
addF of
F . (
ab,
c)
by A101
;
per cases
( the addF of F . (ab,c1) = x or the addF of F . (ab,c1) <> x )
;
suppose A128:
the
addF of
F . (
ab,
c1)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A129:
the
addF of
F . (
ab,
c1)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; end; end; suppose A130:
b <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bR =
b as
Element of
F by A131;
A132:
now not x = x + xend; per cases
( the addF of F . (a,b) = x or the addF of F . (a,b) <> x )
;
suppose A134:
the
addF of
F . (
a,
b)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A136:
now not bR + x = xend; per cases
( c = o or c <> o )
;
suppose A139:
c = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)then
c in {o}
by TARSKI:def 1;
then reconsider c1 =
c as
Element of
carr (
x,
o)
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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A142;
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
;
verum end; suppose A145:
c <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider cR =
c as
Element of
F by A146;
per cases
( the addF of F . (b,c) <> x or the addF of F . (b,c) = x )
;
suppose A147:
the
addF of
F . (
b,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A150;
per cases
( the addF of F . (x,c) <> x or the addF of F . (x,c) = x )
;
suppose A151:
the
addF of
F . (
x,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A154:
the
addF of
F . (
x,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; suppose A156:
the
addF of
F . (
b,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A159:
x + cR =
aR + x
by A157, ALGSTR_0:def 4
.=
the
addF of
F . (
a,
x)
;
per cases
( the addF of F . (x,c) <> x or the addF of F . (x,c) = x )
;
suppose A160:
the
addF of
F . (
x,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A161:
the
addF of
F . (
x,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; end; suppose A162:
the
addF of
F . (
a,
b)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider abR =
a + b as
Element of
F by A165;
per cases
( c = o or c <> o )
;
suppose A166:
c = o
;
(b1 + b2) + b3 = b1 + (b2 + b3)then
c in {o}
by TARSKI:def 1;
then reconsider c1 =
c as
Element of
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( the addF of F . (b,x) <> x or the addF of F . (b,x) = x )
;
suppose A167:
the
addF of
F . (
b,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A170;
A171: the
addF of
F . (
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
( the addF of F . (ab,x) <> x or the addF of F . (ab,x) = x )
;
suppose A172:
the
addF of
F . (
ab,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A173:
the
addF of
F . (
ab,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; suppose A174:
the
addF of
F . (
b,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
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
( the addF of F . (ab,x) <> x or the addF of F . (ab,x) = x )
;
suppose A177:
the
addF of
F . (
ab,
x)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A178:
the
addF of
F . (
ab,
x)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; suppose A179:
c <> o
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider cR =
c as
Element of
F by A180;
per cases
( the addF of F . (b,c) <> x or the addF of F . (b,c) = x )
;
suppose A181:
the
addF of
F . (
b,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A184;
A185: the
addF of
F . (
ab,
c) =
(aR + bR) + cR
by A163
.=
aR + (bR + cR)
by RLVECT_1:def 3
.=
the
addF of
F . (
a,
bc)
by A182
;
per cases
( the addF of F . (ab,c) <> x or the addF of F . (ab,c) = x )
;
suppose A186:
the
addF of
F . (
ab,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A187:
the
addF of
F . (
ab,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; suppose A188:
the
addF of
F . (
b,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A190:
(aR + bR) + cR =
aR + (bR + cR)
by RLVECT_1:def 3
.=
the
addF of
F . (
a,
x)
by A188
;
per cases
( the addF of F . (ab,c) <> x or the addF of F . (ab,c) = x )
;
suppose A191:
the
addF of
F . (
ab,
c)
<> x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose A192:
the
addF of
F . (
ab,
c)
= x
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; end; end; end;
hence
ExField (x,o) is add-associative
by RLVECT_1:def 3; verum