Metamath Proof Explorer


Theorem lcvat

Description: If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. ( cvati analog.) (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses lcvat.s
|- S = ( LSubSp ` W )
lcvat.p
|- .(+) = ( LSSum ` W )
lcvat.a
|- A = ( LSAtoms ` W )
icvat.c
|- C = ( 
    lcvat.w
    |- ( ph -> W e. LMod )
    lcvat.t
    |- ( ph -> T e. S )
    lcvat.u
    |- ( ph -> U e. S )
    lcvat.l
    |- ( ph -> T C U )
    Assertion lcvat
    |- ( ph -> E. q e. A ( T .(+) q ) = U )

    Proof

    Step Hyp Ref Expression
    1 lcvat.s
     |-  S = ( LSubSp ` W )
    2 lcvat.p
     |-  .(+) = ( LSSum ` W )
    3 lcvat.a
     |-  A = ( LSAtoms ` W )
    4 icvat.c
     |-  C = ( 
      5 lcvat.w
       |-  ( ph -> W e. LMod )
      6 lcvat.t
       |-  ( ph -> T e. S )
      7 lcvat.u
       |-  ( ph -> U e. S )
      8 lcvat.l
       |-  ( ph -> T C U )
      9 1 4 5 6 7 8 lcvpss
       |-  ( ph -> T C. U )
      10 1 2 3 5 6 7 9 lrelat
       |-  ( ph -> E. q e. A ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) )
      11 5 3ad2ant1
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> W e. LMod )
      12 6 3ad2ant1
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> T e. S )
      13 7 3ad2ant1
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> U e. S )
      14 simp2
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> q e. A )
      15 1 3 11 14 lsatlssel
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> q e. S )
      16 1 2 lsmcl
       |-  ( ( W e. LMod /\ T e. S /\ q e. S ) -> ( T .(+) q ) e. S )
      17 11 12 15 16 syl3anc
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> ( T .(+) q ) e. S )
      18 8 3ad2ant1
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> T C U )
      19 simp3l
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> T C. ( T .(+) q ) )
      20 simp3r
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> ( T .(+) q ) C_ U )
      21 1 4 11 12 13 17 18 19 20 lcvnbtwn2
       |-  ( ( ph /\ q e. A /\ ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) ) -> ( T .(+) q ) = U )
      22 21 3exp
       |-  ( ph -> ( q e. A -> ( ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) -> ( T .(+) q ) = U ) ) )
      23 22 reximdvai
       |-  ( ph -> ( E. q e. A ( T C. ( T .(+) q ) /\ ( T .(+) q ) C_ U ) -> E. q e. A ( T .(+) q ) = U ) )
      24 10 23 mpd
       |-  ( ph -> E. q e. A ( T .(+) q ) = U )