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 } ) )