let R be commutative domRing-like Ring; :: thesis: for a, b, c, d being Element of R st b <> 0. R & d <> 0. R & b divides a & d divides c holds
(a / b) * (c / d) = (a * c) / (b * d)
let a, b, c, d be Element of R; :: thesis: ( b <> 0. R & d <> 0. R & b divides a & d divides c implies (a / b) * (c / d) = (a * c) / (b * d) )
assume that
A1: ( b <> 0. R & d <> 0. R ) and
A2: ( b divides a & d divides c ) ; :: thesis: (a / b) * (c / d) = (a * c) / (b * d)
A3: b * d divides a * c by A2, Th3;
set z = (a * c) / (b * d);
set y = c / d;
set x = a / b;
A4: b * d <> 0. R by A1, VECTSP_2:def 1;
( (a / b) * b = a & (c / d) * d = c ) by A1, A2, Def4;
then ((a * c) / (b * d)) * (b * d) = ((a / b) * b) * ((c / d) * d) by A3, A4, Def4
.= (a / b) * (b * ((c / d) * d)) by GROUP_1:def 3
.= (a / b) * ((c / d) * (b * d)) by GROUP_1:def 3
.= ((a / b) * (c / d)) * (b * d) by GROUP_1:def 3 ;
hence (a / b) * (c / d) = (a * c) / (b * d) by A4, Th1; :: thesis: verum