Metamath Proof Explorer

Theorem lspabs3

Description: Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015)

Ref Expression
Hypotheses lspabs2.v 
|- V = ( Base ` W )
lspabs2.p 
|- .+ = ( +g ` W )
lspabs2.o 
|- .0. = ( 0g ` W )
lspabs2.n 
|- N = ( LSpan ` W )
lspabs2.w 
|- ( ph -> W e. LVec )
lspabs2.x 
|- ( ph -> X e. V )
lspabs3.y 
|- ( ph -> Y e. V )
lspabs3.xy 
|- ( ph -> ( X .+ Y ) =/= .0. )
lspabs3.e 
|- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
Assertion lspabs3 
|- ( ph -> ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) )

Proof

Step Hyp Ref Expression
1 lspabs2.v 
 |-  V = ( Base ` W )
2 lspabs2.p 
 |-  .+ = ( +g ` W )
3 lspabs2.o 
 |-  .0. = ( 0g ` W )
4 lspabs2.n 
 |-  N = ( LSpan ` W )
5 lspabs2.w 
 |-  ( ph -> W e. LVec )
6 lspabs2.x 
 |-  ( ph -> X e. V )
7 lspabs3.y 
 |-  ( ph -> Y e. V )
8 lspabs3.xy 
 |-  ( ph -> ( X .+ Y ) =/= .0. )
9 lspabs3.e 
 |-  ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
10 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
11 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
12 5 11 syl 
 |-  ( ph -> W e. LMod )
13 1 10 4 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
14 12 6 13 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` W ) )
15 1 10 4 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
16 12 7 15 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
17 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
18 10 17 lsmcl 
 |-  ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) /\ ( N ` { Y } ) e. ( LSubSp ` W ) ) -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) e. ( LSubSp ` W ) )
19 12 14 16 18 syl3anc 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) e. ( LSubSp ` W ) )
20 1 4 lspsnsubg 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
21 12 6 20 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
22 9 21 eqeltrrd 
 |-  ( ph -> ( N ` { Y } ) e. ( SubGrp ` W ) )
23 1 4 lspsnid 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
24 12 6 23 syl2anc 
 |-  ( ph -> X e. ( N ` { X } ) )
25 1 4 lspsnid 
 |-  ( ( W e. LMod /\ Y e. V ) -> Y e. ( N ` { Y } ) )
26 12 7 25 syl2anc 
 |-  ( ph -> Y e. ( N ` { Y } ) )
27 2 17 lsmelvali 
 |-  ( ( ( ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { Y } ) e. ( SubGrp ` W ) ) /\ ( X e. ( N ` { X } ) /\ Y e. ( N ` { Y } ) ) ) -> ( X .+ Y ) e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
28 21 22 24 26 27 syl22anc 
 |-  ( ph -> ( X .+ Y ) e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
29 10 4 12 19 28 lspsnel5a 
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
30 9 oveq2d 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { X } ) ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
31 17 lsmidm 
 |-  ( ( N ` { X } ) e. ( SubGrp ` W ) -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { X } ) ) = ( N ` { X } ) )
32 21 31 syl 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { X } ) ) = ( N ` { X } ) )
33 30 32 eqtr3d 
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) = ( N ` { X } ) )
34 29 33 sseqtrd 
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) C_ ( N ` { X } ) )
35 1 2 lmodvacl 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
36 12 6 7 35 syl3anc 
 |-  ( ph -> ( X .+ Y ) e. V )
37 eldifsn 
 |-  ( ( X .+ Y ) e. ( V \ { .0. } ) <-> ( ( X .+ Y ) e. V /\ ( X .+ Y ) =/= .0. ) )
38 36 8 37 sylanbrc 
 |-  ( ph -> ( X .+ Y ) e. ( V \ { .0. } ) )
39 1 3 4 5 38 6 lspsncmp 
 |-  ( ph -> ( ( N ` { ( X .+ Y ) } ) C_ ( N ` { X } ) <-> ( N ` { ( X .+ Y ) } ) = ( N ` { X } ) ) )
40 34 39 mpbid 
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) = ( N ` { X } ) )
41 40 eqcomd 
 |-  ( ph -> ( N ` { X } ) = ( N ` { ( X .+ Y ) } ) )