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 distributive
let x be non trivial Element of F; for o being object st not o in [#] F holds
ExField (x,o) is distributive
let o be object ; ( not o in [#] F implies ExField (x,o) is distributive )
assume
not o in [#] F
; ExField (x,o) is distributive
then A1:
for a being Element of F holds a <> o
;
set C = carr (x,o);
set E = ExField (x,o);
A2:
[#] (ExField (x,o)) = carr (x,o)
by Def8;
A3:
now not x + x = xend;
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 carr (x,o) 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 not x * x = xend;
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 carr (x,o) by XBOOLE_0:def 3;
A7:
x * x <> o
by A1;
A8:
now not (x * x) + x = xend;
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 carr (x,o) by XBOOLE_0:def 3;
A9:
now for a, b, c being Element of (ExField (x,o)) holds (a * b) + (a * c) = a * (b + c)let a,
b,
c be
Element of
(ExField (x,o));
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)per cases
( a = o or a <> o )
;
suppose A10:
a = o
;
(b1 * b2) + (b1 * 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 A11:
b = o
;
(b1 * b2) + (b1 * 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;
A12:
a * b =
(multR (x,o)) . (
a1,
b1)
by Def8
.=
multR (
a1,
b1)
by Def7
.=
x * x
by A10, A11, A6, Def6
;
per cases
( c = o or c <> o )
;
suppose A13:
c = o
;
(b1 * b2) + (b1 * 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;
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
( (x * x) + (x * x) <> x or (x * x) + (x * x) = x )
;
suppose A17:
(x * x) + (x * x) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A19:
(x * x) + (x * x) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; suppose A21:
c <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider cR =
c as
Element of
F by A22;
per cases
( x + cR = x or x + cR <> x )
;
suppose A23:
x + cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
carr (
x,
o)
by Def8;
A29:
now not (x * x) + (x * cR) = xend; 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
;
verum end; suppose A30:
x + cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A33;
per cases
( x * cR = x or x * cR <> x )
;
suppose A34:
x * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A37:
x * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider acR =
a * c as
Element of
F by A40;
per cases
( (x * x) + (x * cR) <> x or (x * x) + (x * cR) = x )
;
suppose A41:
(x * x) + (x * cR) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A43:
(x * x) + (x * cR) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; end; end; suppose A45:
b <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bR =
b as
Element of
F by A46;
per cases
( x * bR = x or x * bR <> x )
;
suppose A47:
x * bR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( c = o or c <> o )
;
suppose A49:
c = o
;
(b1 * b2) + (b1 * 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;
A50:
a * c =
(multR (x,o)) . (
a1,
c1)
by Def8
.=
multR (
a1,
c1)
by Def7
.=
x * x
by A10, A49, A6, Def6
;
A51:
now not bR + x = xend; 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
carr (
x,
o)
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
;
verum end; suppose A55:
c <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider cR =
c as
Element of
F by A56;
per cases
( bR + cR = x or bR + cR <> x )
;
suppose A57:
bR + cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( x * cR = x or x * cR <> x )
;
suppose A59:
x * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A61:
x * x = x + x
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
;
verum end; suppose A66:
x * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; end; suppose A70:
bR + cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A73;
per cases
( x * cR = x or x * cR <> x )
;
suppose A74:
x * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A76:
now not x * (bR + cR) = xend; 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
;
verum end; suppose A79:
x * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
( x + (x * cR) = x or x + (x * cR) <> x )
;
suppose A84:
x + (x * cR) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A85:
x + (x * cR) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; end; end; suppose A86:
x * bR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider abR =
a * b as
Element of
F by A89;
per cases
( c = o or c <> o )
;
suppose A90:
c = o
;
(b1 * b2) + (b1 * 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;
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
carr (
x,
o)
by Def8;
reconsider acR =
a * c as
Element of
F by A93;
per cases
( bR + x = x or bR + x <> x )
;
suppose A94:
bR + x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A97:
bR + x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider bcR =
b + c as
Element of
F by A100;
per cases
( (x * bR) + (x * x) <> x or (x * bR) + (x * x) = x )
;
suppose A101:
(x * bR) + (x * x) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A103:
(x * bR) + (x * x) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; suppose A105:
c <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider cR =
c as
Element of
F by A106;
per cases
( bR + cR = x or bR + cR <> x )
;
suppose A107:
bR + cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A109:
(x * bR) + (x * cR) = x * x
by A107, VECTSP_1:def 2;
per cases
( x * cR <> x or x * cR = x )
;
suppose A110:
x * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A114:
x * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A116:
now not (x * bR) + x = xend; 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
;
verum end; end; suppose A118:
bR + cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
( x * cR <> x or x * cR = x )
;
suppose A123:
x * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider acR =
a * c as
Element of
F by A126;
per cases
( (x * bR) + (x * cR) <> x or (x * bR) + (x * cR) = x )
;
suppose A127:
(x * bR) + (x * cR) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A128:
(x * bR) + (x * cR) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; suppose A129:
x * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A131:
(x * bR) + x = x * (bR + cR)
by A129, VECTSP_1:def 2;
per cases
( (x * bR) + x <> x or (x * bR) + x = x )
;
suppose A132:
(x * bR) + x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A133:
(x * bR) + x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; end; end; end; end; suppose A134:
a <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
( b = o or b <> o )
;
suppose A136:
b = o
;
(b1 * b2) + (b1 * 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
( aR * x = x or aR * x <> x )
;
suppose A137:
aR * x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( c = o or c <> o )
;
suppose A139:
c = o
;
(b1 * b2) + (b1 * 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:
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
carr (
x,
o)
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
carr (
x,
o)
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
;
verum end; suppose A144:
c <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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 not aR * cR = xend; 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
carr (
x,
o)
by Def8;
per cases
( x + cR = x or x + cR <> x )
;
suppose A150:
x + cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A153:
x + cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
A156:
now not x + (aR * cR) = xend; 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
;
verum end; end; end; suppose A160:
aR * x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider abR =
a * b as
Element of
F by A163;
per cases
( c = o or c <> o )
;
suppose A164:
c = o
;
(b1 * b2) + (b1 * 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;
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
carr (
x,
o)
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
carr (
x,
o)
by Def8;
A169:
aR * (x + x) = (aR * x) + (aR * x)
by VECTSP_1:def 2;
per cases
( (aR * x) + (aR * x) <> x or (aR * x) + (aR * x) = x )
;
suppose A170:
(aR * x) + (aR * x) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A171:
(aR * x) + (aR * x) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; suppose A172:
c <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
( aR * cR = x or aR * cR <> x )
;
suppose A174:
aR * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( x + cR = x or x + cR <> x )
;
suppose A176:
x + cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A179:
x + cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
A182:
(aR * x) + x = aR * (x + cR)
by A174, VECTSP_1:def 2;
per cases
( (aR * x) + x <> x or (aR * x) + x = x )
;
suppose A183:
(aR * x) + x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A184:
(aR * x) + x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; suppose A185:
aR * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( x + cR = x or x + cR <> x )
;
suppose A188:
x + cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A191:
x + cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
A194:
(aR * x) + (aR * cR) = aR * (x + cR)
by VECTSP_1:def 2;
per cases
( (aR * x) + (aR * cR) = x or (aR * x) + (aR * cR) <> x )
;
suppose A195:
(aR * x) + (aR * cR) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A196:
(aR * x) + (aR * cR) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; end; end; end; suppose A197:
b <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
( aR * bR = x or aR * bR <> x )
;
suppose A199:
aR * bR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A201:
aR * (bR + x) = x + (aR * x)
by A199, VECTSP_1:def 2;
A202:
now not bR + x = xend; A203:
now not aR * x = xend; per cases
( c = o or c <> o )
;
suppose A206:
c = o
;
(b1 * b2) + (b1 * 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;
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
carr (
x,
o)
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
carr (
x,
o)
by Def8;
reconsider acR =
a * c as
Element of
F by A211;
per cases
( x + (aR * x) = x or x + (aR * x) <> x )
;
suppose A212:
x + (aR * x) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A213:
x + (aR * x) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; suppose A214:
c <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider cR =
c as
Element of
F by A215;
per cases
( bR + cR = x or bR + cR <> x )
;
suppose A216:
bR + cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( aR * cR = x or aR * cR <> x )
;
suppose A218:
aR * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A220:
aR * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
( x + (aR * cR) = x or x + (aR * cR) <> x )
;
suppose A225:
x + (aR * cR) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; suppose A226:
bR + cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( aR * cR = x or aR * cR <> x )
;
suppose A229:
aR * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A232:
aR * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
A235:
x + (aR * cR) = aR * (bR + cR)
by A199, VECTSP_1:def 2;
per cases
( x + (aR * cR) = x or x + (aR * cR) <> x )
;
suppose A236:
x + (aR * cR) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A237:
x + (aR * cR) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; end; end; suppose A238:
aR * bR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
reconsider abR =
a * b as
Element of
F by A239;
per cases
( c = o or c <> o )
;
suppose A241:
c = o
;
(b1 * b2) + (b1 * 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
( bR + x <> x or bR + x = x )
;
suppose A242:
bR + x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( aR * x <> x or aR * x = x )
;
suppose A245:
aR * x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
A248:
(aR * bR) + (aR * x) = aR * (bR + x)
by VECTSP_1:def 2;
per cases
( (aR * bR) + (aR * x) <> x or (aR * bR) + (aR * x) = x )
;
suppose A249:
(aR * bR) + (aR * x) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A250:
(aR * bR) + (aR * x) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; suppose A251:
aR * x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A253:
(aR * bR) + x = aR * (bR + x)
by A251, VECTSP_1:def 2;
per cases
( (aR * bR) + x <> x or (aR * bR) + x = x )
;
suppose A254:
(aR * bR) + x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A255:
(aR * bR) + x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; suppose A256:
bR + x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( aR * x <> x or aR * x = x )
;
suppose A258:
aR * x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; suppose A262:
aR * x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
;
verum end; end; end; suppose A265:
c <> o
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
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
( bR + cR <> x or bR + cR = x )
;
suppose A268:
bR + cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( aR * cR <> x or aR * cR = x )
;
suppose A271:
aR * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( (aR * bR) + (aR * cR) <> x or (aR * bR) + (aR * cR) = x )
;
suppose A274:
(aR * bR) + (aR * cR) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A275:
(aR * bR) + (aR * cR) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; suppose A276:
aR * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( (aR * bR) + x <> x or (aR * bR) + x = x )
;
suppose A278:
(aR * bR) + x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A280:
(aR * bR) + x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; suppose A281:
bR + cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
per cases
( aR * cR <> x or aR * cR = x )
;
suppose A283:
aR * cR <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by Def8;
per cases
( (aR * bR) + (aR * cR) <> x or (aR * bR) + (aR * cR) = x )
;
suppose A286:
(aR * bR) + (aR * cR) <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A287:
(aR * bR) + (aR * cR) = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; suppose A288:
aR * cR = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
carr (
x,
o)
by XBOOLE_0:def 3;
A290:
(aR * bR) + x = aR * (bR + cR)
by A288, VECTSP_1:def 2;
per cases
( (aR * bR) + x <> x or (aR * bR) + x = x )
;
suppose A291:
(aR * bR) + x <> x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; suppose A292:
(aR * bR) + x = x
;
(b1 * b2) + (b1 * b3) = b1 * (b2 + b3)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
;
verum end; end; end; end; end; end; end; end;
hence
ExField (x,o) is distributive
; verum