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

for W being Subspace of V holds V / W is strict LeftMod of K

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

let W be Subspace of V; :: thesis: V / W is strict LeftMod of K

for W being Subspace of V holds V / W is strict LeftMod of K

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

let W be Subspace of V; :: thesis: V / W is strict LeftMod of K

now :: thesis: for x, y being Scalar of K

for v, w being Vector of (V / W) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )

hence
V / W is strict LeftMod of K
by Lm2, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17; :: thesis: verumfor v, w being Vector of (V / W) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )

let x, y be Scalar of K; :: thesis: for v, w being Vector of (V / W) holds

( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )

let v, w be Vector of (V / W); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )

consider a being Vector of V such that

A1: v = a / W by Th20;

consider b being Vector of V such that

A2: w = b / W by Th20;

A3: (x * a) / W = x * v by A1, Th22;

A4: (x * b) / W = x * w by A2, Th22;

A5: (y * a) / W = y * v by A1, Th22;

thus x * (v + w) = x * ((a + b) / W) by A1, A2, Th22

.= (x * (a + b)) / W by Th22

.= ((x * a) + (x * b)) / W by VECTSP_1:def 14

.= (x * v) + (x * w) by A3, A4, Th22 ; :: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )

thus (x + y) * v = ((x + y) * a) / W by A1, Th22

.= ((x * a) + (y * a)) / W by VECTSP_1:def 15

.= (x * v) + (y * v) by A3, A5, Th22 ; :: thesis: ( (x * y) * v = x * (y * v) & (1_ K) * v = v )

thus (x * y) * v = ((x * y) * a) / W by A1, Th22

.= (x * (y * a)) / W by VECTSP_1:def 16

.= x * ((y * a) / W) by Th22

.= x * (y * v) by A1, Th22 ; :: thesis: (1_ K) * v = v

thus (1_ K) * v = ((1_ K) * a) / W by A1, Th22

.= v by A1, VECTSP_1:def 17 ; :: thesis: verum

end;( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )

let v, w be Vector of (V / W); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )

consider a being Vector of V such that

A1: v = a / W by Th20;

consider b being Vector of V such that

A2: w = b / W by Th20;

A3: (x * a) / W = x * v by A1, Th22;

A4: (x * b) / W = x * w by A2, Th22;

A5: (y * a) / W = y * v by A1, Th22;

thus x * (v + w) = x * ((a + b) / W) by A1, A2, Th22

.= (x * (a + b)) / W by Th22

.= ((x * a) + (x * b)) / W by VECTSP_1:def 14

.= (x * v) + (x * w) by A3, A4, Th22 ; :: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1_ K) * v = v )

thus (x + y) * v = ((x + y) * a) / W by A1, Th22

.= ((x * a) + (y * a)) / W by VECTSP_1:def 15

.= (x * v) + (y * v) by A3, A5, Th22 ; :: thesis: ( (x * y) * v = x * (y * v) & (1_ K) * v = v )

thus (x * y) * v = ((x * y) * a) / W by A1, Th22

.= (x * (y * a)) / W by VECTSP_1:def 16

.= x * ((y * a) / W) by Th22

.= x * (y * v) by A1, Th22 ; :: thesis: (1_ K) * v = v

thus (1_ K) * v = ((1_ K) * a) / W by A1, Th22

.= v by A1, VECTSP_1:def 17 ; :: thesis: verum