Description: The sum of two vectors belongs to their span. (Contributed by NM, 20-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lspprvacl.v | |- V = ( Base ` W ) |
|
lspprvacl.p | |- .+ = ( +g ` W ) |
||
lspprvacl.n | |- N = ( LSpan ` W ) |
||
lspprvacl.w | |- ( ph -> W e. LMod ) |
||
lspprvacl.x | |- ( ph -> X e. V ) |
||
lspprvacl.y | |- ( ph -> Y e. V ) |
||
Assertion | lspprvacl | |- ( ph -> ( X .+ Y ) e. ( N ` { X , Y } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspprvacl.v | |- V = ( Base ` W ) |
|
2 | lspprvacl.p | |- .+ = ( +g ` W ) |
|
3 | lspprvacl.n | |- N = ( LSpan ` W ) |
|
4 | lspprvacl.w | |- ( ph -> W e. LMod ) |
|
5 | lspprvacl.x | |- ( ph -> X e. V ) |
|
6 | lspprvacl.y | |- ( ph -> Y e. V ) |
|
7 | eqid | |- ( LSubSp ` W ) = ( LSubSp ` W ) |
|
8 | 1 7 3 4 5 6 | lspprcl | |- ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` W ) ) |
9 | 1 3 4 5 6 | lspprid1 | |- ( ph -> X e. ( N ` { X , Y } ) ) |
10 | 1 3 4 5 6 | lspprid2 | |- ( ph -> Y e. ( N ` { X , Y } ) ) |
11 | 2 7 | 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 } ) ) |
12 | 4 8 9 10 11 | syl22anc | |- ( ph -> ( X .+ Y ) e. ( N ` { X , Y } ) ) |