Metamath Proof Explorer

Theorem lcvexchlem4

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.f 
    |- ( ph -> T C ( T .(+) U ) )
    Assertion lcvexchlem4 
    |- ( ph -> ( T i^i U ) C U )

    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.f 
       |-  ( ph -> T C ( T .(+) U ) )
      8 1 2 lsmcl 
       |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T .(+) U ) e. S )
      9 4 5 6 8 syl3anc 
       |-  ( ph -> ( T .(+) U ) e. S )
      10 1 3 4 5 9 7 lcvpss 
       |-  ( ph -> T C. ( T .(+) U ) )
      11 1 2 3 4 5 6 lcvexchlem1 
       |-  ( ph -> ( T C. ( T .(+) U ) <-> ( T i^i U ) C. U ) )
      12 10 11 mpbid 
       |-  ( ph -> ( T i^i U ) C. U )
      13 4 3ad2ant1 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> W e. LMod )
      14 1 lsssssubg 
       |-  ( W e. LMod -> S C_ ( SubGrp ` W ) )
      15 13 14 syl 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> S C_ ( SubGrp ` W ) )
      16 simp2 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> s e. S )
      17 15 16 sseldd 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> s e. ( SubGrp ` W ) )
      18 5 3ad2ant1 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> T e. S )
      19 15 18 sseldd 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> T e. ( SubGrp ` W ) )
      20 2 lsmub2 
       |-  ( ( s e. ( SubGrp ` W ) /\ T e. ( SubGrp ` W ) ) -> T C_ ( s .(+) T ) )
      21 17 19 20 syl2anc 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> T C_ ( s .(+) T ) )
      22 6 3ad2ant1 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> U e. S )
      23 15 22 sseldd 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> U e. ( SubGrp ` W ) )
      24 simp3r 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> s C_ U )
      25 2 lsmless1 
       |-  ( ( U e. ( SubGrp ` W ) /\ T e. ( SubGrp ` W ) /\ s C_ U ) -> ( s .(+) T ) C_ ( U .(+) T ) )
      26 23 19 24 25 syl3anc 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( s .(+) T ) C_ ( U .(+) T ) )
      27 lmodabl 
       |-  ( W e. LMod -> W e. Abel )
      28 4 27 syl 
       |-  ( ph -> W e. Abel )
      29 4 14 syl 
       |-  ( ph -> S C_ ( SubGrp ` W ) )
      30 29 5 sseldd 
       |-  ( ph -> T e. ( SubGrp ` W ) )
      31 29 6 sseldd 
       |-  ( ph -> U e. ( SubGrp ` W ) )
      32 2 lsmcom 
       |-  ( ( W e. Abel /\ T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> ( T .(+) U ) = ( U .(+) T ) )
      33 28 30 31 32 syl3anc 
       |-  ( ph -> ( T .(+) U ) = ( U .(+) T ) )
      34 33 3ad2ant1 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( T .(+) U ) = ( U .(+) T ) )
      35 26 34 sseqtrrd 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( s .(+) T ) C_ ( T .(+) U ) )
      36 7 3ad2ant1 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> T C ( T .(+) U ) )
      37 1 3 4 5 9 lcvbr3 
       |-  ( ph -> ( T C ( T .(+) U ) <-> ( T C. ( T .(+) U ) /\ A. r e. S ( ( T C_ r /\ r C_ ( T .(+) U ) ) -> ( r = T \/ r = ( T .(+) U ) ) ) ) ) )
      38 37 adantr 
       |-  ( ( ph /\ s e. S ) -> ( T C ( T .(+) U ) <-> ( T C. ( T .(+) U ) /\ A. r e. S ( ( T C_ r /\ r C_ ( T .(+) U ) ) -> ( r = T \/ r = ( T .(+) U ) ) ) ) ) )
      39 4 adantr 
       |-  ( ( ph /\ s e. S ) -> W e. LMod )
      40 simpr 
       |-  ( ( ph /\ s e. S ) -> s e. S )
      41 5 adantr 
       |-  ( ( ph /\ s e. S ) -> T e. S )
      42 1 2 lsmcl 
       |-  ( ( W e. LMod /\ s e. S /\ T e. S ) -> ( s .(+) T ) e. S )
      43 39 40 41 42 syl3anc 
       |-  ( ( ph /\ s e. S ) -> ( s .(+) T ) e. S )
      44 sseq2 
       |-  ( r = ( s .(+) T ) -> ( T C_ r <-> T C_ ( s .(+) T ) ) )
      45 sseq1 
       |-  ( r = ( s .(+) T ) -> ( r C_ ( T .(+) U ) <-> ( s .(+) T ) C_ ( T .(+) U ) ) )
      46 44 45 anbi12d 
       |-  ( r = ( s .(+) T ) -> ( ( T C_ r /\ r C_ ( T .(+) U ) ) <-> ( T C_ ( s .(+) T ) /\ ( s .(+) T ) C_ ( T .(+) U ) ) ) )
      47 eqeq1 
       |-  ( r = ( s .(+) T ) -> ( r = T <-> ( s .(+) T ) = T ) )
      48 eqeq1 
       |-  ( r = ( s .(+) T ) -> ( r = ( T .(+) U ) <-> ( s .(+) T ) = ( T .(+) U ) ) )
      49 47 48 orbi12d 
       |-  ( r = ( s .(+) T ) -> ( ( r = T \/ r = ( T .(+) U ) ) <-> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) ) )
      50 46 49 imbi12d 
       |-  ( r = ( s .(+) T ) -> ( ( ( T C_ r /\ r C_ ( T .(+) U ) ) -> ( r = T \/ r = ( T .(+) U ) ) ) <-> ( ( T C_ ( s .(+) T ) /\ ( s .(+) T ) C_ ( T .(+) U ) ) -> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) ) ) )
      51 50 rspcv 
       |-  ( ( s .(+) T ) e. S -> ( A. r e. S ( ( T C_ r /\ r C_ ( T .(+) U ) ) -> ( r = T \/ r = ( T .(+) U ) ) ) -> ( ( T C_ ( s .(+) T ) /\ ( s .(+) T ) C_ ( T .(+) U ) ) -> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) ) ) )
      52 43 51 syl 
       |-  ( ( ph /\ s e. S ) -> ( A. r e. S ( ( T C_ r /\ r C_ ( T .(+) U ) ) -> ( r = T \/ r = ( T .(+) U ) ) ) -> ( ( T C_ ( s .(+) T ) /\ ( s .(+) T ) C_ ( T .(+) U ) ) -> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) ) ) )
      53 52 adantld 
       |-  ( ( ph /\ s e. S ) -> ( ( T C. ( T .(+) U ) /\ A. r e. S ( ( T C_ r /\ r C_ ( T .(+) U ) ) -> ( r = T \/ r = ( T .(+) U ) ) ) ) -> ( ( T C_ ( s .(+) T ) /\ ( s .(+) T ) C_ ( T .(+) U ) ) -> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) ) ) )
      54 38 53 sylbid 
       |-  ( ( ph /\ s e. S ) -> ( T C ( T .(+) U ) -> ( ( T C_ ( s .(+) T ) /\ ( s .(+) T ) C_ ( T .(+) U ) ) -> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) ) ) )
      55 54 3adant3 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( T C ( T .(+) U ) -> ( ( T C_ ( s .(+) T ) /\ ( s .(+) T ) C_ ( T .(+) U ) ) -> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) ) ) )
      56 36 55 mpd 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( T C_ ( s .(+) T ) /\ ( s .(+) T ) C_ ( T .(+) U ) ) -> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) ) )
      57 21 35 56 mp2and 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) )
      58 ineq1 
       |-  ( ( s .(+) T ) = T -> ( ( s .(+) T ) i^i U ) = ( T i^i U ) )
      59 simp3l 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( T i^i U ) C_ s )
      60 1 2 3 13 18 22 16 59 24 lcvexchlem2 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( s .(+) T ) i^i U ) = s )
      61 60 eqeq1d 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( ( s .(+) T ) i^i U ) = ( T i^i U ) <-> s = ( T i^i U ) ) )
      62 58 61 imbitrid 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( s .(+) T ) = T -> s = ( T i^i U ) ) )
      63 ineq1 
       |-  ( ( s .(+) T ) = ( T .(+) U ) -> ( ( s .(+) T ) i^i U ) = ( ( T .(+) U ) i^i U ) )
      64 2 lsmub2 
       |-  ( ( T e. ( SubGrp ` W ) /\ U e. ( SubGrp ` W ) ) -> U C_ ( T .(+) U ) )
      65 19 23 64 syl2anc 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> U C_ ( T .(+) U ) )
      66 sseqin2 
       |-  ( U C_ ( T .(+) U ) <-> ( ( T .(+) U ) i^i U ) = U )
      67 65 66 sylib 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( T .(+) U ) i^i U ) = U )
      68 60 67 eqeq12d 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( ( s .(+) T ) i^i U ) = ( ( T .(+) U ) i^i U ) <-> s = U ) )
      69 63 68 imbitrid 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( s .(+) T ) = ( T .(+) U ) -> s = U ) )
      70 62 69 orim12d 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( ( ( s .(+) T ) = T \/ ( s .(+) T ) = ( T .(+) U ) ) -> ( s = ( T i^i U ) \/ s = U ) ) )
      71 57 70 mpd 
       |-  ( ( ph /\ s e. S /\ ( ( T i^i U ) C_ s /\ s C_ U ) ) -> ( s = ( T i^i U ) \/ s = U ) )
      72 71 3exp 
       |-  ( ph -> ( s e. S -> ( ( ( T i^i U ) C_ s /\ s C_ U ) -> ( s = ( T i^i U ) \/ s = U ) ) ) )
      73 72 ralrimiv 
       |-  ( ph -> A. s e. S ( ( ( T i^i U ) C_ s /\ s C_ U ) -> ( s = ( T i^i U ) \/ s = U ) ) )
      74 1 lssincl 
       |-  ( ( W e. LMod /\ T e. S /\ U e. S ) -> ( T i^i U ) e. S )
      75 4 5 6 74 syl3anc 
       |-  ( ph -> ( T i^i U ) e. S )
      76 1 3 4 75 6 lcvbr3 
       |-  ( ph -> ( ( T i^i U ) C U <-> ( ( T i^i U ) C. U /\ A. s e. S ( ( ( T i^i U ) C_ s /\ s C_ U ) -> ( s = ( T i^i U ) \/ s = U ) ) ) ) )
      77 12 73 76 mpbir2and 
       |-  ( ph -> ( T i^i U ) C U )