let I be non degenerated commutative domRing-like Ring; for u, v being Element of Quot. I st u meets v holds
u = v
let u, v be Element of Quot. I; ( u meets v implies u = v )
consider x being Element of Q. I such that
A1:
u = QClass. x
by Def5;
assume
u /\ v <> {}
; XBOOLE_0:def 7 u = v
then
u meets v
;
then consider w being object such that
A2:
w in u
and
A3:
w in v
by XBOOLE_0:3;
consider y being Element of Q. I such that
A4:
v = QClass. y
by Def5;
reconsider w = w as Element of Q. I by A2;
A5:
(w `1) * (y `2) = (w `2) * (y `1)
by A4, A3, Def4;
A6:
for z being Element of Q. I st z in QClass. x holds
z in QClass. y
proof
let z be
Element of
Q. I;
( z in QClass. x implies z in QClass. y )
w `2 divides w `2
;
then A7:
w `2 divides ((z `2) * (y `1)) * (w `2)
by GCD_1:7;
assume
z in QClass. x
;
z in QClass. y
then A8:
(z `1) * (w `2) = (z `2) * (w `1)
by A1, A2, Th7;
then A9:
w `2 divides (z `2) * (w `1)
by GCD_1:def 1;
then A10:
w `2 divides ((z `2) * (w `1)) * (y `2)
by GCD_1:7;
A11:
w `2 <> 0. I
by Th2;
then (z `1) * (y `2) =
(((z `2) * (w `1)) / (w `2)) * (y `2)
by A8, A9, GCD_1:def 4
.=
(((z `2) * (w `1)) * (y `2)) / (w `2)
by A9, A10, A11, GCD_1:11
.=
((z `2) * ((w `2) * (y `1))) / (w `2)
by A5, GROUP_1:def 3
.=
(((z `2) * (y `1)) * (w `2)) / (w `2)
by GROUP_1:def 3
.=
((z `2) * (y `1)) * ((w `2) / (w `2))
by A7, A11, GCD_1:11
.=
((z `2) * (y `1)) * (1_ I)
by A11, GCD_1:9
.=
(z `2) * (y `1)
;
hence
z in QClass. y
by Def4;
verum
end;
A12:
(w `1) * (x `2) = (w `2) * (x `1)
by A1, A2, Def4;
for z being Element of Q. I st z in QClass. y holds
z in QClass. x
proof
let z be
Element of
Q. I;
( z in QClass. y implies z in QClass. x )
w `2 divides w `2
;
then A13:
w `2 divides ((z `2) * (x `1)) * (w `2)
by GCD_1:7;
assume
z in QClass. y
;
z in QClass. x
then A14:
(z `1) * (w `2) = (z `2) * (w `1)
by A4, A3, Th7;
then A15:
w `2 divides (z `2) * (w `1)
by GCD_1:def 1;
then A16:
w `2 divides ((z `2) * (w `1)) * (x `2)
by GCD_1:7;
A17:
w `2 <> 0. I
by Th2;
then (z `1) * (x `2) =
(((z `2) * (w `1)) / (w `2)) * (x `2)
by A14, A15, GCD_1:def 4
.=
(((z `2) * (w `1)) * (x `2)) / (w `2)
by A15, A16, A17, GCD_1:11
.=
((z `2) * ((w `2) * (x `1))) / (w `2)
by A12, GROUP_1:def 3
.=
(((z `2) * (x `1)) * (w `2)) / (w `2)
by GROUP_1:def 3
.=
((z `2) * (x `1)) * ((w `2) / (w `2))
by A13, A17, GCD_1:11
.=
((z `2) * (x `1)) * (1_ I)
by A17, GCD_1:9
.=
(z `2) * (x `1)
;
hence
z in QClass. x
by Def4;
verum
end;
hence
u = v
by A1, A4, A6, SUBSET_1:3; verum