set j = 1;
0 in NAT
;
then reconsider zz = 0 as Element of REAL by NUMBERS:19;
consider u1, u2, v1, v2 being Element of REAL such that
A13:
1 = [*u1,u2*]
and
A14:
( y = [*v1,v2*] & 1 * y = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*] )
by Def4;
A15:
u2 = 0
by A13, ARYTM_0:24, Lm2;
then A16:
+ ((* (u1,v2)),(* (u2,v1))) = * (u1,v2)
by ARYTM_0:11, ARYTM_0:12;
A17:
u1 = 1
by A13, A15, ARYTM_0:def 5;
+ (zz,(opp zz)) = 0
by ARYTM_0:def 3;
then A18:
opp zz = 0
by ARYTM_0:11;
A19: + ((* (u1,v1)),(opp (* (u2,v2)))) =
+ (v1,(opp (* (u2,v2))))
by A17, ARYTM_0:19
.=
+ (v1,(* ((opp u2),v2)))
by ARYTM_0:15
.=
+ (v1,(* (zz,v2)))
by A13, A18, ARYTM_0:24, Lm2
.=
v1
by ARYTM_0:11, ARYTM_0:12
;
set z = 0 ;
consider u1, u2, v1, v2 being Element of REAL such that
x " = [*u1,u2*]
and
A20:
0 = [*v1,v2*]
and
A21:
(x ") * 0 = [*(+ ((* (u1,v1)),(opp (* (u2,v2))))),(+ ((* (u1,v2)),(* (u2,v1))))*]
by Def4;
v2 = zz
by A20, ARYTM_0:24;
then A22:
v1 = 0
by A20, ARYTM_0:def 5;
then A23: + ((* (u1,v1)),(opp (* (u2,v2)))) =
opp (* (u2,v2))
by ARYTM_0:11, ARYTM_0:12
.=
0
by A18, A20, ARYTM_0:12, ARYTM_0:24
;
A24: + ((* (u1,v2)),(* (u2,v1))) =
+ (zz,(* (u2,v1)))
by A20, ARYTM_0:12, ARYTM_0:24
.=
* (u2,v1)
by ARYTM_0:11
.=
0
by A22, ARYTM_0:12
;
assume A25:
x * y = 0
; ORDINAL1:def 14 contradiction
A26: ((x ") * x) * y =
(x ") * (x * y)
by Lm5
.=
0
by A21, A23, A24, A25, ARYTM_0:def 5
;
((x ") * x) * y =
1 * y
by Def6
.=
y
by A14, A16, A17, A19, ARYTM_0:19
;
hence
contradiction
by A26; verum