Metamath Proof Explorer

Theorem mapdcv

Description: Covering property of the converse of the map defined by df-mapd . (Contributed by NM, 14-Mar-2015)

Ref Expression
Hypotheses mapdcv.h 
|- H = ( LHyp ` K )
mapdcv.m 
|- M = ( ( mapd ` K ) ` W )
mapdcv.u 
|- U = ( ( DVecH ` K ) ` W )
mapdcv.s 
|- S = ( LSubSp ` U )
mapdcv.c 
|- C = (
    mapdcv.d 
    |- D = ( ( LCDual ` K ) ` W )
    mapdcv.e 
    |- E = (
      mapdcv.k 
      |- ( ph -> ( K e. HL /\ W e. H ) )
      mapdcv.x 
      |- ( ph -> X e. S )
      mapdcv.y 
      |- ( ph -> Y e. S )
      Assertion mapdcv 
      |- ( ph -> ( X C Y <-> ( M ` X ) E ( M ` Y ) ) )

      Proof

      Step Hyp Ref Expression
      1 mapdcv.h 
       |-  H = ( LHyp ` K )
      2 mapdcv.m 
       |-  M = ( ( mapd ` K ) ` W )
      3 mapdcv.u 
       |-  U = ( ( DVecH ` K ) ` W )
      4 mapdcv.s 
       |-  S = ( LSubSp ` U )
      5 mapdcv.c 
       |-  C = (
        6 mapdcv.d 
         |-  D = ( ( LCDual ` K ) ` W )
        7 mapdcv.e 
         |-  E = (
          8 mapdcv.k 
           |-  ( ph -> ( K e. HL /\ W e. H ) )
          9 mapdcv.x 
           |-  ( ph -> X e. S )
          10 mapdcv.y 
           |-  ( ph -> Y e. S )
          11 1 2 3 4 8 9 10 mapdsord 
           |-  ( ph -> ( ( M ` X ) C. ( M ` Y ) <-> X C. Y ) )
          12 eqid 
           |-  ( LSubSp ` D ) = ( LSubSp ` D )
          13 8 adantr 
           |-  ( ( ph /\ v e. S ) -> ( K e. HL /\ W e. H ) )
          14 simpr 
           |-  ( ( ph /\ v e. S ) -> v e. S )
          15 1 2 3 4 6 12 13 14 mapdcl2 
           |-  ( ( ph /\ v e. S ) -> ( M ` v ) e. ( LSubSp ` D ) )
          16 8 adantr 
           |-  ( ( ph /\ f e. ( LSubSp ` D ) ) -> ( K e. HL /\ W e. H ) )
          17 1 2 6 12 8 mapdrn2 
           |-  ( ph -> ran M = ( LSubSp ` D ) )
          18 17 eleq2d 
           |-  ( ph -> ( f e. ran M <-> f e. ( LSubSp ` D ) ) )
          19 18 biimpar 
           |-  ( ( ph /\ f e. ( LSubSp ` D ) ) -> f e. ran M )
          20 1 2 3 4 16 19 mapdcnvcl 
           |-  ( ( ph /\ f e. ( LSubSp ` D ) ) -> ( `' M ` f ) e. S )
          21 1 2 16 19 mapdcnvid2 
           |-  ( ( ph /\ f e. ( LSubSp ` D ) ) -> ( M ` ( `' M ` f ) ) = f )
          22 21 eqcomd 
           |-  ( ( ph /\ f e. ( LSubSp ` D ) ) -> f = ( M ` ( `' M ` f ) ) )
          23 fveq2 
           |-  ( v = ( `' M ` f ) -> ( M ` v ) = ( M ` ( `' M ` f ) ) )
          24 23 rspceeqv 
           |-  ( ( ( `' M ` f ) e. S /\ f = ( M ` ( `' M ` f ) ) ) -> E. v e. S f = ( M ` v ) )
          25 20 22 24 syl2anc 
           |-  ( ( ph /\ f e. ( LSubSp ` D ) ) -> E. v e. S f = ( M ` v ) )
          26 psseq2 
           |-  ( f = ( M ` v ) -> ( ( M ` X ) C. f <-> ( M ` X ) C. ( M ` v ) ) )
          27 psseq1 
           |-  ( f = ( M ` v ) -> ( f C. ( M ` Y ) <-> ( M ` v ) C. ( M ` Y ) ) )
          28 26 27 anbi12d 
           |-  ( f = ( M ` v ) -> ( ( ( M ` X ) C. f /\ f C. ( M ` Y ) ) <-> ( ( M ` X ) C. ( M ` v ) /\ ( M ` v ) C. ( M ` Y ) ) ) )
          29 28 adantl 
           |-  ( ( ph /\ f = ( M ` v ) ) -> ( ( ( M ` X ) C. f /\ f C. ( M ` Y ) ) <-> ( ( M ` X ) C. ( M ` v ) /\ ( M ` v ) C. ( M ` Y ) ) ) )
          30 15 25 29 rexxfrd 
           |-  ( ph -> ( E. f e. ( LSubSp ` D ) ( ( M ` X ) C. f /\ f C. ( M ` Y ) ) <-> E. v e. S ( ( M ` X ) C. ( M ` v ) /\ ( M ` v ) C. ( M ` Y ) ) ) )
          31 9 adantr 
           |-  ( ( ph /\ v e. S ) -> X e. S )
          32 1 2 3 4 13 31 14 mapdsord 
           |-  ( ( ph /\ v e. S ) -> ( ( M ` X ) C. ( M ` v ) <-> X C. v ) )
          33 10 adantr 
           |-  ( ( ph /\ v e. S ) -> Y e. S )
          34 1 2 3 4 13 14 33 mapdsord 
           |-  ( ( ph /\ v e. S ) -> ( ( M ` v ) C. ( M ` Y ) <-> v C. Y ) )
          35 32 34 anbi12d 
           |-  ( ( ph /\ v e. S ) -> ( ( ( M ` X ) C. ( M ` v ) /\ ( M ` v ) C. ( M ` Y ) ) <-> ( X C. v /\ v C. Y ) ) )
          36 35 rexbidva 
           |-  ( ph -> ( E. v e. S ( ( M ` X ) C. ( M ` v ) /\ ( M ` v ) C. ( M ` Y ) ) <-> E. v e. S ( X C. v /\ v C. Y ) ) )
          37 30 36 bitrd 
           |-  ( ph -> ( E. f e. ( LSubSp ` D ) ( ( M ` X ) C. f /\ f C. ( M ` Y ) ) <-> E. v e. S ( X C. v /\ v C. Y ) ) )
          38 37 notbid 
           |-  ( ph -> ( -. E. f e. ( LSubSp ` D ) ( ( M ` X ) C. f /\ f C. ( M ` Y ) ) <-> -. E. v e. S ( X C. v /\ v C. Y ) ) )
          39 11 38 anbi12d 
           |-  ( ph -> ( ( ( M ` X ) C. ( M ` Y ) /\ -. E. f e. ( LSubSp ` D ) ( ( M ` X ) C. f /\ f C. ( M ` Y ) ) ) <-> ( X C. Y /\ -. E. v e. S ( X C. v /\ v C. Y ) ) ) )
          40 1 6 8 lcdlmod 
           |-  ( ph -> D e. LMod )
          41 1 2 3 4 6 12 8 9 mapdcl2 
           |-  ( ph -> ( M ` X ) e. ( LSubSp ` D ) )
          42 1 2 3 4 6 12 8 10 mapdcl2 
           |-  ( ph -> ( M ` Y ) e. ( LSubSp ` D ) )
          43 12 7 40 41 42 lcvbr 
           |-  ( ph -> ( ( M ` X ) E ( M ` Y ) <-> ( ( M ` X ) C. ( M ` Y ) /\ -. E. f e. ( LSubSp ` D ) ( ( M ` X ) C. f /\ f C. ( M ` Y ) ) ) ) )
          44 1 3 8 dvhlmod 
           |-  ( ph -> U e. LMod )
          45 4 5 44 9 10 lcvbr 
           |-  ( ph -> ( X C Y <-> ( X C. Y /\ -. E. v e. S ( X C. v /\ v C. Y ) ) ) )
          46 39 43 45 3bitr4rd 
           |-  ( ph -> ( X C Y <-> ( M ` X ) E ( M ` Y ) ) )