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
by XBOOLE_0:def 7;
then consider w being set 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, Th8;
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 4
.=
(((z `2 ) * (y `1 )) * (w `2 )) / (w `2 )
by GROUP_1:def 4
.=
((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 )
by VECTSP_1:def 13
;
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, Th8;
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 4
.=
(((z `2 ) * (x `1 )) * (w `2 )) / (w `2 )
by GROUP_1:def 4
.=
((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 )
by VECTSP_1:def 13
;
hence
z in QClass. x
by Def4;
verum
end;
hence
u = v
by A1, A4, A6, SUBSET_1:8; verum