let F be Field; :: thesis: for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F holds VecSp (E,F) is Subspace of VecSp (K,F)
let E be FieldExtension of F; :: thesis: for K being E -extending FieldExtension of F holds VecSp (E,F) is Subspace of VecSp (K,F)
let K be E -extending FieldExtension of F; :: thesis: VecSp (E,F) is Subspace of VecSp (K,F)
set VK = VecSp (K,F);
set VE = VecSp (E,F);
H1: E is Subring of K by FIELD_4:def 1;
then H2: the carrier of E c= the carrier of K by C0SP1:def 3;
H3: ( the carrier of (VecSp (E,F)) = the carrier of E & the carrier of (VecSp (K,F)) = the carrier of K ) by FIELD_4:def 6;
F is Subring of E by FIELD_4:def 1;
then H4: the carrier of F c= the carrier of E by C0SP1:def 3;
B1: the carrier of (VecSp (E,F)) c= the carrier of (VecSp (K,F)) by H1, H3, C0SP1:def 3;
B2: 0. (VecSp (E,F)) = 0. E by FIELD_4:def 6
.= 0. K by H1, C0SP1:def 3
.= 0. (VecSp (K,F)) by FIELD_4:def 6 ;
B3: the addF of (VecSp (E,F)) = the addF of E by FIELD_4:def 6
.= the addF of K || the carrier of E by H1, C0SP1:def 3
.= the addF of (VecSp (K,F)) || the carrier of E by FIELD_4:def 6
.= the addF of (VecSp (K,F)) || the carrier of (VecSp (E,F)) by FIELD_4:def 6 ;
B4: the lmult of (VecSp (E,F)) = the multF of E | [: the carrier of F, the carrier of (VecSp (E,F)):] by H3, FIELD_4:def 6
.= ( the multF of K || the carrier of E) | [: the carrier of F, the carrier of (VecSp (E,F)):] by H1, C0SP1:def 3
.= the multF of K | [: the carrier of F, the carrier of (VecSp (E,F)):] by H4, H3, ZFMISC_1:96, RELAT_1:74
.= ( the multF of K | [: the carrier of F, the carrier of K:]) | [: the carrier of F, the carrier of (VecSp (E,F)):] by H2, H3, ZFMISC_1:96, RELAT_1:74
.= the lmult of (VecSp (K,F)) | [: the carrier of F, the carrier of (VecSp (E,F)):] by FIELD_4:def 6 ;
thus VecSp (E,F) is Subspace of VecSp (K,F) by B1, B2, B3, B4, VECTSP_4:def 2; :: thesis: verum