Metamath Proof Explorer


Theorem lspprabs

Description: Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015)

Ref Expression
Hypotheses lspprabs.v
|- V = ( Base ` W )
lspprabs.p
|- .+ = ( +g ` W )
lspprabs.n
|- N = ( LSpan ` W )
lspprabs.w
|- ( ph -> W e. LMod )
lspprabs.x
|- ( ph -> X e. V )
lspprabs.y
|- ( ph -> Y e. V )
Assertion lspprabs
|- ( ph -> ( N ` { X , ( X .+ Y ) } ) = ( N ` { X , Y } ) )

Proof

Step Hyp Ref Expression
1 lspprabs.v
 |-  V = ( Base ` W )
2 lspprabs.p
 |-  .+ = ( +g ` W )
3 lspprabs.n
 |-  N = ( LSpan ` W )
4 lspprabs.w
 |-  ( ph -> W e. LMod )
5 lspprabs.x
 |-  ( ph -> X e. V )
6 lspprabs.y
 |-  ( ph -> Y e. V )
7 eqid
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
8 7 lsssssubg
 |-  ( W e. LMod -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
9 4 8 syl
 |-  ( ph -> ( LSubSp ` W ) C_ ( SubGrp ` W ) )
10 1 7 3 lspsncl
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
11 4 5 10 syl2anc
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` W ) )
12 9 11 sseldd
 |-  ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
13 1 7 3 lspsncl
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
14 4 6 13 syl2anc
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
15 9 14 sseldd
 |-  ( ph -> ( N ` { Y } ) e. ( SubGrp ` W ) )
16 eqid
 |-  ( LSSum ` W ) = ( LSSum ` W )
17 16 lsmub1
 |-  ( ( ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { Y } ) e. ( SubGrp ` W ) ) -> ( N ` { X } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
18 12 15 17 syl2anc
 |-  ( ph -> ( N ` { X } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
19 7 16 lsmcl
 |-  ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) /\ ( N ` { Y } ) e. ( LSubSp ` W ) ) -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) e. ( LSubSp ` W ) )
20 4 11 14 19 syl3anc
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) e. ( LSubSp ` W ) )
21 1 3 lspsnid
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
22 4 5 21 syl2anc
 |-  ( ph -> X e. ( N ` { X } ) )
23 1 3 lspsnid
 |-  ( ( W e. LMod /\ Y e. V ) -> Y e. ( N ` { Y } ) )
24 4 6 23 syl2anc
 |-  ( ph -> Y e. ( N ` { Y } ) )
25 2 16 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 } ) ) )
26 12 15 22 24 25 syl22anc
 |-  ( ph -> ( X .+ Y ) e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
27 7 3 4 20 26 lspsnel5a
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
28 1 2 lmodvacl
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
29 4 5 6 28 syl3anc
 |-  ( ph -> ( X .+ Y ) e. V )
30 1 7 3 lspsncl
 |-  ( ( W e. LMod /\ ( X .+ Y ) e. V ) -> ( N ` { ( X .+ Y ) } ) e. ( LSubSp ` W ) )
31 4 29 30 syl2anc
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) e. ( LSubSp ` W ) )
32 9 31 sseldd
 |-  ( ph -> ( N ` { ( X .+ Y ) } ) e. ( SubGrp ` W ) )
33 9 20 sseldd
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) e. ( SubGrp ` W ) )
34 16 lsmlub
 |-  ( ( ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { ( X .+ Y ) } ) e. ( SubGrp ` W ) /\ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) e. ( SubGrp ` W ) ) -> ( ( ( N ` { X } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) /\ ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) ) <-> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) ) )
35 12 32 33 34 syl3anc
 |-  ( ph -> ( ( ( N ` { X } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) /\ ( N ` { ( X .+ Y ) } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) ) <-> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) ) )
36 18 27 35 mpbi2and
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
37 16 lsmub1
 |-  ( ( ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { ( X .+ Y ) } ) e. ( SubGrp ` W ) ) -> ( N ` { X } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) )
38 12 32 37 syl2anc
 |-  ( ph -> ( N ` { X } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) )
39 7 16 lsmcl
 |-  ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) /\ ( N ` { ( X .+ Y ) } ) e. ( LSubSp ` W ) ) -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) e. ( LSubSp ` W ) )
40 4 11 31 39 syl3anc
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) e. ( LSubSp ` W ) )
41 eqid
 |-  ( -g ` W ) = ( -g ` W )
42 1 3 lspsnid
 |-  ( ( W e. LMod /\ ( X .+ Y ) e. V ) -> ( X .+ Y ) e. ( N ` { ( X .+ Y ) } ) )
43 4 29 42 syl2anc
 |-  ( ph -> ( X .+ Y ) e. ( N ` { ( X .+ Y ) } ) )
44 41 16 32 12 43 22 lsmelvalmi
 |-  ( ph -> ( ( X .+ Y ) ( -g ` W ) X ) e. ( ( N ` { ( X .+ Y ) } ) ( LSSum ` W ) ( N ` { X } ) ) )
45 lmodabl
 |-  ( W e. LMod -> W e. Abel )
46 4 45 syl
 |-  ( ph -> W e. Abel )
47 1 2 41 ablpncan2
 |-  ( ( W e. Abel /\ X e. V /\ Y e. V ) -> ( ( X .+ Y ) ( -g ` W ) X ) = Y )
48 46 5 6 47 syl3anc
 |-  ( ph -> ( ( X .+ Y ) ( -g ` W ) X ) = Y )
49 16 lsmcom
 |-  ( ( W e. Abel /\ ( N ` { ( X .+ Y ) } ) e. ( SubGrp ` W ) /\ ( N ` { X } ) e. ( SubGrp ` W ) ) -> ( ( N ` { ( X .+ Y ) } ) ( LSSum ` W ) ( N ` { X } ) ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) )
50 46 32 12 49 syl3anc
 |-  ( ph -> ( ( N ` { ( X .+ Y ) } ) ( LSSum ` W ) ( N ` { X } ) ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) )
51 44 48 50 3eltr3d
 |-  ( ph -> Y e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) )
52 7 3 4 40 51 lspsnel5a
 |-  ( ph -> ( N ` { Y } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) )
53 9 40 sseldd
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) e. ( SubGrp ` W ) )
54 16 lsmlub
 |-  ( ( ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { Y } ) e. ( SubGrp ` W ) /\ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) e. ( SubGrp ` W ) ) -> ( ( ( N ` { X } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) /\ ( N ` { Y } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) ) <-> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) ) )
55 12 15 53 54 syl3anc
 |-  ( ph -> ( ( ( N ` { X } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) /\ ( N ` { Y } ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) ) <-> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) ) )
56 38 52 55 mpbi2and
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) C_ ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) )
57 36 56 eqssd
 |-  ( ph -> ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
58 1 3 16 4 5 29 lsmpr
 |-  ( ph -> ( N ` { X , ( X .+ Y ) } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { ( X .+ Y ) } ) ) )
59 1 3 16 4 5 6 lsmpr
 |-  ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
60 57 58 59 3eqtr4d
 |-  ( ph -> ( N ` { X , ( X .+ Y ) } ) = ( N ` { X , Y } ) )