let F be non degenerated almost_left_invertible commutative Ring; :: thesis: for a, b, c, d being Element of F st b <> 0. F & d <> 0. F holds
(a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
let a, b, c, d be Element of F; :: thesis: ( b <> 0. F & d <> 0. F implies (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) )
assume that
A1: b <> 0. F and
A2: d <> 0. F ; :: thesis: (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
((a * d) + (c * b)) / (b * d) = ((a * d) + (c * b)) * ((b " ) * (d " )) by A1, A2, GCD_1:53
.= (((a * d) + (c * b)) * (b " )) * (d " ) by GROUP_1:def 4
.= (((a * d) * (b " )) + ((c * b) * (b " ))) * (d " ) by VECTSP_1:def 12
.= (((a * d) * (b " )) + (c * (b * (b " )))) * (d " ) by GROUP_1:def 4
.= (((a * d) * (b " )) + (c * (1. F))) * (d " ) by A1, VECTSP_1:def 22
.= (((a * d) * (b " )) + c) * (d " ) by VECTSP_1:def 16
.= (((a * d) * (b " )) * (d " )) + (c * (d " )) by VECTSP_1:def 12
.= ((b " ) * ((a * d) * (d " ))) + (c * (d " )) by GROUP_1:def 4
.= ((b " ) * (a * (d * (d " )))) + (c * (d " )) by GROUP_1:def 4
.= ((b " ) * (a * (1. F))) + (c * (d " )) by A2, VECTSP_1:def 22
.= ((b " ) * a) + (c * (d " )) by VECTSP_1:def 16 ;
hence (a / b) + (c / d) = ((a * d) + (c * b)) / (b * d) ; :: thesis: verum