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