Step |
Hyp |
Ref |
Expression |
1 |
|
lspss.v |
|- V = ( Base ` W ) |
2 |
|
lspss.n |
|- N = ( LSpan ` W ) |
3 |
|
simpl3 |
|- ( ( ( W e. LMod /\ U C_ V /\ T C_ U ) /\ t e. ( LSubSp ` W ) ) -> T C_ U ) |
4 |
|
sstr2 |
|- ( T C_ U -> ( U C_ t -> T C_ t ) ) |
5 |
3 4
|
syl |
|- ( ( ( W e. LMod /\ U C_ V /\ T C_ U ) /\ t e. ( LSubSp ` W ) ) -> ( U C_ t -> T C_ t ) ) |
6 |
5
|
ss2rabdv |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> { t e. ( LSubSp ` W ) | U C_ t } C_ { t e. ( LSubSp ` W ) | T C_ t } ) |
7 |
|
intss |
|- ( { t e. ( LSubSp ` W ) | U C_ t } C_ { t e. ( LSubSp ` W ) | T C_ t } -> |^| { t e. ( LSubSp ` W ) | T C_ t } C_ |^| { t e. ( LSubSp ` W ) | U C_ t } ) |
8 |
6 7
|
syl |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> |^| { t e. ( LSubSp ` W ) | T C_ t } C_ |^| { t e. ( LSubSp ` W ) | U C_ t } ) |
9 |
|
simp1 |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> W e. LMod ) |
10 |
|
simp3 |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> T C_ U ) |
11 |
|
simp2 |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> U C_ V ) |
12 |
10 11
|
sstrd |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> T C_ V ) |
13 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
14 |
1 13 2
|
lspval |
|- ( ( W e. LMod /\ T C_ V ) -> ( N ` T ) = |^| { t e. ( LSubSp ` W ) | T C_ t } ) |
15 |
9 12 14
|
syl2anc |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> ( N ` T ) = |^| { t e. ( LSubSp ` W ) | T C_ t } ) |
16 |
1 13 2
|
lspval |
|- ( ( W e. LMod /\ U C_ V ) -> ( N ` U ) = |^| { t e. ( LSubSp ` W ) | U C_ t } ) |
17 |
16
|
3adant3 |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> ( N ` U ) = |^| { t e. ( LSubSp ` W ) | U C_ t } ) |
18 |
8 15 17
|
3sstr4d |
|- ( ( W e. LMod /\ U C_ V /\ T C_ U ) -> ( N ` T ) C_ ( N ` U ) ) |