Step |
Hyp |
Ref |
Expression |
1 |
|
lspvadd.v |
|- V = ( Base ` W ) |
2 |
|
lspvadd.a |
|- .+ = ( +g ` W ) |
3 |
|
lspvadd.n |
|- N = ( LSpan ` W ) |
4 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
5 |
|
simp1 |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> W e. LMod ) |
6 |
|
prssi |
|- ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V ) |
7 |
6
|
3adant1 |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> { X , Y } C_ V ) |
8 |
1 4 3
|
lspcl |
|- ( ( W e. LMod /\ { X , Y } C_ V ) -> ( N ` { X , Y } ) e. ( LSubSp ` W ) ) |
9 |
5 7 8
|
syl2anc |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { X , Y } ) e. ( LSubSp ` W ) ) |
10 |
1 3
|
lspssid |
|- ( ( W e. LMod /\ { X , Y } C_ V ) -> { X , Y } C_ ( N ` { X , Y } ) ) |
11 |
5 7 10
|
syl2anc |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> { X , Y } C_ ( N ` { X , Y } ) ) |
12 |
|
prssg |
|- ( ( X e. V /\ Y e. V ) -> ( ( X e. ( N ` { X , Y } ) /\ Y e. ( N ` { X , Y } ) ) <-> { X , Y } C_ ( N ` { X , Y } ) ) ) |
13 |
12
|
3adant1 |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( X e. ( N ` { X , Y } ) /\ Y e. ( N ` { X , Y } ) ) <-> { X , Y } C_ ( N ` { X , Y } ) ) ) |
14 |
11 13
|
mpbird |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X e. ( N ` { X , Y } ) /\ Y e. ( N ` { X , Y } ) ) ) |
15 |
2 4
|
lssvacl |
|- ( ( ( W e. LMod /\ ( N ` { X , Y } ) e. ( LSubSp ` W ) ) /\ ( X e. ( N ` { X , Y } ) /\ Y e. ( N ` { X , Y } ) ) ) -> ( X .+ Y ) e. ( N ` { X , Y } ) ) |
16 |
5 9 14 15
|
syl21anc |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. ( N ` { X , Y } ) ) |
17 |
4 3 5 9 16
|
lspsnel5a |
|- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( N ` { ( X .+ Y ) } ) C_ ( N ` { X , Y } ) ) |