consider x being Element of Q. I such that
A1:
u = QClass. x
by Def5;
x `2 <> 0. I
by Th2;
then reconsider t = [(- (x `1)),(x `2)] as Element of Q. I by Def1;
set M = QClass. t;
A2:
for z being Element of Q. I st ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) holds
z in QClass. t
proof
let z be
Element of
Q. I;
( ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) implies z in QClass. t )
given a being
Element of
Q. I such that A3:
a in u
and A4:
(z `1) * (a `2) = (z `2) * (- (a `1))
;
z in QClass. t
A5:
(a `1) * (x `2) = (a `2) * (x `1)
by A1, A3, Def4;
A6:
((z `1) * (x `2)) * (a `2) =
((z `2) * (- (a `1))) * (x `2)
by A4, GROUP_1:def 3
.=
(- ((z `2) * (a `1))) * (x `2)
by GCD_1:48
.=
((- (z `2)) * (a `1)) * (x `2)
by GCD_1:48
.=
(- (z `2)) * ((a `2) * (x `1))
by A5, GROUP_1:def 3
.=
((- (z `2)) * (x `1)) * (a `2)
by GROUP_1:def 3
.=
(- ((z `2) * (x `1))) * (a `2)
by GCD_1:48
.=
((z `2) * (- (x `1))) * (a `2)
by GCD_1:48
;
A7:
a `2 <> 0. I
by Th2;
a `2 divides a `2
;
then A8:
a `2 divides ((z `2) * (- (x `1))) * (a `2)
by GCD_1:7;
a `2 divides a `2
;
then A9:
a `2 divides ((z `1) * (x `2)) * (a `2)
by GCD_1:7;
(z `1) * (t `2) =
(z `1) * (x `2)
.=
((z `1) * (x `2)) * (1_ I)
.=
((z `1) * (x `2)) * ((a `2) / (a `2))
by A7, GCD_1:9
.=
(((z `2) * (- (x `1))) * (a `2)) / (a `2)
by A7, A6, A9, GCD_1:11
.=
((z `2) * (- (x `1))) * ((a `2) / (a `2))
by A7, A8, GCD_1:11
.=
((z `2) * (- (x `1))) * (1_ I)
by A7, GCD_1:9
.=
(z `2) * (- (x `1))
.=
(z `2) * (t `1)
;
hence
z in QClass. t
by Def4;
verum
end;
for z being Element of Q. I st z in QClass. t holds
ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) )
hence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) )
by A2; verum