Metamath Proof Explorer

Theorem mapdordlem2

Description: Lemma for mapdord . Ordering property of projectivity M . TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the T hypothesis. (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses mapdord.h 
|- H = ( LHyp ` K )
mapdord.u 
|- U = ( ( DVecH ` K ) ` W )
mapdord.s 
|- S = ( LSubSp ` U )
mapdord.m 
|- M = ( ( mapd ` K ) ` W )
mapdord.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
mapdord.x 
|- ( ph -> X e. S )
mapdord.y 
|- ( ph -> Y e. S )
mapdord.o 
|- O = ( ( ocH ` K ) ` W )
mapdord.a 
|- A = ( LSAtoms ` U )
mapdord.f 
|- F = ( LFnl ` U )
mapdord.c 
|- J = ( LSHyp ` U )
mapdord.l 
|- L = ( LKer ` U )
mapdord.t 
|- T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. J }
mapdord.q 
|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
Assertion mapdordlem2 
|- ( ph -> ( ( M ` X ) C_ ( M ` Y ) <-> X C_ Y ) )

Proof

Step Hyp Ref Expression
1 mapdord.h 
 |-  H = ( LHyp ` K )
2 mapdord.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 mapdord.s 
 |-  S = ( LSubSp ` U )
4 mapdord.m 
 |-  M = ( ( mapd ` K ) ` W )
5 mapdord.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 mapdord.x 
 |-  ( ph -> X e. S )
7 mapdord.y 
 |-  ( ph -> Y e. S )
8 mapdord.o 
 |-  O = ( ( ocH ` K ) ` W )
9 mapdord.a 
 |-  A = ( LSAtoms ` U )
10 mapdord.f 
 |-  F = ( LFnl ` U )
11 mapdord.c 
 |-  J = ( LSHyp ` U )
12 mapdord.l 
 |-  L = ( LKer ` U )
13 mapdord.t 
 |-  T = { g e. F | ( O ` ( O ` ( L ` g ) ) ) e. J }
14 mapdord.q 
 |-  C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
15 1 2 3 10 12 8 4 5 6 14 mapdvalc 
 |-  ( ph -> ( M ` X ) = { f e. C | ( O ` ( L ` f ) ) C_ X } )
16 1 2 3 10 12 8 4 5 7 14 mapdvalc 
 |-  ( ph -> ( M ` Y ) = { f e. C | ( O ` ( L ` f ) ) C_ Y } )
17 15 16 sseq12d 
 |-  ( ph -> ( ( M ` X ) C_ ( M ` Y ) <-> { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } ) )
18 ss2rab 
 |-  ( { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } <-> A. f e. C ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) )
19 eqid 
 |-  ( Base ` U ) = ( Base ` U )
20 1 8 2 19 11 10 12 13 14 5 mapdordlem1a 
 |-  ( ph -> ( f e. T <-> ( f e. C /\ ( O ` ( O ` ( L ` f ) ) ) e. J ) ) )
21 simprl 
 |-  ( ( ph /\ ( f e. C /\ ( O ` ( O ` ( L ` f ) ) ) e. J ) ) -> f e. C )
22 idd 
 |-  ( ( ph /\ ( f e. C /\ ( O ` ( O ` ( L ` f ) ) ) e. J ) ) -> ( ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
23 21 22 embantd 
 |-  ( ( ph /\ ( f e. C /\ ( O ` ( O ` ( L ` f ) ) ) e. J ) ) -> ( ( f e. C -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
24 23 ex 
 |-  ( ph -> ( ( f e. C /\ ( O ` ( O ` ( L ` f ) ) ) e. J ) -> ( ( f e. C -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) ) )
25 20 24 sylbid 
 |-  ( ph -> ( f e. T -> ( ( f e. C -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) ) )
26 25 com23 
 |-  ( ph -> ( ( f e. C -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) -> ( f e. T -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) ) )
27 26 ralimdv2 
 |-  ( ph -> ( A. f e. C ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) -> A. f e. T ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
28 18 27 biimtrid 
 |-  ( ph -> ( { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } -> A. f e. T ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
29 1 2 5 dvhlmod 
 |-  ( ph -> U e. LMod )
30 3 9 29 6 7 lssatle 
 |-  ( ph -> ( X C_ Y <-> A. p e. A ( p C_ X -> p C_ Y ) ) )
31 13 mapdordlem1 
 |-  ( f e. T <-> ( f e. F /\ ( O ` ( O ` ( L ` f ) ) ) e. J ) )
32 31 simprbi 
 |-  ( f e. T -> ( O ` ( O ` ( L ` f ) ) ) e. J )
33 32 adantl 
 |-  ( ( ph /\ f e. T ) -> ( O ` ( O ` ( L ` f ) ) ) e. J )
34 5 adantr 
 |-  ( ( ph /\ f e. T ) -> ( K e. HL /\ W e. H ) )
35 31 simplbi 
 |-  ( f e. T -> f e. F )
36 35 adantl 
 |-  ( ( ph /\ f e. T ) -> f e. F )
37 1 8 2 10 11 12 34 36 dochlkr 
 |-  ( ( ph /\ f e. T ) -> ( ( O ` ( O ` ( L ` f ) ) ) e. J <-> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( L ` f ) e. J ) ) )
38 33 37 mpbid 
 |-  ( ( ph /\ f e. T ) -> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) /\ ( L ` f ) e. J ) )
39 38 simpld 
 |-  ( ( ph /\ f e. T ) -> ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) )
40 38 simprd 
 |-  ( ( ph /\ f e. T ) -> ( L ` f ) e. J )
41 1 8 2 9 11 34 40 dochshpsat 
 |-  ( ( ph /\ f e. T ) -> ( ( O ` ( O ` ( L ` f ) ) ) = ( L ` f ) <-> ( O ` ( L ` f ) ) e. A ) )
42 39 41 mpbid 
 |-  ( ( ph /\ f e. T ) -> ( O ` ( L ` f ) ) e. A )
43 1 2 5 dvhlvec 
 |-  ( ph -> U e. LVec )
44 5 adantr 
 |-  ( ( ph /\ p e. A ) -> ( K e. HL /\ W e. H ) )
45 simpr 
 |-  ( ( ph /\ p e. A ) -> p e. A )
46 1 2 8 9 11 44 45 dochsatshp 
 |-  ( ( ph /\ p e. A ) -> ( O ` p ) e. J )
47 11 10 12 lshpkrex 
 |-  ( ( U e. LVec /\ ( O ` p ) e. J ) -> E. f e. F ( L ` f ) = ( O ` p ) )
48 43 46 47 syl2an2r 
 |-  ( ( ph /\ p e. A ) -> E. f e. F ( L ` f ) = ( O ` p ) )
49 simprl 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> f e. F )
50 simprr 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( L ` f ) = ( O ` p ) )
51 50 fveq2d 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( L ` f ) ) = ( O ` ( O ` p ) ) )
52 51 fveq2d 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` ( L ` f ) ) ) = ( O ` ( O ` ( O ` p ) ) ) )
53 29 adantr 
 |-  ( ( ph /\ p e. A ) -> U e. LMod )
54 19 9 53 45 lsatssv 
 |-  ( ( ph /\ p e. A ) -> p C_ ( Base ` U ) )
55 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
56 1 55 2 19 8 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p C_ ( Base ` U ) ) -> ( O ` p ) e. ran ( ( DIsoH ` K ) ` W ) )
57 5 54 56 syl2an2r 
 |-  ( ( ph /\ p e. A ) -> ( O ` p ) e. ran ( ( DIsoH ` K ) ` W ) )
58 1 55 8 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( O ` p ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( O ` ( O ` ( O ` p ) ) ) = ( O ` p ) )
59 5 57 58 syl2an2r 
 |-  ( ( ph /\ p e. A ) -> ( O ` ( O ` ( O ` p ) ) ) = ( O ` p ) )
60 59 adantr 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` ( O ` p ) ) ) = ( O ` p ) )
61 52 60 eqtrd 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` ( L ` f ) ) ) = ( O ` p ) )
62 46 adantr 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` p ) e. J )
63 61 62 eqeltrd 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` ( L ` f ) ) ) e. J )
64 49 63 31 sylanbrc 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> f e. T )
65 1 2 55 9 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. A ) -> p e. ran ( ( DIsoH ` K ) ` W ) )
66 5 45 65 syl2an2r 
 |-  ( ( ph /\ p e. A ) -> p e. ran ( ( DIsoH ` K ) ` W ) )
67 1 55 8 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ran ( ( DIsoH ` K ) ` W ) ) -> ( O ` ( O ` p ) ) = p )
68 5 66 67 syl2an2r 
 |-  ( ( ph /\ p e. A ) -> ( O ` ( O ` p ) ) = p )
69 68 adantr 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` p ) ) = p )
70 51 69 eqtr2d 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> p = ( O ` ( L ` f ) ) )
71 48 64 70 reximssdv 
 |-  ( ( ph /\ p e. A ) -> E. f e. T p = ( O ` ( L ` f ) ) )
72 sseq1 
 |-  ( p = ( O ` ( L ` f ) ) -> ( p C_ X <-> ( O ` ( L ` f ) ) C_ X ) )
73 sseq1 
 |-  ( p = ( O ` ( L ` f ) ) -> ( p C_ Y <-> ( O ` ( L ` f ) ) C_ Y ) )
74 72 73 imbi12d 
 |-  ( p = ( O ` ( L ` f ) ) -> ( ( p C_ X -> p C_ Y ) <-> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
75 74 adantl 
 |-  ( ( ph /\ p = ( O ` ( L ` f ) ) ) -> ( ( p C_ X -> p C_ Y ) <-> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
76 42 71 75 ralxfrd 
 |-  ( ph -> ( A. p e. A ( p C_ X -> p C_ Y ) <-> A. f e. T ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
77 30 76 bitr2d 
 |-  ( ph -> ( A. f e. T ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) <-> X C_ Y ) )
78 28 77 sylibd 
 |-  ( ph -> ( { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } -> X C_ Y ) )
79 simplr 
 |-  ( ( ( ph /\ X C_ Y ) /\ f e. C ) -> X C_ Y )
80 sstr 
 |-  ( ( ( O ` ( L ` f ) ) C_ X /\ X C_ Y ) -> ( O ` ( L ` f ) ) C_ Y )
81 80 ancoms 
 |-  ( ( X C_ Y /\ ( O ` ( L ` f ) ) C_ X ) -> ( O ` ( L ` f ) ) C_ Y )
82 81 a1i 
 |-  ( ( ( ph /\ X C_ Y ) /\ f e. C ) -> ( ( X C_ Y /\ ( O ` ( L ` f ) ) C_ X ) -> ( O ` ( L ` f ) ) C_ Y ) )
83 79 82 mpand 
 |-  ( ( ( ph /\ X C_ Y ) /\ f e. C ) -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) )
84 83 ss2rabdv 
 |-  ( ( ph /\ X C_ Y ) -> { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } )
85 84 ex 
 |-  ( ph -> ( X C_ Y -> { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } ) )
86 78 85 impbid 
 |-  ( ph -> ( { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } <-> X C_ Y ) )
87 17 86 bitrd 
 |-  ( ph -> ( ( M ` X ) C_ ( M ` Y ) <-> X C_ Y ) )