This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem l1cvat

Description: Create an atom under an element covered by the lattice unity. Part of proof of Lemma B in Crawley p. 112. ( 1cvrat analog.) (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses l1cvat.v 
|- V = ( Base ` W )
l1cvat.s 
|- S = ( LSubSp ` W )
l1cvat.p 
|- .(+) = ( LSSum ` W )
l1cvat.a 
|- A = ( LSAtoms ` W )
l1cvat.c 
|- C = (
    l1cvat.w 
    |- ( ph -> W e. LVec )
    l1cvat.u 
    |- ( ph -> U e. S )
    l1cvat.q 
    |- ( ph -> Q e. A )
    l1cvat.r 
    |- ( ph -> R e. A )
    l1cvat.n 
    |- ( ph -> Q =/= R )
    l1cvat.l 
    |- ( ph -> U C V )
    l1cvat.m 
    |- ( ph -> -. Q C_ U )
    Assertion l1cvat 
    |- ( ph -> ( ( Q .(+) R ) i^i U ) e. A )

    Proof

    Step Hyp Ref Expression
    1 l1cvat.v 
     |-  V = ( Base ` W )
    2 l1cvat.s 
     |-  S = ( LSubSp ` W )
    3 l1cvat.p 
     |-  .(+) = ( LSSum ` W )
    4 l1cvat.a 
     |-  A = ( LSAtoms ` W )
    5 l1cvat.c 
     |-  C = (
      6 l1cvat.w 
       |-  ( ph -> W e. LVec )
      7 l1cvat.u 
       |-  ( ph -> U e. S )
      8 l1cvat.q 
       |-  ( ph -> Q e. A )
      9 l1cvat.r 
       |-  ( ph -> R e. A )
      10 l1cvat.n 
       |-  ( ph -> Q =/= R )
      11 l1cvat.l 
       |-  ( ph -> U C V )
      12 l1cvat.m 
       |-  ( ph -> -. Q C_ U )
      13 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      14 6 13 syl 
       |-  ( ph -> W e. LMod )
      15 lmodabl 
       |-  ( W e. LMod -> W e. Abel )
      16 14 15 syl 
       |-  ( ph -> W e. Abel )
      17 2 lsssssubg 
       |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
      18 14 17 syl 
       |-  ( ph -> S C_ ( SubGrp ` W ) )
      19 2 4 14 8 lsatlssel 
       |-  ( ph -> Q e. S )
      20 18 19 sseldd 
       |-  ( ph -> Q e. ( SubGrp ` W ) )
      21 2 4 14 9 lsatlssel 
       |-  ( ph -> R e. S )
      22 18 21 sseldd 
       |-  ( ph -> R e. ( SubGrp ` W ) )
      23 3 lsmcom 
       |-  ( ( W e. Abel /\ Q e. ( SubGrp ` W ) /\ R e. ( SubGrp ` W ) ) -> ( Q .(+) R ) = ( R .(+) Q ) )
      24 16 20 22 23 syl3anc 
       |-  ( ph -> ( Q .(+) R ) = ( R .(+) Q ) )
      25 24 ineq1d 
       |-  ( ph -> ( ( Q .(+) R ) i^i U ) = ( ( R .(+) Q ) i^i U ) )
      26 incom 
       |-  ( ( R .(+) Q ) i^i U ) = ( U i^i ( R .(+) Q ) )
      27 25 26 eqtrdi 
       |-  ( ph -> ( ( Q .(+) R ) i^i U ) = ( U i^i ( R .(+) Q ) ) )
      28 10 necomd 
       |-  ( ph -> R =/= Q )
      29 1 4 14 9 lsatssv 
       |-  ( ph -> R C_ V )
      30 1 2 3 4 5 6 7 8 11 12 l1cvpat 
       |-  ( ph -> ( U .(+) Q ) = V )
      31 29 30 sseqtrrd 
       |-  ( ph -> R C_ ( U .(+) Q ) )
      32 2 3 4 6 7 9 8 28 12 31 lsatcvat3 
       |-  ( ph -> ( U i^i ( R .(+) Q ) ) e. A )
      33 27 32 eqeltrd 
       |-  ( ph -> ( ( Q .(+) R ) i^i U ) e. A )