Metamath Proof Explorer

Theorem lsatexch

Description: The atom exchange property. Proposition 1(i) of Kalmbach p. 140. A version of this theorem was originally proved by Hermann Grassmann in 1862. ( atexch analog.) (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lsatexch.s 
|- S = ( LSubSp ` W )
lsatexch.p 
|- .(+) = ( LSSum ` W )
lsatexch.o 
|- .0. = ( 0g ` W )
lsatexch.a 
|- A = ( LSAtoms ` W )
lsatexch.w 
|- ( ph -> W e. LVec )
lsatexch.u 
|- ( ph -> U e. S )
lsatexch.q 
|- ( ph -> Q e. A )
lsatexch.r 
|- ( ph -> R e. A )
lsatexch.l 
|- ( ph -> Q C_ ( U .(+) R ) )
lsatexch.z 
|- ( ph -> ( U i^i Q ) = { .0. } )
Assertion lsatexch 
|- ( ph -> R C_ ( U .(+) Q ) )

Proof

Step Hyp Ref Expression
1 lsatexch.s 
 |-  S = ( LSubSp ` W )
2 lsatexch.p 
 |-  .(+) = ( LSSum ` W )
3 lsatexch.o 
 |-  .0. = ( 0g ` W )
4 lsatexch.a 
 |-  A = ( LSAtoms ` W )
5 lsatexch.w 
 |-  ( ph -> W e. LVec )
6 lsatexch.u 
 |-  ( ph -> U e. S )
7 lsatexch.q 
 |-  ( ph -> Q e. A )
8 lsatexch.r 
 |-  ( ph -> R e. A )
9 lsatexch.l 
 |-  ( ph -> Q C_ ( U .(+) R ) )
10 lsatexch.z 
 |-  ( ph -> ( U i^i Q ) = { .0. } )
11 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
12 5 11 syl 
 |-  ( ph -> W e. LMod )
13 1 lsssssubg 
 |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
14 12 13 syl 
 |-  ( ph -> S C_ ( SubGrp ` W ) )
15 14 6 sseldd 
 |-  ( ph -> U e. ( SubGrp ` W ) )
16 1 4 12 8 lsatlssel 
 |-  ( ph -> R e. S )
17 14 16 sseldd 
 |-  ( ph -> R e. ( SubGrp ` W ) )
18 2 lsmub2 
 |-  ( ( U e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) ) -> R C_ ( U .(+) R ) )
19 15 17 18 syl2anc 
 |-  ( ph -> R C_ ( U .(+) R ) )
20 eqid 
 |-  (
    21 1 2 lsmcl 
     |-  ( ( W e. LMod /\ U e. S /\ R e. S ) -> ( U .(+) R ) e. S )
    22 12 6 16 21 syl3anc 
     |-  ( ph -> ( U .(+) R ) e. S )
    23 1 4 12 7 lsatlssel 
     |-  ( ph -> Q e. S )
    24 1 2 lsmcl 
     |-  ( ( W e. LMod /\ U e. S /\ Q e. S ) -> ( U .(+) Q ) e. S )
    25 12 6 23 24 syl3anc 
     |-  ( ph -> ( U .(+) Q ) e. S )
    26 1 2 3 4 20 5 6 7 lcvp 
     |-  ( ph -> ( ( U i^i Q ) = { .0. } <-> U (
      27 10 26 mpbid 
       |-  ( ph -> U (
        28 1 20 5 6 25 27 lcvpss 
         |-  ( ph -> U C. ( U .(+) Q ) )
        29 2 lsmub1 
         |-  ( ( U e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) ) -> U C_ ( U .(+) R ) )
        30 15 17 29 syl2anc 
         |-  ( ph -> U C_ ( U .(+) R ) )
        31 14 23 sseldd 
         |-  ( ph -> Q e. ( SubGrp ` W ) )
        32 14 22 sseldd 
         |-  ( ph -> ( U .(+) R ) e. ( SubGrp ` W ) )
        33 2 lsmlub 
         |-  ( ( U e. ( SubGrp ` W ) /\ Q e. ( SubGrp ` W ) /\ ( U .(+) R ) e. ( SubGrp ` W ) ) -> ( ( U C_ ( U .(+) R ) /\ Q C_ ( U .(+) R ) ) <-> ( U .(+) Q ) C_ ( U .(+) R ) ) )
        34 15 31 32 33 syl3anc 
         |-  ( ph -> ( ( U C_ ( U .(+) R ) /\ Q C_ ( U .(+) R ) ) <-> ( U .(+) Q ) C_ ( U .(+) R ) ) )
        35 30 9 34 mpbi2and 
         |-  ( ph -> ( U .(+) Q ) C_ ( U .(+) R ) )
        36 28 35 psssstrd 
         |-  ( ph -> U C. ( U .(+) R ) )
        37 1 2 4 20 5 6 8 lcv2 
         |-  ( ph -> ( U C. ( U .(+) R ) <-> U (
          38 36 37 mpbid 
           |-  ( ph -> U (
            39 1 20 5 6 22 25 38 28 35 lcvnbtwn2 
             |-  ( ph -> ( U .(+) Q ) = ( U .(+) R ) )
            40 19 39 sseqtrrd 
             |-  ( ph -> R C_ ( U .(+) Q ) )