Metamath Proof Explorer


Theorem lcvexchlem3

Description: Lemma for lcvexch . (Contributed by NM, 10-Jan-2015)

Ref Expression
Hypotheses lcvexch.s
|- S = ( LSubSp ` W )
lcvexch.p
|- .(+) = ( LSSum ` W )
lcvexch.c
|- C = ( 
    lcvexch.w
    |- ( ph -> W e. LMod )
    lcvexch.t
    |- ( ph -> T e. S )
    lcvexch.u
    |- ( ph -> U e. S )
    lcvexch.q
    |- ( ph -> R e. S )
    lcvexch.d
    |- ( ph -> T C_ R )
    lcvexch.e
    |- ( ph -> R C_ ( T .(+) U ) )
    Assertion lcvexchlem3
    |- ( ph -> ( ( R i^i U ) .(+) T ) = R )

    Proof

    Step Hyp Ref Expression
    1 lcvexch.s
     |-  S = ( LSubSp ` W )
    2 lcvexch.p
     |-  .(+) = ( LSSum ` W )
    3 lcvexch.c
     |-  C = ( 
      4 lcvexch.w
       |-  ( ph -> W e. LMod )
      5 lcvexch.t
       |-  ( ph -> T e. S )
      6 lcvexch.u
       |-  ( ph -> U e. S )
      7 lcvexch.q
       |-  ( ph -> R e. S )
      8 lcvexch.d
       |-  ( ph -> T C_ R )
      9 lcvexch.e
       |-  ( ph -> R C_ ( T .(+) U ) )
      10 1 lsssssubg
       |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
      11 4 10 syl
       |-  ( ph -> S C_ ( SubGrp ` W ) )
      12 11 7 sseldd
       |-  ( ph -> R e. ( SubGrp ` W ) )
      13 11 6 sseldd
       |-  ( ph -> U e. ( SubGrp ` W ) )
      14 11 5 sseldd
       |-  ( ph -> T e. ( SubGrp ` W ) )
      15 2 lsmmod2
       |-  ( ( ( R e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) /\ T e. ( SubGrp ` W ) ) /\ T C_ R ) -> ( R i^i ( U .(+) T ) ) = ( ( R i^i U ) .(+) T ) )
      16 12 13 14 8 15 syl31anc
       |-  ( ph -> ( R i^i ( U .(+) T ) ) = ( ( R i^i U ) .(+) T ) )
      17 lmodabl
       |-  ( W e. LMod -> W e. Abel )
      18 4 17 syl
       |-  ( ph -> W e. Abel )
      19 2 lsmcom
       |-  ( ( W e. Abel /\ T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( T .(+) U ) = ( U .(+) T ) )
      20 18 14 13 19 syl3anc
       |-  ( ph -> ( T .(+) U ) = ( U .(+) T ) )
      21 9 20 sseqtrd
       |-  ( ph -> R C_ ( U .(+) T ) )
      22 df-ss
       |-  ( R C_ ( U .(+) T ) <-> ( R i^i ( U .(+) T ) ) = R )
      23 21 22 sylib
       |-  ( ph -> ( R i^i ( U .(+) T ) ) = R )
      24 16 23 eqtr3d
       |-  ( ph -> ( ( R i^i U ) .(+) T ) = R )