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