let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v being Element of Quot. I st u meets v holds
u = v
let u, v be Element of Quot. I; :: thesis: ( u meets v implies u = v )
assume A1:
u /\ v <> {}
; :: according to XBOOLE_0:def 7 :: thesis: u = v
consider x being Element of Q. I such that
A2:
u = QClass. x
by Def5;
consider y being Element of Q. I such that
A3:
v = QClass. y
by Def5;
u meets v
by A1, XBOOLE_0:def 7;
then consider w being set such that
A4:
( w in u & w in v )
by XBOOLE_0:3;
reconsider w = w as Element of Q. I by A4;
A5:
(w `1 ) * (x `2 ) = (w `2 ) * (x `1 )
by A2, A4, Def4;
A6:
(w `1 ) * (y `2 ) = (w `2 ) * (y `1 )
by A3, A4, Def4;
A7:
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;
:: thesis: ( z in QClass. x implies z in QClass. y )
assume
z in QClass. x
;
:: thesis: z in QClass. y
then A8:
(z `1 ) * (w `2 ) = (z `2 ) * (w `1 )
by A2, A4, 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;
w `2 divides w `2
;
then A11:
w `2 divides ((z `2 ) * (y `1 )) * (w `2 )
by GCD_1:7;
A12:
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, A12, GCD_1:11
.=
((z `2 ) * ((w `2 ) * (y `1 ))) / (w `2 )
by A6, 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 A11, A12, GCD_1:11
.=
((z `2 ) * (y `1 )) * (1_ I)
by A12, GCD_1:9
.=
(z `2 ) * (y `1 )
by VECTSP_1:def 13
;
hence
z in QClass. y
by Def4;
:: thesis: verum
end;
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;
:: thesis: ( z in QClass. y implies z in QClass. x )
assume
z in QClass. y
;
:: thesis: z in QClass. x
then A13:
(z `1 ) * (w `2 ) = (z `2 ) * (w `1 )
by A3, A4, Th8;
then A14:
w `2 divides (z `2 ) * (w `1 )
by GCD_1:def 1;
then A15:
w `2 divides ((z `2 ) * (w `1 )) * (x `2 )
by GCD_1:7;
w `2 divides w `2
;
then A16:
w `2 divides ((z `2 ) * (x `1 )) * (w `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 A13, A14, GCD_1:def 4
.=
(((z `2 ) * (w `1 )) * (x `2 )) / (w `2 )
by A14, A15, A17, GCD_1:11
.=
((z `2 ) * ((w `2 ) * (x `1 ))) / (w `2 )
by A5, 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 A16, 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;
:: thesis: verum
end;
hence
u = v
by A2, A3, A7, SUBSET_1:8; :: thesis: verum