let R be commutative Ring; for S being non empty multiplicatively-closed Subset of R
for x, y, z being Element of Frac S st x,y Fr_Eq S & y,z Fr_Eq S holds
x,z Fr_Eq S
let S be non empty multiplicatively-closed Subset of R; for x, y, z being Element of Frac S st x,y Fr_Eq S & y,z Fr_Eq S holds
x,z Fr_Eq S
let x, y, z be Element of Frac S; ( x,y Fr_Eq S & y,z Fr_Eq S implies x,z Fr_Eq S )
assume
( x,y Fr_Eq S & y,z Fr_Eq S )
; x,z Fr_Eq S
then consider s1, s2 being Element of R such that
A2:
s1 in S
and
A3:
s2 in S
and
A4:
(((x `1) * (y `2)) - ((y `1) * (x `2))) * s1 = 0. R
and
A5:
(((y `1) * (z `2)) - ((z `1) * (y `2))) * s2 = 0. R
;
0. R =
((((x `1) * (y `2)) - ((y `1) * (x `2))) * s1) * (z `2)
by A4
.=
((((x `1) * (y `2)) * s1) - (((y `1) * (x `2)) * s1)) * (z `2)
by VECTSP_1:13
.=
((z `2) * (((x `1) * (y `2)) * s1)) - ((z `2) * (((y `1) * (x `2)) * s1))
by VECTSP_1:11
.=
((z `2) * ((x `1) * ((y `2) * s1))) - ((z `2) * (((y `1) * (x `2)) * s1))
by GROUP_1:def 3
.=
(((x `1) * (z `2)) * ((y `2) * s1)) - ((z `2) * (((y `1) * (x `2)) * s1))
by GROUP_1:def 3
;
then A7: 0. R =
((((x `1) * (z `2)) * ((y `2) * s1)) - ((z `2) * (((y `1) * (x `2)) * s1))) * s2
.=
((((x `1) * (z `2)) * ((y `2) * s1)) * s2) - (((z `2) * (((y `1) * (x `2)) * s1)) * s2)
by VECTSP_1:13
.=
(((x `1) * (z `2)) * (((y `2) * s1) * s2)) - (((z `2) * (((y `1) * (x `2)) * s1)) * s2)
by GROUP_1:def 3
.=
(((x `1) * (z `2)) * (((y `2) * s1) * s2)) - ((z `2) * ((((y `1) * (x `2)) * s1) * s2))
by GROUP_1:def 3
;
A8: 0. R =
((((y `1) * (z `2)) - ((z `1) * (y `2))) * s2) * (x `2)
by A5
.=
((((y `1) * (z `2)) * s2) - (((z `1) * (y `2)) * s2)) * (x `2)
by VECTSP_1:13
.=
((((y `1) * (z `2)) * s2) * (x `2)) - ((x `2) * (((z `1) * (y `2)) * s2))
by VECTSP_1:13
.=
((((y `1) * (z `2)) * s2) * (x `2)) - ((x `2) * ((z `1) * ((y `2) * s2)))
by GROUP_1:def 3
.=
((((y `1) * (z `2)) * s2) * (x `2)) - (((x `2) * (z `1)) * ((y `2) * s2))
by GROUP_1:def 3
.=
(((z `2) * ((y `1) * s2)) * (x `2)) - (((x `2) * (z `1)) * ((y `2) * s2))
by GROUP_1:def 3
.=
((z `2) * (((y `1) * s2) * (x `2))) - (((x `2) * (z `1)) * ((y `2) * s2))
by GROUP_1:def 3
.=
((z `2) * (((y `1) * (x `2)) * s2)) - (((x `2) * (z `1)) * ((y `2) * s2))
by GROUP_1:def 3
.=
((z `2) * (((y `1) * (x `2)) * s2)) - ((((z `1) * (x `2)) * (y `2)) * s2)
by GROUP_1:def 3
;
A9: 0. R =
(0. R) * s1
.=
(((z `2) * (((y `1) * (x `2)) * s2)) - (((z `1) * (x `2)) * ((y `2) * s2))) * s1
by A8, GROUP_1:def 3
.=
(((z `2) * (((y `1) * (x `2)) * s2)) * s1) - ((((z `1) * (x `2)) * ((y `2) * s2)) * s1)
by VECTSP_1:13
.=
((z `2) * ((((y `1) * (x `2)) * s2) * s1)) - ((((z `1) * (x `2)) * ((y `2) * s2)) * s1)
by GROUP_1:def 3
.=
((z `2) * ((((y `1) * (x `2)) * s2) * s1)) - (((z `1) * (x `2)) * (((y `2) * s2) * s1))
by GROUP_1:def 3
.=
((z `2) * ((((y `1) * (x `2)) * s1) * s2)) - (((z `1) * (x `2)) * (((y `2) * s2) * s1))
by GROUP_1:def 3
.=
((z `2) * ((((y `1) * (x `2)) * s1) * s2)) - (((z `1) * (x `2)) * (((y `2) * s1) * s2))
by GROUP_1:def 3
;
reconsider u = (z `2) * ((((y `1) * (x `2)) * s1) * s2) as Element of R ;
y `2 in S
by Lm17;
then reconsider v = (y `2) * s1 as Element of S by A2, C0SP1:def 4;
reconsider w = v * s2 as Element of S by A3, C0SP1:def 4;
0. R =
(((((x `1) * (z `2)) * (((y `2) * s1) * s2)) - u) + u) - (((z `1) * (x `2)) * (((y `2) * s1) * s2))
by A7, A9
.=
((((x `1) * (z `2)) * (((y `2) * s1) * s2)) + ((- u) + u)) - (((z `1) * (x `2)) * (((y `2) * s1) * s2))
by RLVECT_1:def 3
.=
((((x `1) * (z `2)) * (((y `2) * s1) * s2)) + (0. R)) - (((z `1) * (x `2)) * (((y `2) * s1) * s2))
by RLVECT_1:5
.=
(((x `1) * (z `2)) - ((z `1) * (x `2))) * w
by VECTSP_1:13
;
hence
x,z Fr_Eq S
; verum