Metamath Proof Explorer

Theorem lcvexchlem5

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