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 )