Metamath Proof Explorer

Theorem lsmsat

Description: Convert comparison of atom with sum of subspaces to a comparison to sum with atom. ( elpaddatiN analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses lsmsat.o 
|- .0. = ( 0g ` W )
lsmsat.s 
|- S = ( LSubSp ` W )
lsmsat.p 
|- .(+) = ( LSSum ` W )
lsmsat.a 
|- A = ( LSAtoms ` W )
lsmsat.w 
|- ( ph -> W e. LMod )
lsmsat.t 
|- ( ph -> T e. S )
lsmsat.u 
|- ( ph -> U e. S )
lsmsat.q 
|- ( ph -> Q e. A )
lsmsat.n 
|- ( ph -> T =/= { .0. } )
lsmsat.l 
|- ( ph -> Q C_ ( T .(+) U ) )
Assertion lsmsat 
|- ( ph -> E. p e. A ( p C_ T /\ Q C_ ( p .(+) U ) ) )

Proof

Step Hyp Ref Expression
1 lsmsat.o 
 |-  .0. = ( 0g ` W )
2 lsmsat.s 
 |-  S = ( LSubSp ` W )
3 lsmsat.p 
 |-  .(+) = ( LSSum ` W )
4 lsmsat.a 
 |-  A = ( LSAtoms ` W )
5 lsmsat.w 
 |-  ( ph -> W e. LMod )
6 lsmsat.t 
 |-  ( ph -> T e. S )
7 lsmsat.u 
 |-  ( ph -> U e. S )
8 lsmsat.q 
 |-  ( ph -> Q e. A )
9 lsmsat.n 
 |-  ( ph -> T =/= { .0. } )
10 lsmsat.l 
 |-  ( ph -> Q C_ ( T .(+) U ) )
11 eqid 
 |-  ( Base ` W ) = ( Base ` W )
12 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
13 11 12 1 4 islsat 
 |-  ( W e. LMod -> ( Q e. A <-> E. r e. ( ( Base ` W ) \ { .0. } ) Q = ( ( LSpan ` W ) ` { r } ) ) )
14 5 13 syl 
 |-  ( ph -> ( Q e. A <-> E. r e. ( ( Base ` W ) \ { .0. } ) Q = ( ( LSpan ` W ) ` { r } ) ) )
15 8 14 mpbid 
 |-  ( ph -> E. r e. ( ( Base ` W ) \ { .0. } ) Q = ( ( LSpan ` W ) ` { r } ) )
16 simp3 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> Q = ( ( LSpan ` W ) ` { r } ) )
17 10 3ad2ant1 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> Q C_ ( T .(+) U ) )
18 16 17 eqsstrrd 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> ( ( LSpan ` W ) ` { r } ) C_ ( T .(+) U ) )
19 5 3ad2ant1 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> W e. LMod )
20 2 3 lsmcl 
 |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T .(+) U ) e. S )
21 5 6 7 20 syl3anc 
 |-  ( ph -> ( T .(+) U ) e. S )
22 21 3ad2ant1 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> ( T .(+) U ) e. S )
23 eldifi 
 |-  ( r e. ( ( Base ` W ) \ { .0. } ) -> r e. ( Base ` W ) )
24 23 3ad2ant2 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> r e. ( Base ` W ) )
25 11 2 12 19 22 24 lspsnel5 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> ( r e. ( T .(+) U ) <-> ( ( LSpan ` W ) ` { r } ) C_ ( T .(+) U ) ) )
26 18 25 mpbird 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> r e. ( T .(+) U ) )
27 2 lsssssubg 
 |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
28 19 27 syl 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> S C_ ( SubGrp ` W ) )
29 6 3ad2ant1 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> T e. S )
30 28 29 sseldd 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> T e. ( SubGrp ` W ) )
31 7 3ad2ant1 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> U e. S )
32 28 31 sseldd 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> U e. ( SubGrp ` W ) )
33 eqid 
 |-  ( +g ` W ) = ( +g ` W )
34 33 3 lsmelval 
 |-  ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( r e. ( T .(+) U ) <-> E. y e. T E. z e. U r = ( y ( +g ` W ) z ) ) )
35 30 32 34 syl2anc 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> ( r e. ( T .(+) U ) <-> E. y e. T E. z e. U r = ( y ( +g ` W ) z ) ) )
36 26 35 mpbid 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> E. y e. T E. z e. U r = ( y ( +g ` W ) z ) )
37 1 2 lssne0 
 |-  ( T e. S -> ( T =/= { .0. } <-> E. q e. T q =/= .0. ) )
38 6 37 syl 
 |-  ( ph -> ( T =/= { .0. } <-> E. q e. T q =/= .0. ) )
39 9 38 mpbid 
 |-  ( ph -> E. q e. T q =/= .0. )
40 39 adantr 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) -> E. q e. T q =/= .0. )
41 40 3ad2ant1 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> E. q e. T q =/= .0. )
42 41 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y = .0. ) -> E. q e. T q =/= .0. )
43 5 adantr 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) -> W e. LMod )
44 43 3ad2ant1 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> W e. LMod )
45 44 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> W e. LMod )
46 6 adantr 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) -> T e. S )
47 46 3ad2ant1 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> T e. S )
48 47 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> T e. S )
49 simpr2 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> q e. T )
50 11 2 lssel 
 |-  ( ( T e. S /\ q e. T ) -> q e. ( Base ` W ) )
51 48 49 50 syl2anc 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> q e. ( Base ` W ) )
52 simpr3 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> q =/= .0. )
53 11 12 1 4 lsatlspsn2 
 |-  ( ( W e. LMod /\ q e. ( Base ` W ) /\ q =/= .0. ) -> ( ( LSpan ` W ) ` { q } ) e. A )
54 45 51 52 53 syl3anc 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( ( LSpan ` W ) ` { q } ) e. A )
55 2 12 45 48 49 lspsnel5a 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( ( LSpan ` W ) ` { q } ) C_ T )
56 simpl3 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> r = ( y ( +g ` W ) z ) )
57 simpr1 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> y = .0. )
58 57 oveq1d 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( y ( +g ` W ) z ) = ( .0. ( +g ` W ) z ) )
59 7 adantr 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) -> U e. S )
60 59 3ad2ant1 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> U e. S )
61 simp2r 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> z e. U )
62 11 2 lssel 
 |-  ( ( U e. S /\ z e. U ) -> z e. ( Base ` W ) )
63 60 61 62 syl2anc 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> z e. ( Base ` W ) )
64 63 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> z e. ( Base ` W ) )
65 11 33 1 lmod0vlid 
 |-  ( ( W e. LMod /\ z e. ( Base ` W ) ) -> ( .0. ( +g ` W ) z ) = z )
66 45 64 65 syl2anc 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( .0. ( +g ` W ) z ) = z )
67 56 58 66 3eqtrd 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> r = z )
68 67 sneqd 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> { r } = { z } )
69 68 fveq2d 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( ( LSpan ` W ) ` { r } ) = ( ( LSpan ` W ) ` { z } ) )
70 2 12 44 60 61 lspsnel5a 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { z } ) C_ U )
71 70 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( ( LSpan ` W ) ` { z } ) C_ U )
72 69 71 eqsstrd 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( ( LSpan ` W ) ` { r } ) C_ U )
73 11 12 lspsnsubg 
 |-  ( ( W e. LMod /\ q e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` { q } ) e. ( SubGrp ` W ) )
74 45 51 73 syl2anc 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( ( LSpan ` W ) ` { q } ) e. ( SubGrp ` W ) )
75 45 27 syl 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> S C_ ( SubGrp ` W ) )
76 60 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> U e. S )
77 75 76 sseldd 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> U e. ( SubGrp ` W ) )
78 3 lsmub2 
 |-  ( ( ( ( LSpan ` W ) ` { q } ) e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> U C_ ( ( ( LSpan ` W ) ` { q } ) .(+) U ) )
79 74 77 78 syl2anc 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> U C_ ( ( ( LSpan ` W ) ` { q } ) .(+) U ) )
80 72 79 sstrd 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { q } ) .(+) U ) )
81 sseq1 
 |-  ( p = ( ( LSpan ` W ) ` { q } ) -> ( p C_ T <-> ( ( LSpan ` W ) ` { q } ) C_ T ) )
82 oveq1 
 |-  ( p = ( ( LSpan ` W ) ` { q } ) -> ( p .(+) U ) = ( ( ( LSpan ` W ) ` { q } ) .(+) U ) )
83 82 sseq2d 
 |-  ( p = ( ( LSpan ` W ) ` { q } ) -> ( ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) <-> ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { q } ) .(+) U ) ) )
84 81 83 anbi12d 
 |-  ( p = ( ( LSpan ` W ) ` { q } ) -> ( ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) <-> ( ( ( LSpan ` W ) ` { q } ) C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { q } ) .(+) U ) ) ) )
85 84 rspcev 
 |-  ( ( ( ( LSpan ` W ) ` { q } ) e. A /\ ( ( ( LSpan ` W ) ` { q } ) C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { q } ) .(+) U ) ) ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) )
86 54 55 80 85 syl12anc 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ ( y = .0. /\ q e. T /\ q =/= .0. ) ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) )
87 86 3exp2 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( y = .0. -> ( q e. T -> ( q =/= .0. -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) ) ) )
88 87 imp 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y = .0. ) -> ( q e. T -> ( q =/= .0. -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) ) )
89 88 rexlimdv 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y = .0. ) -> ( E. q e. T q =/= .0. -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) )
90 42 89 mpd 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y = .0. ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) )
91 44 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y =/= .0. ) -> W e. LMod )
92 simp2l 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> y e. T )
93 11 2 lssel 
 |-  ( ( T e. S /\ y e. T ) -> y e. ( Base ` W ) )
94 47 92 93 syl2anc 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> y e. ( Base ` W ) )
95 94 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y =/= .0. ) -> y e. ( Base ` W ) )
96 simpr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y =/= .0. ) -> y =/= .0. )
97 11 12 1 4 lsatlspsn2 
 |-  ( ( W e. LMod /\ y e. ( Base ` W ) /\ y =/= .0. ) -> ( ( LSpan ` W ) ` { y } ) e. A )
98 91 95 96 97 syl3anc 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y =/= .0. ) -> ( ( LSpan ` W ) ` { y } ) e. A )
99 2 12 44 47 92 lspsnel5a 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { y } ) C_ T )
100 99 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y =/= .0. ) -> ( ( LSpan ` W ) ` { y } ) C_ T )
101 simp3 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> r = ( y ( +g ` W ) z ) )
102 101 sneqd 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> { r } = { ( y ( +g ` W ) z ) } )
103 102 fveq2d 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { r } ) = ( ( LSpan ` W ) ` { ( y ( +g ` W ) z ) } ) )
104 11 33 12 lspvadd 
 |-  ( ( W e. LMod /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` { ( y ( +g ` W ) z ) } ) C_ ( ( LSpan ` W ) ` { y , z } ) )
105 44 94 63 104 syl3anc 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { ( y ( +g ` W ) z ) } ) C_ ( ( LSpan ` W ) ` { y , z } ) )
106 103 105 eqsstrd 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { r } ) C_ ( ( LSpan ` W ) ` { y , z } ) )
107 11 12 3 44 94 63 lsmpr 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { y , z } ) = ( ( ( LSpan ` W ) ` { y } ) .(+) ( ( LSpan ` W ) ` { z } ) ) )
108 106 107 sseqtrd 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { y } ) .(+) ( ( LSpan ` W ) ` { z } ) ) )
109 44 27 syl 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> S C_ ( SubGrp ` W ) )
110 11 2 12 lspsncl 
 |-  ( ( W e. LMod /\ y e. ( Base ` W ) ) -> ( ( LSpan ` W ) ` { y } ) e. S )
111 44 94 110 syl2anc 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { y } ) e. S )
112 109 111 sseldd 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { y } ) e. ( SubGrp ` W ) )
113 109 60 sseldd 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> U e. ( SubGrp ` W ) )
114 3 lsmless2 
 |-  ( ( ( ( LSpan ` W ) ` { y } ) e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) /\ ( ( LSpan ` W ) ` { z } ) C_ U ) -> ( ( ( LSpan ` W ) ` { y } ) .(+) ( ( LSpan ` W ) ` { z } ) ) C_ ( ( ( LSpan ` W ) ` { y } ) .(+) U ) )
115 112 113 70 114 syl3anc 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( ( LSpan ` W ) ` { y } ) .(+) ( ( LSpan ` W ) ` { z } ) ) C_ ( ( ( LSpan ` W ) ` { y } ) .(+) U ) )
116 108 115 sstrd 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { y } ) .(+) U ) )
117 116 adantr 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y =/= .0. ) -> ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { y } ) .(+) U ) )
118 sseq1 
 |-  ( p = ( ( LSpan ` W ) ` { y } ) -> ( p C_ T <-> ( ( LSpan ` W ) ` { y } ) C_ T ) )
119 oveq1 
 |-  ( p = ( ( LSpan ` W ) ` { y } ) -> ( p .(+) U ) = ( ( ( LSpan ` W ) ` { y } ) .(+) U ) )
120 119 sseq2d 
 |-  ( p = ( ( LSpan ` W ) ` { y } ) -> ( ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) <-> ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { y } ) .(+) U ) ) )
121 118 120 anbi12d 
 |-  ( p = ( ( LSpan ` W ) ` { y } ) -> ( ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) <-> ( ( ( LSpan ` W ) ` { y } ) C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { y } ) .(+) U ) ) ) )
122 121 rspcev 
 |-  ( ( ( ( LSpan ` W ) ` { y } ) e. A /\ ( ( ( LSpan ` W ) ` { y } ) C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( ( ( LSpan ` W ) ` { y } ) .(+) U ) ) ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) )
123 98 100 117 122 syl12anc 
 |-  ( ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) /\ y =/= .0. ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) )
124 90 123 pm2.61dane 
 |-  ( ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) /\ ( y e. T /\ z e. U ) /\ r = ( y ( +g ` W ) z ) ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) )
125 124 3exp 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) -> ( ( y e. T /\ z e. U ) -> ( r = ( y ( +g ` W ) z ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) ) )
126 125 rexlimdvv 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) ) -> ( E. y e. T E. z e. U r = ( y ( +g ` W ) z ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) )
127 126 3adant3 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> ( E. y e. T E. z e. U r = ( y ( +g ` W ) z ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) )
128 36 127 mpd 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) )
129 sseq1 
 |-  ( Q = ( ( LSpan ` W ) ` { r } ) -> ( Q C_ ( p .(+) U ) <-> ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) )
130 129 anbi2d 
 |-  ( Q = ( ( LSpan ` W ) ` { r } ) -> ( ( p C_ T /\ Q C_ ( p .(+) U ) ) <-> ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) )
131 130 rexbidv 
 |-  ( Q = ( ( LSpan ` W ) ` { r } ) -> ( E. p e. A ( p C_ T /\ Q C_ ( p .(+) U ) ) <-> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) )
132 131 3ad2ant3 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> ( E. p e. A ( p C_ T /\ Q C_ ( p .(+) U ) ) <-> E. p e. A ( p C_ T /\ ( ( LSpan ` W ) ` { r } ) C_ ( p .(+) U ) ) ) )
133 128 132 mpbird 
 |-  ( ( ph /\ r e. ( ( Base ` W ) \ { .0. } ) /\ Q = ( ( LSpan ` W ) ` { r } ) ) -> E. p e. A ( p C_ T /\ Q C_ ( p .(+) U ) ) )
134 133 3exp 
 |-  ( ph -> ( r e. ( ( Base ` W ) \ { .0. } ) -> ( Q = ( ( LSpan ` W ) ` { r } ) -> E. p e. A ( p C_ T /\ Q C_ ( p .(+) U ) ) ) ) )
135 134 rexlimdv 
 |-  ( ph -> ( E. r e. ( ( Base ` W ) \ { .0. } ) Q = ( ( LSpan ` W ) ` { r } ) -> E. p e. A ( p C_ T /\ Q C_ ( p .(+) U ) ) ) )
136 15 135 mpd 
 |-  ( ph -> E. p e. A ( p C_ T /\ Q C_ ( p .(+) U ) ) )