Metamath Proof Explorer


Theorem lsmelval2

Description: Subspace sum membership in terms of a sum of 1-dim subspaces (atoms), which can be useful for treating subspaces as projective lattice elements. (Contributed by NM, 9-Aug-2014)

Ref Expression
Hypotheses lsmelval2.v
|- V = ( Base ` W )
lsmelval2.s
|- S = ( LSubSp ` W )
lsmelval2.p
|- .(+) = ( LSSum ` W )
lsmelval2.n
|- N = ( LSpan ` W )
lsmelval2.w
|- ( ph -> W e. LMod )
lsmelval2.t
|- ( ph -> T e. S )
lsmelval2.u
|- ( ph -> U e. S )
Assertion lsmelval2
|- ( ph -> ( X e. ( T .(+) U ) <-> ( X e. V /\ E. y e. T E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmelval2.v
 |-  V = ( Base ` W )
2 lsmelval2.s
 |-  S = ( LSubSp ` W )
3 lsmelval2.p
 |-  .(+) = ( LSSum ` W )
4 lsmelval2.n
 |-  N = ( LSpan ` W )
5 lsmelval2.w
 |-  ( ph -> W e. LMod )
6 lsmelval2.t
 |-  ( ph -> T e. S )
7 lsmelval2.u
 |-  ( ph -> U e. S )
8 2 lsssubg
 |-  ( ( W e. LMod /\ T e. S ) -> T e. ( SubGrp ` W ) )
9 5 6 8 syl2anc
 |-  ( ph -> T e. ( SubGrp ` W ) )
10 2 lsssubg
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
11 5 7 10 syl2anc
 |-  ( ph -> U e. ( SubGrp ` W ) )
12 eqid
 |-  ( +g ` W ) = ( +g ` W )
13 12 3 lsmelval
 |-  ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y ( +g ` W ) z ) ) )
14 9 11 13 syl2anc
 |-  ( ph -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U X = ( y ( +g ` W ) z ) ) )
15 5 adantr
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> W e. LMod )
16 6 adantr
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> T e. S )
17 simprl
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> y e. T )
18 1 2 lssel
 |-  ( ( T e. S /\ y e. T ) -> y e. V )
19 16 17 18 syl2anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> y e. V )
20 1 2 4 lspsncl
 |-  ( ( W e. LMod /\ y e. V ) -> ( N ` { y } ) e. S )
21 15 19 20 syl2anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { y } ) e. S )
22 2 lsssubg
 |-  ( ( W e. LMod /\ ( N ` { y } ) e. S ) -> ( N ` { y } ) e. ( SubGrp ` W ) )
23 15 21 22 syl2anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { y } ) e. ( SubGrp ` W ) )
24 7 adantr
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> U e. S )
25 simprr
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> z e. U )
26 1 2 lssel
 |-  ( ( U e. S /\ z e. U ) -> z e. V )
27 24 25 26 syl2anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> z e. V )
28 1 2 4 lspsncl
 |-  ( ( W e. LMod /\ z e. V ) -> ( N ` { z } ) e. S )
29 15 27 28 syl2anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { z } ) e. S )
30 2 lsssubg
 |-  ( ( W e. LMod /\ ( N ` { z } ) e. S ) -> ( N ` { z } ) e. ( SubGrp ` W ) )
31 15 29 30 syl2anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { z } ) e. ( SubGrp ` W ) )
32 1 4 lspsnid
 |-  ( ( W e. LMod /\ y e. V ) -> y e. ( N ` { y } ) )
33 15 19 32 syl2anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> y e. ( N ` { y } ) )
34 1 4 lspsnid
 |-  ( ( W e. LMod /\ z e. V ) -> z e. ( N ` { z } ) )
35 15 27 34 syl2anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> z e. ( N ` { z } ) )
36 12 3 lsmelvali
 |-  ( ( ( ( N ` { y } ) e. ( SubGrp ` W ) /\ ( N ` { z } ) e. ( SubGrp ` W ) ) /\ ( y e. ( N ` { y } ) /\ z e. ( N ` { z } ) ) ) -> ( y ( +g ` W ) z ) e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) )
37 23 31 33 35 36 syl22anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( y ( +g ` W ) z ) e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) )
38 eleq1a
 |-  ( ( y ( +g ` W ) z ) e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) -> ( X = ( y ( +g ` W ) z ) -> X e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) )
39 37 38 syl
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( X = ( y ( +g ` W ) z ) -> X e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) )
40 2 3 lsmcl
 |-  ( ( W e. LMod /\ ( N ` { y } ) e. S /\ ( N ` { z } ) e. S ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) e. S )
41 15 21 29 40 syl3anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) e. S )
42 1 2 4 15 41 lspsnel6
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( X e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) <-> ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )
43 39 42 sylibd
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( X = ( y ( +g ` W ) z ) -> ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )
44 43 reximdvva
 |-  ( ph -> ( E. y e. T E. z e. U X = ( y ( +g ` W ) z ) -> E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )
45 14 44 sylbid
 |-  ( ph -> ( X e. ( T .(+) U ) -> E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )
46 9 adantr
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> T e. ( SubGrp ` W ) )
47 2 4 15 16 17 lspsnel5a
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { y } ) C_ T )
48 3 lsmless1
 |-  ( ( T e. ( SubGrp ` W ) /\ ( N ` { z } ) e. ( SubGrp ` W ) /\ ( N ` { y } ) C_ T ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) C_ ( T .(+) ( N ` { z } ) ) )
49 46 31 47 48 syl3anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) C_ ( T .(+) ( N ` { z } ) ) )
50 11 adantr
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> U e. ( SubGrp ` W ) )
51 2 4 15 24 25 lspsnel5a
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( N ` { z } ) C_ U )
52 3 lsmless2
 |-  ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) /\ ( N ` { z } ) C_ U ) -> ( T .(+) ( N ` { z } ) ) C_ ( T .(+) U ) )
53 46 50 51 52 syl3anc
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( T .(+) ( N ` { z } ) ) C_ ( T .(+) U ) )
54 49 53 sstrd
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( ( N ` { y } ) .(+) ( N ` { z } ) ) C_ ( T .(+) U ) )
55 54 sseld
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( X e. ( ( N ` { y } ) .(+) ( N ` { z } ) ) -> X e. ( T .(+) U ) ) )
56 42 55 sylbird
 |-  ( ( ph /\ ( y e. T /\ z e. U ) ) -> ( ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) -> X e. ( T .(+) U ) ) )
57 56 rexlimdvva
 |-  ( ph -> ( E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) -> X e. ( T .(+) U ) ) )
58 45 57 impbid
 |-  ( ph -> ( X e. ( T .(+) U ) <-> E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )
59 r19.42v
 |-  ( E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> ( X e. V /\ E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) )
60 59 rexbii
 |-  ( E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> E. y e. T ( X e. V /\ E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) )
61 r19.42v
 |-  ( E. y e. T ( X e. V /\ E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> ( X e. V /\ E. y e. T E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) )
62 60 61 bitri
 |-  ( E. y e. T E. z e. U ( X e. V /\ ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) <-> ( X e. V /\ E. y e. T E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) )
63 58 62 bitrdi
 |-  ( ph -> ( X e. ( T .(+) U ) <-> ( X e. V /\ E. y e. T E. z e. U ( N ` { X } ) C_ ( ( N ` { y } ) .(+) ( N ` { z } ) ) ) ) )