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