let K be Ring; :: thesis: for V being LeftMod of K

for W being Subspace of V holds

( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

let V be LeftMod of K; :: thesis: for W being Subspace of V holds

( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

let W be Subspace of V; :: thesis: ( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

A1: for x, y, z being Element of (V . W)

for x9, y9, z9 being Vector of (V / W) st x = x9 & y = y9 & z = z9 holds

x + y = x9 + y9 ;

thus V / W is Abelian :: thesis: ( V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

reconsider x9 = x as Element of (V . W) ;

consider b being Element of (V . W) such that

A2: x9 + b = 0. (V . W) by ALGSTR_0:def 11;

reconsider b9 = b as Vector of (V / W) ;

take b9 ; :: according to ALGSTR_0:def 11 :: thesis: x + b9 = 0. (V / W)

thus x + b9 = 0. (V / W) by A2; :: thesis: verum

for W being Subspace of V holds

( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

let V be LeftMod of K; :: thesis: for W being Subspace of V holds

( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

let W be Subspace of V; :: thesis: ( V / W is Abelian & V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

A1: for x, y, z being Element of (V . W)

for x9, y9, z9 being Vector of (V / W) st x = x9 & y = y9 & z = z9 holds

x + y = x9 + y9 ;

thus V / W is Abelian :: thesis: ( V / W is add-associative & V / W is right_zeroed & V / W is right_complementable )

proof

let x, y be Vector of (V / W); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x

reconsider x9 = x, y9 = y as Element of (V . W) ;

thus x + y = x9 + y9

.= y + x by A1 ; :: thesis: verum

end;reconsider x9 = x, y9 = y as Element of (V . W) ;

thus x + y = x9 + y9

.= y + x by A1 ; :: thesis: verum

hereby :: according to RLVECT_1:def 3 :: thesis: ( V / W is right_zeroed & V / W is right_complementable )

let x, y, z be Vector of (V / W); :: thesis: (x + y) + z = x + (y + z)

reconsider x9 = x, y9 = y, z9 = z as Element of (V . W) ;

thus (x + y) + z = (x9 + y9) + z9

.= x9 + (y9 + z9) by RLVECT_1:def 3

.= x + (y + z) ; :: thesis: verum

end;reconsider x9 = x, y9 = y, z9 = z as Element of (V . W) ;

thus (x + y) + z = (x9 + y9) + z9

.= x9 + (y9 + z9) by RLVECT_1:def 3

.= x + (y + z) ; :: thesis: verum

hereby :: according to RLVECT_1:def 4 :: thesis: V / W is right_complementable

let x be Vector of (V / W); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable let x be Vector of (V / W); :: thesis: x + (0. (V / W)) = x

reconsider x9 = x as Element of (V . W) ;

thus x + (0. (V / W)) = x9 + (0. (V . W))

.= x by RLVECT_1:4 ; :: thesis: verum

end;reconsider x9 = x as Element of (V . W) ;

thus x + (0. (V / W)) = x9 + (0. (V . W))

.= x by RLVECT_1:4 ; :: thesis: verum

reconsider x9 = x as Element of (V . W) ;

consider b being Element of (V . W) such that

A2: x9 + b = 0. (V . W) by ALGSTR_0:def 11;

reconsider b9 = b as Vector of (V / W) ;

take b9 ; :: according to ALGSTR_0:def 11 :: thesis: x + b9 = 0. (V / W)

thus x + b9 = 0. (V / W) by A2; :: thesis: verum