Metamath Proof Explorer

Theorem lcvexch

Description: Subspaces satisfy the exchange axiom. Lemma 7.5 of MaedaMaeda p. 31. ( cvexchi analog.) TODO: combine some lemmas. (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 )
    Assertion lcvexch 
    |- ( ph -> ( ( T i^i U ) C U <-> 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 4 adantr 
       |-  ( ( ph /\ ( T i^i U ) C U ) -> W e. LMod )
      8 5 adantr 
       |-  ( ( ph /\ ( T i^i U ) C U ) -> T e. S )
      9 6 adantr 
       |-  ( ( ph /\ ( T i^i U ) C U ) -> U e. S )
      10 simpr 
       |-  ( ( ph /\ ( T i^i U ) C U ) -> ( T i^i U ) C U )
      11 1 2 3 7 8 9 10 lcvexchlem5 
       |-  ( ( ph /\ ( T i^i U ) C U ) -> T C ( T .(+) U ) )
      12 4 adantr 
       |-  ( ( ph /\ T C ( T .(+) U ) ) -> W e. LMod )
      13 5 adantr 
       |-  ( ( ph /\ T C ( T .(+) U ) ) -> T e. S )
      14 6 adantr 
       |-  ( ( ph /\ T C ( T .(+) U ) ) -> U e. S )
      15 simpr 
       |-  ( ( ph /\ T C ( T .(+) U ) ) -> T C ( T .(+) U ) )
      16 1 2 3 12 13 14 15 lcvexchlem4 
       |-  ( ( ph /\ T C ( T .(+) U ) ) -> ( T i^i U ) C U )
      17 11 16 impbida 
       |-  ( ph -> ( ( T i^i U ) C U <-> T C ( T .(+) U ) ) )