let c1, c2 be Complex; :: thesis: ( ( 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 ) :: thesis: ( 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 ) :: thesis: ( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 )

proof

thus
( not z <> 0 & c1 = 0 & c2 = 0 implies c1 = c2 )
; :: thesis: verum
assume that

A19: z <> 0 and

A20: z * c1 = 1 and

A21: z * c2 = 1 ; :: thesis: 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)))))))*]

.= c2 by A21, A22 ;

:: thesis: verum

end;A19: z <> 0 and

A20: z * c1 = 1 and

A21: z * c2 = 1 ; :: thesis: 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

hence c1 =
[*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]
by A20
let z9 be Complex; :: thesis: ( z * z9 = 1 implies z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*] )

assume A23: z * z9 = 1 ; :: thesis: 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;

end;assume A23: z * z9 = 1 ; :: thesis: 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;

end;

suppose that A28:
x = 0
and

A29: y <> 0 ; :: thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]

A29: y <> 0 ; :: thesis: 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 ;

:: thesis: verum

end;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 ;

:: thesis: verum

suppose that A36:
opp y = 0
and

A37: x <> 0 ; :: thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]

A37: x <> 0 ; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

suppose that A45:
opp y <> 0
and

A46: x <> 0 ; :: thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]

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; :: thesis: verum

end;

A46: x <> 0 ; :: thesis: z9 = [*(* (x,(inv (+ ((* (x,x)),(* (y,y))))))),(* ((opp y),(inv (+ ((* (x,x)),(* (y,y)))))))*]

A47: now :: thesis: not + ((* ((* (x,x)),(inv (opp y)))),(opp y)) = 0

A50:
1 = [*j,zz*]
by ARYTM_0:def 5;assume
+ ((* ((* (x,x)),(inv (opp y)))),(opp y)) = 0
; :: thesis: contradiction

then + ((* ((* (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; :: thesis: verum

end;then + ((* ((* (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; :: thesis: verum

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; :: thesis: verum

.= c2 by A21, A22 ;

:: thesis: verum