Metamath Proof Explorer

Theorem islshpcv

Description: Hyperplane properties expressed with covers relation. (Contributed by NM, 11-Jan-2015)

Ref Expression
Hypotheses islshpcv.v 
|- V = ( Base ` W )
islshpcv.s 
|- S = ( LSubSp ` W )
islshpcv.h 
|- H = ( LSHyp ` W )
islshpcv.c 
|- C = (
    islshpcv.w 
    |- ( ph -> W e. LVec )
    Assertion islshpcv 
    |- ( ph -> ( U e. H <-> ( U e. S /\ U C V ) ) )

    Proof

    Step Hyp Ref Expression
    1 islshpcv.v 
     |-  V = ( Base ` W )
    2 islshpcv.s 
     |-  S = ( LSubSp ` W )
    3 islshpcv.h 
     |-  H = ( LSHyp ` W )
    4 islshpcv.c 
     |-  C = (
      5 islshpcv.w 
       |-  ( ph -> W e. LVec )
      6 eqid 
       |-  ( LSSum ` W ) = ( LSSum ` W )
      7 eqid 
       |-  ( LSAtoms ` W ) = ( LSAtoms ` W )
      8 lveclmod 
       |-  ( W e. LVec -> W e. LMod )
      9 5 8 syl 
       |-  ( ph -> W e. LMod )
      10 1 2 6 3 7 9 islshpat 
       |-  ( ph -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. q e. ( LSAtoms ` W ) ( U ( LSSum ` W ) q ) = V ) ) )
      11 simp12 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> U e. S )
      12 1 2 lssss 
       |-  ( U e. S -> U C_ V )
      13 11 12 syl 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> U C_ V )
      14 simp13 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> U =/= V )
      15 df-pss 
       |-  ( U C. V <-> ( U C_ V /\ U =/= V ) )
      16 13 14 15 sylanbrc 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> U C. V )
      17 psseq2 
       |-  ( ( U ( LSSum ` W ) q ) = V -> ( U C. ( U ( LSSum ` W ) q ) <-> U C. V ) )
      18 17 3ad2ant3 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> ( U C. ( U ( LSSum ` W ) q ) <-> U C. V ) )
      19 16 18 mpbird 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> U C. ( U ( LSSum ` W ) q ) )
      20 5 3ad2ant1 
       |-  ( ( ph /\ U e. S /\ U =/= V ) -> W e. LVec )
      21 20 3ad2ant1 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> W e. LVec )
      22 simp2 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> q e. ( LSAtoms ` W ) )
      23 2 6 7 4 21 11 22 lcv2 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> ( U C. ( U ( LSSum ` W ) q ) <-> U C ( U ( LSSum ` W ) q ) ) )
      24 19 23 mpbid 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> U C ( U ( LSSum ` W ) q ) )
      25 simp3 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> ( U ( LSSum ` W ) q ) = V )
      26 24 25 breqtrd 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> U C V )
      27 11 26 jca 
       |-  ( ( ( ph /\ U e. S /\ U =/= V ) /\ q e. ( LSAtoms ` W ) /\ ( U ( LSSum ` W ) q ) = V ) -> ( U e. S /\ U C V ) )
      28 27 rexlimdv3a 
       |-  ( ( ph /\ U e. S /\ U =/= V ) -> ( E. q e. ( LSAtoms ` W ) ( U ( LSSum ` W ) q ) = V -> ( U e. S /\ U C V ) ) )
      29 28 3exp 
       |-  ( ph -> ( U e. S -> ( U =/= V -> ( E. q e. ( LSAtoms ` W ) ( U ( LSSum ` W ) q ) = V -> ( U e. S /\ U C V ) ) ) ) )
      30 29 3impd 
       |-  ( ph -> ( ( U e. S /\ U =/= V /\ E. q e. ( LSAtoms ` W ) ( U ( LSSum ` W ) q ) = V ) -> ( U e. S /\ U C V ) ) )
      31 simprl 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> U e. S )
      32 5 adantr 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> W e. LVec )
      33 9 adantr 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> W e. LMod )
      34 1 2 lss1 
       |-  ( W e. LMod -> V e. S )
      35 33 34 syl 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> V e. S )
      36 simprr 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> U C V )
      37 2 4 32 31 35 36 lcvpss 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> U C. V )
      38 37 pssned 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> U =/= V )
      39 2 6 7 4 33 31 35 36 lcvat 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> E. q e. ( LSAtoms ` W ) ( U ( LSSum ` W ) q ) = V )
      40 31 38 39 3jca 
       |-  ( ( ph /\ ( U e. S /\ U C V ) ) -> ( U e. S /\ U =/= V /\ E. q e. ( LSAtoms ` W ) ( U ( LSSum ` W ) q ) = V ) )
      41 40 ex 
       |-  ( ph -> ( ( U e. S /\ U C V ) -> ( U e. S /\ U =/= V /\ E. q e. ( LSAtoms ` W ) ( U ( LSSum ` W ) q ) = V ) ) )
      42 30 41 impbid 
       |-  ( ph -> ( ( U e. S /\ U =/= V /\ E. q e. ( LSAtoms ` W ) ( U ( LSSum ` W ) q ) = V ) <-> ( U e. S /\ U C V ) ) )
      43 10 42 bitrd 
       |-  ( ph -> ( U e. H <-> ( U e. S /\ U C V ) ) )