let c1, c2 be Complex; ( ( z <> 0 & z * c1 = 1 & z * c2 = 1 implies c1 = c2 ) & ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 ) )
0 in NAT
;
then reconsider zz = 0 , j = 1 as Element of REAL by Lm2, NUMBERS:19;
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 A19:
z <> 0
and A20:
z * c1 = 1
and A21:
z * c2 = 1
;
c1 = c2
A22:
for
z9 being
Complex st
z * z9 = 1 holds
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
proof
let z9 be
Complex;
( z * z9 = 1 implies z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] )
assume A23:
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 A24:
z = [*x1,x2*]
and A25:
z9 = [*x9,y9*]
and A26:
1
= [*(+ ((* (x1,x9)),(opp (* (x2,y9))))),(+ ((* (x1,y9)),(* (x2,x9))))*]
by A23, Def4;
A27:
(
x = x1 &
y = x2 )
by A1, A24, ARYTM_0:10;
per cases
( ( x = 0 & y <> 0 ) or ( opp y = 0 & x <> 0 ) or ( opp y <> 0 & x <> 0 ) )
by A1, A19, ARYTM_0:def 5;
suppose that A28:
x = 0
and A29:
y <> 0
;
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
+ (
y,
(opp y))
= 0
by ARYTM_0:def 3;
then A30:
opp y <> 0
by A29, ARYTM_0:11;
(
* (
x,
y9)
= 0 &
* (
x,
x9)
= 0 )
by A28, ARYTM_0:12;
then A31: 1 =
[*(opp (* (y,y9))),(+ (zz,(* (y,x9))))*]
by A26, A27, ARYTM_0:11
.=
[*(opp (* (y,y9))),(* (y,x9))*]
by ARYTM_0:11
;
A32:
1
= [*j,zz*]
by ARYTM_0:def 5;
* (
(opp y),
y9) =
opp (* (y,y9))
by ARYTM_0:15
.=
1
by A31, A32, ARYTM_0:10
;
then A33:
y9 = inv (opp y)
by A30, ARYTM_0:def 4;
A34:
* (
x,
x)
= 0
by A28, ARYTM_0:12;
* (
(opp y),
(opp (inv y))) =
opp (* (y,(opp (inv y))))
by ARYTM_0:15
.=
opp (opp (* (y,(inv y))))
by ARYTM_0:15
.=
1
by A29, ARYTM_0:def 4
;
then A35:
inv (opp y) = opp (inv y)
by A30, ARYTM_0:def 4;
* (
y,
x9)
= 0
by A31, A32, ARYTM_0:10;
hence z9 =
[*zz,(inv (opp y))*]
by A25, A29, A33, ARYTM_0:21
.=
[*zz,(opp (* (j,(inv y))))*]
by A35, ARYTM_0:19
.=
[*zz,(opp (* ((* (y,(inv y))),(inv y))))*]
by A29, ARYTM_0:def 4
.=
[*zz,(opp (* (y,(* ((inv y),(inv y))))))*]
by ARYTM_0:13
.=
[*zz,(* ((opp y),(* ((inv y),(inv y)))))*]
by ARYTM_0:15
.=
[*zz,(* ((opp y),(inv (* (y,y)))))*]
by ARYTM_0:22
.=
[*zz,(* ((opp y),(inv (+ (zz,(* (y,y)))))))*]
by ARYTM_0:11
.=
[*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A28, A34, ARYTM_0:12
;
verum end; suppose that A36:
opp y = 0
and A37:
x <> 0
;
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
+ (
y,
(opp y))
= 0
by ARYTM_0:def 3;
then A38:
y = 0
by A36, ARYTM_0:11;
then A39:
* (
y,
x9)
= 0
by ARYTM_0:12;
opp (* (y,y9)) =
* (
(opp y),
y9)
by ARYTM_0:15
.=
0
by A36, ARYTM_0:12
;
then A40: 1 =
[*(* (x,x9)),(+ ((* (x,y9)),zz))*]
by A26, A27, A39, ARYTM_0:11
.=
[*(* (x,x9)),(* (x,y9))*]
by ARYTM_0:11
;
A41:
1
= [*j,zz*]
by ARYTM_0:def 5;
then
* (
x,
x9)
= 1
by A40, ARYTM_0:10;
then A42:
x9 = inv x
by A37, ARYTM_0:def 4;
* (
x,
y9)
= 0
by A40, A41, ARYTM_0:10;
then A43:
y9 = 0
by A37, ARYTM_0:21;
A44:
* (
y,
y)
= 0
by A38, ARYTM_0:12;
x9 =
* (
j,
(inv x))
by A42, ARYTM_0:19
.=
* (
(* (x,(inv x))),
(inv x))
by A37, ARYTM_0:def 4
.=
* (
x,
(* ((inv x),(inv x))))
by ARYTM_0:13
.=
* (
x,
(inv (* (x,x))))
by ARYTM_0:22
.=
* (
x,
(inv (+ ((* (x,x)),zz))))
by ARYTM_0:11
;
hence
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A25, A36, A43, A44, ARYTM_0:12;
verum end; suppose that A45:
opp y <> 0
and A46:
x <> 0
;
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]A47:
now not + ((* ((* (x,x)),(inv (opp y)))),(opp y)) = 0 assume
+ (
(* ((* (x,x)),(inv (opp y)))),
(opp y))
= 0
;
contradictionthen
+ (
(* ((* (x,x)),(inv (opp y)))),
(* ((opp y),j)))
= 0
by ARYTM_0:19;
then
+ (
(* ((* (x,x)),(inv (opp y)))),
(* ((opp y),(* ((opp y),(inv (opp y)))))))
= 0
by A45, ARYTM_0:def 4;
then
+ (
(* ((* (x,x)),(inv (opp y)))),
(* ((* ((opp y),(opp y))),(inv (opp y)))))
= 0
by ARYTM_0:13;
then A48:
* (
(inv (opp y)),
(+ ((* (x,x)),(* ((opp y),(opp y))))))
= 0
by ARYTM_0:14;
+ (
(* (x,x)),
(* ((opp y),(opp y))))
<> 0
by A46, ARYTM_0:17;
then A49:
inv (opp y) = 0
by A48, ARYTM_0:21;
* (
(opp y),
(inv (opp y)))
= 1
by A45, ARYTM_0:def 4;
hence
contradiction
by A49, ARYTM_0:12;
verum end; A50:
1
= [*j,zz*]
by ARYTM_0:def 5;
then
+ (
(* (x1,y9)),
(* (x2,x9)))
= 0
by A26, ARYTM_0:10;
then
* (
x,
y9)
= opp (* (y,x9))
by A27, ARYTM_0:def 3;
then
* (
x,
y9)
= * (
(opp y),
x9)
by ARYTM_0:15;
then A51:
x9 =
* (
(* (x,y9)),
(inv (opp y)))
by A45, ARYTM_0:20
.=
* (
x,
(* (y9,(inv (opp y)))))
by ARYTM_0:13
;
then
+ (
(* (x,(* (x,(* (y9,(inv (opp y)))))))),
(opp (* (y,y9))))
= 1
by A26, A27, A50, ARYTM_0:10;
then
+ (
(* ((* (x,x)),(* (y9,(inv (opp y)))))),
(opp (* (y,y9))))
= 1
by ARYTM_0:13;
then
+ (
(* ((* (x,x)),(* (y9,(inv (opp y)))))),
(* ((opp y),y9)))
= 1
by ARYTM_0:15;
then
+ (
(* (y9,(* ((* (x,x)),(inv (opp y)))))),
(* ((opp y),y9)))
= 1
by ARYTM_0:13;
then
* (
y9,
(+ ((* ((* (x,x)),(inv (opp y)))),(opp y))))
= 1
by ARYTM_0:14;
then A52:
y9 = inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))
by A47, ARYTM_0:def 4;
then A53:
x9 =
* (
x,
(inv (* ((+ ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp y)))))
by A51, ARYTM_0:22
.=
* (
x,
(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(* ((opp y),(opp y)))))))
by ARYTM_0:14
.=
* (
x,
(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp (* (y,(opp y))))))))
by ARYTM_0:15
.=
* (
x,
(inv (+ ((* ((* ((* (x,x)),(inv (opp y)))),(opp y))),(opp (opp (* (y,y))))))))
by ARYTM_0:15
.=
* (
x,
(inv (+ ((* ((* (x,x)),(* ((inv (opp y)),(opp y))))),(* (y,y))))))
by ARYTM_0:13
.=
* (
x,
(inv (+ ((* ((* (x,x)),j)),(* (y,y))))))
by A45, ARYTM_0:def 4
.=
* (
x,
(inv (+ ((* (x,x)),(* (y,y))))))
by ARYTM_0:19
;
y9 =
* (
j,
(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))))
by A52, ARYTM_0:19
.=
* (
(* ((opp y),(inv (opp y)))),
(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))))
by A45, ARYTM_0:def 4
.=
* (
(opp y),
(* ((inv (opp y)),(inv (+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))))))
by ARYTM_0:13
.=
* (
(opp y),
(inv (* ((opp y),(+ ((* ((* (x,x)),(inv (opp y)))),(opp y)))))))
by ARYTM_0:22
.=
* (
(opp y),
(inv (+ ((* ((opp y),(* ((* (x,x)),(inv (opp y)))))),(* ((opp y),(opp y)))))))
by ARYTM_0:14
.=
* (
(opp y),
(inv (+ ((* ((* (x,x)),(* ((opp y),(inv (opp y)))))),(* ((opp y),(opp y)))))))
by ARYTM_0:13
.=
* (
(opp y),
(inv (+ ((* ((* (x,x)),j)),(* ((opp y),(opp y)))))))
by A45, ARYTM_0:def 4
.=
* (
(opp y),
(inv (+ ((* (x,x)),(* ((opp y),(opp y)))))))
by ARYTM_0:19
.=
* (
(opp y),
(inv (+ ((* (x,x)),(opp (* (y,(opp y))))))))
by ARYTM_0:15
.=
* (
(opp y),
(inv (+ ((* (x,x)),(opp (opp (* (y,y))))))))
by ARYTM_0:15
.=
* (
(opp y),
(inv (+ ((* (x,x)),(* (y,y))))))
;
hence
z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A25, A53;
verum
end;
hence c1 =
[*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A20
.=
c2
by A21, A22
;
verum
end;
thus
( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 )
; verum