let c1, c2 be complex number ; ( ( z <> 0 & z * c1 = 1 & z * c2 = 1 implies c1 = c2 ) & ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 ) )
thus
( z <> 0 & z * c1 = 1 & z * c2 = 1 implies c1 = c2 )
( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 )proof
assume that A29:
z <> 0
and A30:
z * c1 = 1
and A31:
z * c2 = 1
;
c1 = c2
A32:
for
z9 being
complex number st
z * z9 = 1 holds
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
proof
let z9 be
complex number ;
( z * z9 = 1 implies z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] )
assume A33:
z * z9 = 1
;
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
consider x1,
x2,
x9,
y9 being
Element of
REAL such that A34:
z = [*x1,x2*]
and A35:
z9 = [*x9,y9*]
and A36:
1
= [*(+ ((* (x1,x9)),(opp (* (x2,y9))))),(+ ((* (x1,y9)),(* (x2,x9))))*]
by A33, Def5;
A37:
(
x = x1 &
y = x2 )
by A2, A34, ARYTM_0:12;
per cases
( ( x = 0 & y <> 0 ) or ( opp y = 0 & x <> 0 ) or ( opp y <> 0 & x <> 0 ) )
by A2, A29, ARYTM_0:def 7;
suppose that A38:
x = 0
and A39:
y <> 0
;
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
+ (
y,
(opp y))
= 0
by ARYTM_0:def 4;
then A41:
opp y <> 0
by A39, ARYTM_0:13;
(
* (
x,
y9)
= 0 &
* (
x,
x9)
= 0 )
by A38, ARYTM_0:14;
then A43: 1 =
[*(opp (* (y,y9))),(+ (0,(* (y,x9))))*]
by A36, A37, ARYTM_0:13
.=
[*(opp (* (y,y9))),(* (y,x9))*]
by ARYTM_0:13
;
A44:
1
= [*j,0*]
by ARYTM_0:def 7;
* (
(opp y),
y9) =
opp (* (y,y9))
by ARYTM_0:17
.=
1
by A43, A44, ARYTM_0:12
;
then A46:
y9 = inv (opp y)
by A41, ARYTM_0:def 5;
A47:
* (
x,
x)
= 0
by A38, ARYTM_0:14;
* (
(opp y),
(opp (inv y))) =
opp (* (y,(opp (inv y))))
by ARYTM_0:17
.=
opp (opp (* (y,(inv y))))
by ARYTM_0:17
.=
1
by A39, ARYTM_0:def 5
;
then A49:
inv (opp y) = opp (inv y)
by A41, ARYTM_0:def 5;
* (
y,
x9)
= 0
by A43, A44, ARYTM_0:12;
hence z9 =
[*0,(inv (opp y))*]
by A35, A39, A46, ARYTM_0:23
.=
[*0,(opp (* (j,(inv y))))*]
by A49, ARYTM_0:21
.=
[*0,(opp (* ((* (y,(inv y))),(inv y))))*]
by A39, ARYTM_0:def 5
.=
[*0,(opp (* (y,(* ((inv y),(inv y))))))*]
by ARYTM_0:15
.=
[*0,(* ((opp y),(* ((inv y),(inv y)))))*]
by ARYTM_0:17
.=
[*0,(* ((opp y),(inv (* (y,y)))))*]
by ARYTM_0:24
.=
[*0,(* ((opp y),(inv (+ (0,(* (y,y)))))))*]
by ARYTM_0:13
.=
[*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A38, A47, ARYTM_0:14
;
verum end; suppose that A51:
opp y = 0
and A52:
x <> 0
;
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
+ (
y,
(opp y))
= 0
by ARYTM_0:def 4;
then A54:
y = 0
by A51, ARYTM_0:13;
then A55:
* (
y,
x9)
= 0
by ARYTM_0:14;
opp (* (y,y9)) =
* (
(opp y),
y9)
by ARYTM_0:17
.=
0
by A51, ARYTM_0:14
;
then A57: 1 =
[*(* (x,x9)),(+ ((* (x,y9)),0))*]
by A36, A37, A55, ARYTM_0:13
.=
[*(* (x,x9)),(* (x,y9))*]
by ARYTM_0:13
;
A58:
1
= [*j,0*]
by ARYTM_0:def 7;
then
* (
x,
x9)
= 1
by A57, ARYTM_0:12;
then A60:
x9 = inv x
by A52, ARYTM_0:def 5;
* (
x,
y9)
= 0
by A57, A58, ARYTM_0:12;
then A62:
y9 = 0
by A52, ARYTM_0:23;
A63:
* (
y,
y)
= 0
by A54, ARYTM_0:14;
x9 =
* (
j,
(inv x))
by A60, ARYTM_0:21
.=
* (
(* (x,(inv x))),
(inv x))
by A52, ARYTM_0:def 5
.=
* (
x,
(* ((inv x),(inv x))))
by ARYTM_0:15
.=
* (
x,
(inv (* (x,x))))
by ARYTM_0:24
.=
* (
x,
(inv (+ ((* (x,x)),0))))
by ARYTM_0:13
;
hence
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A35, A51, A62, A63, ARYTM_0:14;
verum end; suppose that A65:
opp y <> 0
and A66:
x <> 0
;
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]A67:
now assume
+ (
(* ((* (x,x)),(inv (opp y)))),
(opp y))
= 0
;
contradictionthen
+ (
(* ((* (x,x)),(inv (opp y)))),
(* ((opp y),j)))
= 0
by ARYTM_0:21;
then
+ (
(* ((* (x,x)),(inv (opp y)))),
(* ((opp y),(* ((opp y),(inv (opp y)))))))
= 0
by A65, ARYTM_0:def 5;
then
+ (
(* ((* (x,x)),(inv (opp y)))),
(* ((* ((opp y),(opp y))),(inv (opp y)))))
= 0
by ARYTM_0:15;
then A72:
* (
(inv (opp y)),
(+ ((* (x,x)),(* ((opp y),(opp y))))))
= 0
by ARYTM_0:16;
+ (
(* (x,x)),
(* ((opp y),(opp y))))
<> 0
by A66, ARYTM_0:19;
then A74:
inv (opp y) = 0
by A72, ARYTM_0:23;
* (
(opp y),
(inv (opp y)))
= 1
by A65, ARYTM_0:def 5;
hence
contradiction
by A74, ARYTM_0:14;
verum end; reconsider j = 1 as
Element of
REAL ;
A76:
1
= [*j,0*]
by ARYTM_0:def 7;
then
+ (
(* (x1,y9)),
(* (x2,x9)))
= 0
by A36, ARYTM_0:12;
then
* (
x,
y9)
= opp (* (y,x9))
by A37, ARYTM_0:def 4;
then
* (
x,
y9)
= * (
(opp y),
x9)
by ARYTM_0:17;
then A80:
x9 =
* (
(* (x,y9)),
(inv (opp y)))
by A65, ARYTM_0:22
.=
* (
x,
(* (y9,(inv (opp y)))))
by ARYTM_0:15
;
then
+ (
(* (x,(* (x,(* (y9,(inv (opp y)))))))),
(opp (* (y,y9))))
= 1
by A36, A37, A76, ARYTM_0:12;
then
+ (
(* ((* (x,x)),(* (y9,(inv (opp y)))))),
(opp (* (y,y9))))
= 1
by ARYTM_0:15;
then
+ (
(* ((* (x,x)),(* (y9,(inv (opp y)))))),
(* ((opp y),y9)))
= 1
by ARYTM_0:17;
then
+ (
(* (y9,(* ((* (x,x)),(inv (opp y)))))),
(* ((opp y),y9)))
= 1
by ARYTM_0:15;
then
* (
y9,
(+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))
= 1
by ARYTM_0:16;
then A86:
y9 = inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))
by A67, ARYTM_0:def 5;
then A87:
x9 =
* (
x,
(inv (* ((+ ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp y)))))
by A80, ARYTM_0:24
.=
* (
x,
(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(* ((opp y),(opp y)))))))
by ARYTM_0:16
.=
* (
x,
(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp (* (y,(opp y))))))))
by ARYTM_0:17
.=
* (
x,
(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp (opp (* (y,y))))))))
by ARYTM_0:17
.=
* (
x,
(inv (+ ((* ((* (x,x)),(* ((inv (opp y)),(opp y))))),(* (y,y))))))
by ARYTM_0:15
.=
* (
x,
(inv (+ ((* ((* (x,x)),j)),(* (y,y))))))
by A65, ARYTM_0:def 5
.=
* (
x,
(inv (+ ((* (x,x)),(* (y,y))))))
by ARYTM_0:21
;
y9 =
* (
j,
(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))))
by A86, ARYTM_0:21
.=
* (
(* ((opp y),(inv (opp y)))),
(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))))
by A65, ARYTM_0:def 5
.=
* (
(opp y),
(* ((inv (opp y)),(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))))))
by ARYTM_0:15
.=
* (
(opp y),
(inv (* ((opp y),(+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))))))
by ARYTM_0:24
.=
* (
(opp y),
(inv (+ ((* ((opp y),(* ((* (x,x)),(inv (opp y)))))),(* ((opp y),(opp y)))))))
by ARYTM_0:16
.=
* (
(opp y),
(inv (+ ((* ((* (x,x)),(* ((opp y),(inv (opp y)))))),(* ((opp y),(opp y)))))))
by ARYTM_0:15
.=
* (
(opp y),
(inv (+ ((* ((* (x,x)),j)),(* ((opp y),(opp y)))))))
by A65, ARYTM_0:def 5
.=
* (
(opp y),
(inv (+ ((* (x,x)),(* ((opp y),(opp y)))))))
by ARYTM_0:21
.=
* (
(opp y),
(inv (+ ((* (x,x)),(opp (* (y,(opp y))))))))
by ARYTM_0:17
.=
* (
(opp y),
(inv (+ ((* (x,x)),(opp (opp (* (y,y))))))))
by ARYTM_0:17
.=
* (
(opp y),
(inv (+ ((* (x,x)),(* (y,y))))))
;
hence
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A35, A87;
verum
end;
hence c1 =
[*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A30
.=
c2
by A31, A32
;
verum
end;
thus
( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 )
; verum