let x, y, z be Element of REAL ; * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
reconsider o = 0 as Element of REAL by Lm3;
per cases
( x = 0 or ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & x <> 0 & y in REAL+ & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & z in REAL+ & y in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & z in REAL+ ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & y in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) )
;
suppose A1:
x = 0
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))hence * (
x,
(+ (y,z))) =
0
by Th12
.=
+ (
o,
o)
by Th11
.=
+ (
(* (x,y)),
o)
by A1, Th12
.=
+ (
(* (x,y)),
(* (x,z)))
by A1, Th12
;
verum end; suppose that A2:
x in REAL+
and A3:
(
y in REAL+ &
z in REAL+ )
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))A4:
( ex
x9,
y9 being
Element of
REAL+ st
(
x = x9 &
y = y9 &
* (
x,
y)
= x9 *' y9 ) & ex
x99,
z9 being
Element of
REAL+ st
(
x = x99 &
z = z9 &
* (
x,
z)
= x99 *' z9 ) )
by A2, A3, Def2;
then A5:
ex
xy9,
xz9 being
Element of
REAL+ st
(
* (
x,
y)
= xy9 &
* (
x,
z)
= xz9 &
+ (
(* (x,y)),
(* (x,z)))
= xy9 + xz9 )
by Def1;
A6:
ex
y99,
z99 being
Element of
REAL+ st
(
y = y99 &
z = z99 &
+ (
y,
z)
= y99 + z99 )
by A3, Def1;
then
ex
x999,
yz9 being
Element of
REAL+ st
(
x = x999 &
+ (
y,
z)
= yz9 &
* (
x,
(+ (y,z)))
= x999 *' yz9 )
by A2, Def2;
hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
by A4, A5, A6, ARYTM_2:13;
verum end; suppose that A7:
(
x in REAL+ &
x <> 0 )
and A8:
y in REAL+
and A9:
z in [:{0},REAL+:] \ {[0,0]}
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))consider y99,
z99 being
Element of
REAL+ such that A10:
y = y99
and A11:
z = [0,z99]
and A12:
+ (
y,
z)
= y99 - z99
by A8, A9, Def1;
consider x9,
y9 being
Element of
REAL+ such that A13:
(
x = x9 &
y = y9 )
and A14:
* (
x,
y)
= x9 *' y9
by A7, A8, Def2;
consider x99,
z9 being
Element of
REAL+ such that A15:
x = x99
and A16:
z = [0,z9]
and A17:
* (
x,
z)
= [0,(x99 *' z9)]
by A7, A9, Def2;
* (
x,
z)
in [:{0},REAL+:]
by A17, Lm1;
then A18:
ex
xy9,
xz9 being
Element of
REAL+ st
(
* (
x,
y)
= xy9 &
* (
x,
z)
= [0,xz9] &
+ (
(* (x,y)),
(* (x,z)))
= xy9 - xz9 )
by A14, Def1;
A19:
z9 = z99
by A16, A11, XTUPLE_0:1;
now * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))per cases
( z99 <=' y99 or not z99 <=' y99 )
;
suppose A20:
z99 <=' y99
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then A21:
+ (
y,
z)
= y99 -' z99
by A12, ARYTM_1:def 2;
then
ex
x999,
yz9 being
Element of
REAL+ st
(
x = x999 &
+ (
y,
z)
= yz9 &
* (
x,
(+ (y,z)))
= x999 *' yz9 )
by A7, Def2;
hence * (
x,
(+ (y,z))) =
(x9 *' y9) - (x99 *' z9)
by A13, A15, A10, A19, A20, A21, ARYTM_1:26
.=
+ (
(* (x,y)),
(* (x,z)))
by A14, A17, A18, XTUPLE_0:1
;
verum end; suppose A22:
not
z99 <=' y99
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then A23:
+ (
y,
z)
= [0,(z99 -' y99)]
by A12, ARYTM_1:def 2;
then
+ (
y,
z)
in [:{0},REAL+:]
by Lm1;
then consider x999,
yz9 being
Element of
REAL+ such that A24:
x = x999
and A25:
(
+ (
y,
z)
= [0,yz9] &
* (
x,
(+ (y,z)))
= [0,(x999 *' yz9)] )
by A7, Def2;
thus * (
x,
(+ (y,z))) =
[0,(x999 *' (z99 -' y99))]
by A23, A25, XTUPLE_0:1
.=
(x9 *' y9) - (x99 *' z9)
by A7, A13, A15, A10, A19, A22, A24, ARYTM_1:27
.=
+ (
(* (x,y)),
(* (x,z)))
by A14, A17, A18, XTUPLE_0:1
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; suppose that A26:
(
x in REAL+ &
x <> 0 )
and A27:
z in REAL+
and A28:
y in [:{0},REAL+:] \ {[0,0]}
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))consider z99,
y99 being
Element of
REAL+ such that A29:
z = z99
and A30:
y = [0,y99]
and A31:
+ (
z,
y)
= z99 - y99
by A27, A28, Def1;
consider x9,
z9 being
Element of
REAL+ such that A32:
(
x = x9 &
z = z9 )
and A33:
* (
x,
z)
= x9 *' z9
by A26, A27, Def2;
consider x99,
y9 being
Element of
REAL+ such that A34:
x = x99
and A35:
y = [0,y9]
and A36:
* (
x,
y)
= [0,(x99 *' y9)]
by A26, A28, Def2;
* (
x,
y)
in [:{0},REAL+:]
by A36, Lm1;
then A37:
ex
xz9,
xy9 being
Element of
REAL+ st
(
* (
x,
z)
= xz9 &
* (
x,
y)
= [0,xy9] &
+ (
(* (x,z)),
(* (x,y)))
= xz9 - xy9 )
by A33, Def1;
A38:
y9 = y99
by A35, A30, XTUPLE_0:1;
now * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))per cases
( y99 <=' z99 or not y99 <=' z99 )
;
suppose A39:
y99 <=' z99
;
* (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))then A40:
+ (
z,
y)
= z99 -' y99
by A31, ARYTM_1:def 2;
then
ex
x999,
zy9 being
Element of
REAL+ st
(
x = x999 &
+ (
z,
y)
= zy9 &
* (
x,
(+ (z,y)))
= x999 *' zy9 )
by A26, Def2;
hence * (
x,
(+ (z,y))) =
(x9 *' z9) - (x99 *' y9)
by A32, A34, A29, A38, A39, A40, ARYTM_1:26
.=
+ (
(* (x,z)),
(* (x,y)))
by A33, A36, A37, XTUPLE_0:1
;
verum end; suppose A41:
not
y99 <=' z99
;
* (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))then A42:
+ (
z,
y)
= [0,(y99 -' z99)]
by A31, ARYTM_1:def 2;
then
+ (
z,
y)
in [:{0},REAL+:]
by Lm1;
then consider x999,
zy9 being
Element of
REAL+ such that A43:
x = x999
and A44:
(
+ (
z,
y)
= [0,zy9] &
* (
x,
(+ (z,y)))
= [0,(x999 *' zy9)] )
by A26, Def2;
thus * (
x,
(+ (z,y))) =
[0,(x999 *' (y99 -' z99))]
by A42, A44, XTUPLE_0:1
.=
(x9 *' z9) - (x99 *' y9)
by A26, A32, A34, A29, A38, A41, A43, ARYTM_1:27
.=
+ (
(* (x,z)),
(* (x,y)))
by A33, A36, A37, XTUPLE_0:1
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; suppose that A45:
(
x in REAL+ &
x <> 0 )
and A46:
y in [:{0},REAL+:] \ {[0,0]}
and A47:
z in [:{0},REAL+:] \ {[0,0]}
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
( ( not
y in REAL+ or not
z in [:{0},REAL+:] ) & ( not
y in [:{0},REAL+:] or not
z in REAL+ ) )
by A46, A47, Th5, XBOOLE_0:3;
then consider y99,
z99 being
Element of
REAL+ such that A48:
y = [0,y99]
and A49:
z = [0,z99]
and A50:
+ (
y,
z)
= [0,(y99 + z99)]
by A46, Def1;
+ (
y,
z)
in [:{0},REAL+:]
by A50, Lm1;
then consider x999,
yz9 being
Element of
REAL+ such that A51:
x = x999
and A52:
(
+ (
y,
z)
= [0,yz9] &
* (
x,
(+ (y,z)))
= [0,(x999 *' yz9)] )
by A45, Def2;
consider x9,
y9 being
Element of
REAL+ such that A53:
x = x9
and A54:
y = [0,y9]
and A55:
* (
x,
y)
= [0,(x9 *' y9)]
by A45, A46, Def2;
A56:
y9 = y99
by A54, A48, XTUPLE_0:1;
consider x99,
z9 being
Element of
REAL+ such that A57:
x = x99
and A58:
z = [0,z9]
and A59:
* (
x,
z)
= [0,(x99 *' z9)]
by A45, A47, Def2;
* (
x,
z)
in [:{0},REAL+:]
by A59, Lm1;
then A60:
( not
* (
x,
y)
in [:{0},REAL+:] or not
* (
x,
z)
in REAL+ )
by Th5, XBOOLE_0:3;
* (
x,
y)
in [:{0},REAL+:]
by A55, Lm1;
then
( not
* (
x,
y)
in REAL+ or not
* (
x,
z)
in [:{0},REAL+:] )
by Th5, XBOOLE_0:3;
then consider xy9,
xz9 being
Element of
REAL+ such that A61:
* (
x,
y)
= [0,xy9]
and A62:
(
* (
x,
z)
= [0,xz9] &
+ (
(* (x,y)),
(* (x,z)))
= [0,(xy9 + xz9)] )
by A55, A60, Def1, Lm1;
A63:
xy9 = x9 *' y9
by A55, A61, XTUPLE_0:1;
A64:
z9 = z99
by A58, A49, XTUPLE_0:1;
thus * (
x,
(+ (y,z))) =
[0,(x999 *' (y99 + z99))]
by A50, A52, XTUPLE_0:1
.=
[0,((x9 *' y9) + (x9 *' z9))]
by A53, A51, A56, A64, ARYTM_2:13
.=
+ (
(* (x,y)),
(* (x,z)))
by A53, A57, A59, A62, A63, XTUPLE_0:1
;
verum end; suppose that A65:
x in [:{0},REAL+:] \ {[0,0]}
and A66:
y in REAL+
and A67:
z in REAL+
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))consider y99,
z99 being
Element of
REAL+ such that A68:
y = y99
and A69:
z = z99
and A70:
+ (
y,
z)
= y99 + z99
by A66, A67, Def1;
now * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))per cases
( ( y <> 0 & z <> 0 ) or x = 0 or z = 0 or y = 0 )
;
suppose that A71:
y <> 0
and A72:
z <> 0
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))consider x99,
z9 being
Element of
REAL+ such that A73:
x = [0,x99]
and A74:
z = z9
and A75:
* (
x,
z)
= [0,(z9 *' x99)]
by A65, A67, A72, Def2;
y99 + z99 <> 0
by A69, A72, ARYTM_2:5;
then consider x999,
yz9 being
Element of
REAL+ such that A76:
x = [0,x999]
and A77:
(
+ (
y,
z)
= yz9 &
* (
x,
(+ (y,z)))
= [0,(yz9 *' x999)] )
by A65, A70, Def2;
consider x9,
y9 being
Element of
REAL+ such that A78:
x = [0,x9]
and A79:
y = y9
and A80:
* (
x,
y)
= [0,(y9 *' x9)]
by A65, A66, A71, Def2;
A81:
x99 = x999
by A73, A76, XTUPLE_0:1;
* (
x,
z)
in [:{0},REAL+:]
by A75, Lm1;
then A82:
( not
* (
x,
y)
in [:{0},REAL+:] or not
* (
x,
z)
in REAL+ )
by Th5, XBOOLE_0:3;
* (
x,
y)
in [:{0},REAL+:]
by A80, Lm1;
then
( not
* (
x,
y)
in REAL+ or not
* (
x,
z)
in [:{0},REAL+:] )
by Th5, XBOOLE_0:3;
then consider xy9,
xz9 being
Element of
REAL+ such that A83:
* (
x,
y)
= [0,xy9]
and A84:
(
* (
x,
z)
= [0,xz9] &
+ (
(* (x,y)),
(* (x,z)))
= [0,(xy9 + xz9)] )
by A80, A82, Def1, Lm1;
A85:
xy9 = x9 *' y9
by A80, A83, XTUPLE_0:1;
x9 = x99
by A78, A73, XTUPLE_0:1;
hence * (
x,
(+ (y,z))) =
[0,((x9 *' y9) + (x99 *' z9))]
by A68, A69, A70, A79, A74, A77, A81, ARYTM_2:13
.=
+ (
(* (x,y)),
(* (x,z)))
by A75, A84, A85, XTUPLE_0:1
;
verum end; suppose A86:
x = 0
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))hence * (
x,
(+ (y,z))) =
0
by Th12
.=
+ (
o,
o)
by Th11
.=
+ (
(* (x,y)),
o)
by A86, Th12
.=
+ (
(* (x,y)),
(* (x,z)))
by A86, Th12
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; suppose that A89:
x in [:{0},REAL+:] \ {[0,0]}
and A90:
y in REAL+
and A91:
z in [:{0},REAL+:] \ {[0,0]}
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))consider x99,
z9 being
Element of
REAL+ such that A92:
x = [0,x99]
and A93:
z = [0,z9]
and A94:
* (
x,
z)
= z9 *' x99
by A89, A91, Def2;
now * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))per cases
( y <> 0 or y = 0 )
;
suppose
y <> 0
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then consider x9,
y9 being
Element of
REAL+ such that A95:
x = [0,x9]
and A96:
y = y9
and A97:
* (
x,
y)
= [0,(y9 *' x9)]
by A89, A90, Def2;
* (
x,
y)
in [:{0},REAL+:]
by A97, Lm1;
then consider xy9,
xz9 being
Element of
REAL+ such that A98:
* (
x,
y)
= [0,xy9]
and A99:
(
* (
x,
z)
= xz9 &
+ (
(* (x,y)),
(* (x,z)))
= xz9 - xy9 )
by A94, Def1;
consider y99,
z99 being
Element of
REAL+ such that A100:
y = y99
and A101:
z = [0,z99]
and A102:
+ (
y,
z)
= y99 - z99
by A91, A96, Def1;
A103:
z9 = z99
by A93, A101, XTUPLE_0:1;
now * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))per cases
( z99 <=' y99 or not z99 <=' y99 )
;
suppose A104:
z99 <=' y99
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then A105:
+ (
y,
z)
= y99 -' z99
by A102, ARYTM_1:def 2;
now * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))per cases
( + (y,z) <> 0 or + (y,z) = 0 )
;
suppose A106:
+ (
y,
z)
<> 0
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then consider x999,
yz9 being
Element of
REAL+ such that A107:
x = [0,x999]
and A108:
(
+ (
y,
z)
= yz9 &
* (
x,
(+ (y,z)))
= [0,(yz9 *' x999)] )
by A89, A105, Def2;
not
x in {[0,0]}
by XBOOLE_0:def 5;
then A109:
x999 <> 0
by A107, TARSKI:def 1;
A110:
z9 = z99
by A93, A101, XTUPLE_0:1;
A111:
x9 = x99
by A92, A95, XTUPLE_0:1;
x99 = x999
by A92, A107, XTUPLE_0:1;
hence * (
x,
(+ (y,z))) =
(x9 *' z9) - (x9 *' y9)
by A96, A100, A104, A105, A106, A108, A111, A110, A109, ARYTM_1:28
.=
+ (
(* (x,y)),
(* (x,z)))
by A94, A97, A98, A99, A111, XTUPLE_0:1
;
verum end; suppose A112:
+ (
y,
z)
= 0
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then A113:
y99 = z99
by A104, A105, ARYTM_1:10;
A114:
(
xy9 = x9 *' y9 &
x9 = x99 )
by A92, A95, A97, A98, XTUPLE_0:1;
thus * (
x,
(+ (y,z))) =
0
by A112, Th12
.=
+ (
(* (x,y)),
(* (x,z)))
by A94, A96, A100, A99, A103, A113, A114, ARYTM_1:18
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; suppose A115:
not
z99 <=' y99
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then A116:
+ (
y,
z)
= [0,(z99 -' y99)]
by A102, ARYTM_1:def 2;
then
+ (
y,
z)
in [:{0},REAL+:]
by Lm1;
then consider x999,
yz9 being
Element of
REAL+ such that A117:
x = [0,x999]
and A118:
(
+ (
y,
z)
= [0,yz9] &
* (
x,
(+ (y,z)))
= yz9 *' x999 )
by A89, Def2;
A119:
x99 = x999
by A92, A117, XTUPLE_0:1;
A120:
x9 = x99
by A92, A95, XTUPLE_0:1;
thus * (
x,
(+ (y,z))) =
x999 *' (z99 -' y99)
by A116, A118, XTUPLE_0:1
.=
(x99 *' z9) - (x9 *' y9)
by A96, A100, A103, A115, A120, A119, ARYTM_1:26
.=
+ (
(* (x,y)),
(* (x,z)))
by A94, A97, A98, A99, XTUPLE_0:1
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; suppose that A122:
x in [:{0},REAL+:] \ {[0,0]}
and A123:
z in REAL+
and A124:
y in [:{0},REAL+:] \ {[0,0]}
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))consider x99,
y9 being
Element of
REAL+ such that A125:
x = [0,x99]
and A126:
y = [0,y9]
and A127:
* (
x,
y)
= y9 *' x99
by A122, A124, Def2;
now * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))per cases
( z <> 0 or z = 0 )
;
suppose
z <> 0
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then consider x9,
z9 being
Element of
REAL+ such that A128:
x = [0,x9]
and A129:
z = z9
and A130:
* (
x,
z)
= [0,(z9 *' x9)]
by A122, A123, Def2;
* (
x,
z)
in [:{0},REAL+:]
by A130, Lm1;
then consider xz9,
xy9 being
Element of
REAL+ such that A131:
* (
x,
z)
= [0,xz9]
and A132:
(
* (
x,
y)
= xy9 &
+ (
(* (x,z)),
(* (x,y)))
= xy9 - xz9 )
by A127, Def1;
consider z99,
y99 being
Element of
REAL+ such that A133:
z = z99
and A134:
y = [0,y99]
and A135:
+ (
z,
y)
= z99 - y99
by A124, A129, Def1;
A136:
y9 = y99
by A126, A134, XTUPLE_0:1;
now * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))per cases
( y99 <=' z99 or not y99 <=' z99 )
;
suppose A137:
y99 <=' z99
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then A138:
+ (
z,
y)
= z99 -' y99
by A135, ARYTM_1:def 2;
now * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))per cases
( + (z,y) <> 0 or + (z,y) = 0 )
;
suppose A139:
+ (
z,
y)
<> 0
;
* (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))then consider x999,
zy9 being
Element of
REAL+ such that A140:
x = [0,x999]
and A141:
(
+ (
z,
y)
= zy9 &
* (
x,
(+ (z,y)))
= [0,(zy9 *' x999)] )
by A122, A138, Def2;
not
x in {[0,0]}
by XBOOLE_0:def 5;
then A142:
x999 <> 0
by A140, TARSKI:def 1;
A143:
y9 = y99
by A126, A134, XTUPLE_0:1;
A144:
x9 = x99
by A125, A128, XTUPLE_0:1;
x99 = x999
by A125, A140, XTUPLE_0:1;
hence * (
x,
(+ (z,y))) =
(x9 *' y9) - (x9 *' z9)
by A129, A133, A137, A138, A139, A141, A144, A143, A142, ARYTM_1:28
.=
+ (
(* (x,z)),
(* (x,y)))
by A127, A130, A131, A132, A144, XTUPLE_0:1
;
verum end; suppose A145:
+ (
z,
y)
= 0
;
* (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))then A146:
z99 = y99
by A137, A138, ARYTM_1:10;
A147:
(
xz9 = x9 *' z9 &
x9 = x99 )
by A125, A128, A130, A131, XTUPLE_0:1;
thus * (
x,
(+ (z,y))) =
0
by A145, Th12
.=
+ (
(* (x,z)),
(* (x,y)))
by A127, A129, A133, A132, A136, A146, A147, ARYTM_1:18
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; suppose A148:
not
y99 <=' z99
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))then A149:
+ (
z,
y)
= [0,(y99 -' z99)]
by A135, ARYTM_1:def 2;
then
+ (
z,
y)
in [:{0},REAL+:]
by Lm1;
then consider x999,
zy9 being
Element of
REAL+ such that A150:
x = [0,x999]
and A151:
(
+ (
z,
y)
= [0,zy9] &
* (
x,
(+ (z,y)))
= zy9 *' x999 )
by A122, Def2;
A152:
x99 = x999
by A125, A150, XTUPLE_0:1;
A153:
x9 = x99
by A125, A128, XTUPLE_0:1;
thus * (
x,
(+ (y,z))) =
x999 *' (y99 -' z99)
by A149, A151, XTUPLE_0:1
.=
(x99 *' y9) - (x9 *' z9)
by A129, A133, A136, A148, A153, A152, ARYTM_1:26
.=
+ (
(* (x,y)),
(* (x,z)))
by A127, A130, A131, A132, XTUPLE_0:1
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; end; end; hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
;
verum end; suppose that A155:
x in [:{0},REAL+:] \ {[0,0]}
and A156:
y in [:{0},REAL+:] \ {[0,0]}
and A157:
z in [:{0},REAL+:] \ {[0,0]}
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
( ( not
y in REAL+ or not
z in [:{0},REAL+:] ) & ( not
y in [:{0},REAL+:] or not
z in REAL+ ) )
by A156, A157, Th5, XBOOLE_0:3;
then consider y99,
z99 being
Element of
REAL+ such that A158:
y = [0,y99]
and A159:
z = [0,z99]
and A160:
+ (
y,
z)
= [0,(y99 + z99)]
by A156, Def1;
consider x99,
z9 being
Element of
REAL+ such that A161:
x = [0,x99]
and A162:
z = [0,z9]
and A163:
* (
x,
z)
= z9 *' x99
by A155, A157, Def2;
A164:
z9 = z99
by A162, A159, XTUPLE_0:1;
consider x9,
y9 being
Element of
REAL+ such that A165:
x = [0,x9]
and A166:
y = [0,y9]
and A167:
* (
x,
y)
= y9 *' x9
by A155, A156, Def2;
A168:
y9 = y99
by A166, A158, XTUPLE_0:1;
+ (
y,
z)
in [:{0},REAL+:]
by A160, Lm1;
then consider x999,
yz9 being
Element of
REAL+ such that A169:
x = [0,x999]
and A170:
(
+ (
y,
z)
= [0,yz9] &
* (
x,
(+ (y,z)))
= yz9 *' x999 )
by A155, Def2;
A171:
x9 = x999
by A165, A169, XTUPLE_0:1;
A172:
( ex
xy9,
xz9 being
Element of
REAL+ st
(
* (
x,
y)
= xy9 &
* (
x,
z)
= xz9 &
+ (
(* (x,y)),
(* (x,z)))
= xy9 + xz9 ) &
x9 = x99 )
by A165, A167, A161, A163, Def1, XTUPLE_0:1;
thus * (
x,
(+ (y,z))) =
x999 *' (y99 + z99)
by A160, A170, XTUPLE_0:1
.=
+ (
(* (x,y)),
(* (x,z)))
by A167, A163, A172, A171, A168, A164, ARYTM_2:13
;
verum end; suppose A173:
( ( not
x in REAL+ or not
y in REAL+ or not
z in REAL+ ) & ( not
x in REAL+ or not
y in REAL+ or not
z in [:{0},REAL+:] \ {[0,0]} ) & ( not
x in REAL+ or not
y in [:{0},REAL+:] \ {[0,0]} or not
z in REAL+ ) & ( not
x in REAL+ or not
y in [:{0},REAL+:] \ {[0,0]} or not
z in [:{0},REAL+:] \ {[0,0]} ) & ( not
x in [:{0},REAL+:] \ {[0,0]} or not
y in REAL+ or not
z in REAL+ ) & ( not
x in [:{0},REAL+:] \ {[0,0]} or not
y in REAL+ or not
z in [:{0},REAL+:] \ {[0,0]} ) & ( not
x in [:{0},REAL+:] \ {[0,0]} or not
y in [:{0},REAL+:] \ {[0,0]} or not
z in REAL+ ) & ( not
x in [:{0},REAL+:] \ {[0,0]} or not
y in [:{0},REAL+:] \ {[0,0]} or not
z in [:{0},REAL+:] \ {[0,0]} ) )
;
* (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) REAL =
(REAL+ \ {[0,0]}) \/ ([:{0},REAL+:] \ {[0,0]})
by XBOOLE_1:42
.=
REAL+ \/ ([:{0},REAL+:] \ {[0,0]})
by ARYTM_2:3, ZFMISC_1:57
;
hence
* (
x,
(+ (y,z)))
= + (
(* (x,y)),
(* (x,z)))
by A173, XBOOLE_0:def 3;
verum end; end;