let K be Field; :: thesis: for V being VectSp of K
for W1, W2, W12 being Subspace of V
for U1, U2 being Subspace of W12 st U1 = W1 & U2 = W2 holds
( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
let V be VectSp of K; :: thesis: for W1, W2, W12 being Subspace of V
for U1, U2 being Subspace of W12 st U1 = W1 & U2 = W2 holds
( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
let W1, W2, W12 be Subspace of V; :: thesis: for U1, U2 being Subspace of W12 st U1 = W1 & U2 = W2 holds
( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
let U1, U2 be Subspace of W12; :: thesis: ( U1 = W1 & U2 = W2 implies ( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 ) )
assume that
A1: U1 = W1 and
A2: U2 = W2 ; :: thesis: ( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )
reconsider U12 = U1 /\ U2 as Subspace of V by VECTSP_4:26;
A3: the carrier of U12 c= the carrier of (W1 /\ W2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of U12 or x in the carrier of (W1 /\ W2) )
assume x in the carrier of U12 ; :: thesis: x in the carrier of (W1 /\ W2)
then x in U1 /\ U2 ;
then ( x in U1 & x in U2 ) by VECTSP_5:3;
then x in W1 /\ W2 by A1, A2, VECTSP_5:3;
hence x in the carrier of (W1 /\ W2) ; :: thesis: verum
end;
the carrier of (W1 /\ W2) c= the carrier of U12
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 /\ W2) or x in the carrier of U12 )
assume x in the carrier of (W1 /\ W2) ; :: thesis: x in the carrier of U12
then x in W1 /\ W2 ;
then ( x in W1 & x in W2 ) by VECTSP_5:3;
then x in U12 by A1, A2, VECTSP_5:3;
hence x in the carrier of U12 ; :: thesis: verum
end;
then the carrier of (W1 /\ W2) = the carrier of U12 by A3, XBOOLE_0:def 10;
hence W1 /\ W2 = U1 /\ U2 by VECTSP_4:29; :: thesis: W1 + W2 = U1 + U2
reconsider U12 = U1 + U2 as Subspace of V by VECTSP_4:26;
A4: the carrier of (W1 + W2) c= the carrier of U12
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of U12 )
assume x in the carrier of (W1 + W2) ; :: thesis: x in the carrier of U12
then x in W1 + W2 ;
then consider v1, v2 being Vector of V such that
A5: v1 in W1 and
A6: v2 in W2 and
A7: v1 + v2 = x by VECTSP_5:1;
U2 is Subspace of U12 by VECTSP_5:7;
then A8: v2 in U12 by A2, A6, VECTSP_4:8;
U1 is Subspace of U12 by VECTSP_5:7;
then v1 in U12 by A1, A5, VECTSP_4:8;
then reconsider w1 = v1, w2 = v2 as Vector of U12 by A8;
v1 + v2 = w1 + w2 by VECTSP_4:13;
hence x in the carrier of U12 by A7; :: thesis: verum
end;
the carrier of U12 c= the carrier of (W1 + W2)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of U12 or x in the carrier of (W1 + W2) )
assume x in the carrier of U12 ; :: thesis: x in the carrier of (W1 + W2)
then x in U1 + U2 ;
then consider v1, v2 being Vector of W12 such that
A9: ( v1 in U1 & v2 in U2 & v1 + v2 = x ) by VECTSP_5:1;
reconsider w1 = v1, w2 = v2 as Vector of V by VECTSP_4:10;
v1 + v2 = w1 + w2 by VECTSP_4:13;
then x in W1 + W2 by A1, A2, A9, VECTSP_5:1;
hence x in the carrier of (W1 + W2) ; :: thesis: verum
end;
then the carrier of (W1 + W2) = the carrier of U12 by A4, XBOOLE_0:def 10;
hence W1 + W2 = U1 + U2 by VECTSP_4:29; :: thesis: verum