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 syl5bi 
 |-  ( 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 43 adantr 
 |-  ( ( ph /\ p e. A ) -> U e. LVec )
45 5 adantr 
 |-  ( ( ph /\ p e. A ) -> ( K e. HL /\ W e. H ) )
46 simpr 
 |-  ( ( ph /\ p e. A ) -> p e. A )
47 1 2 8 9 11 45 46 dochsatshp 
 |-  ( ( ph /\ p e. A ) -> ( O ` p ) e. J )
48 11 10 12 lshpkrex 
 |-  ( ( U e. LVec /\ ( O ` p ) e. J ) -> E. f e. F ( L ` f ) = ( O ` p ) )
49 44 47 48 syl2anc 
 |-  ( ( ph /\ p e. A ) -> E. f e. F ( L ` f ) = ( O ` p ) )
50 df-rex 
 |-  ( E. f e. F ( L ` f ) = ( O ` p ) <-> E. f ( f e. F /\ ( L ` f ) = ( O ` p ) ) )
51 49 50 sylib 
 |-  ( ( ph /\ p e. A ) -> E. f ( f e. F /\ ( L ` f ) = ( O ` p ) ) )
52 simprl 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> f e. F )
53 simprr 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( L ` f ) = ( O ` p ) )
54 53 fveq2d 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( L ` f ) ) = ( O ` ( O ` p ) ) )
55 54 fveq2d 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` ( L ` f ) ) ) = ( O ` ( O ` ( O ` p ) ) ) )
56 29 adantr 
 |-  ( ( ph /\ p e. A ) -> U e. LMod )
57 19 9 56 46 lsatssv 
 |-  ( ( ph /\ p e. A ) -> p C_ ( Base ` U ) )
58 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
59 1 58 2 19 8 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p C_ ( Base ` U ) ) -> ( O ` p ) e. ran ( ( DIsoH ` K ) ` W ) )
60 45 57 59 syl2anc 
 |-  ( ( ph /\ p e. A ) -> ( O ` p ) e. ran ( ( DIsoH ` K ) ` W ) )
61 1 58 8 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( O ` p ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( O ` ( O ` ( O ` p ) ) ) = ( O ` p ) )
62 45 60 61 syl2anc 
 |-  ( ( ph /\ p e. A ) -> ( O ` ( O ` ( O ` p ) ) ) = ( O ` p ) )
63 62 adantr 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` ( O ` p ) ) ) = ( O ` p ) )
64 55 63 eqtrd 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` ( L ` f ) ) ) = ( O ` p ) )
65 47 adantr 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` p ) e. J )
66 64 65 eqeltrd 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` ( L ` f ) ) ) e. J )
67 52 66 31 sylanbrc 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> f e. T )
68 1 2 58 9 dih1dimat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. A ) -> p e. ran ( ( DIsoH ` K ) ` W ) )
69 45 46 68 syl2anc 
 |-  ( ( ph /\ p e. A ) -> p e. ran ( ( DIsoH ` K ) ` W ) )
70 1 58 8 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ p e. ran ( ( DIsoH ` K ) ` W ) ) -> ( O ` ( O ` p ) ) = p )
71 45 69 70 syl2anc 
 |-  ( ( ph /\ p e. A ) -> ( O ` ( O ` p ) ) = p )
72 71 adantr 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( O ` ( O ` p ) ) = p )
73 54 72 eqtr2d 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> p = ( O ` ( L ` f ) ) )
74 67 73 jca 
 |-  ( ( ( ph /\ p e. A ) /\ ( f e. F /\ ( L ` f ) = ( O ` p ) ) ) -> ( f e. T /\ p = ( O ` ( L ` f ) ) ) )
75 74 ex 
 |-  ( ( ph /\ p e. A ) -> ( ( f e. F /\ ( L ` f ) = ( O ` p ) ) -> ( f e. T /\ p = ( O ` ( L ` f ) ) ) ) )
76 75 eximdv 
 |-  ( ( ph /\ p e. A ) -> ( E. f ( f e. F /\ ( L ` f ) = ( O ` p ) ) -> E. f ( f e. T /\ p = ( O ` ( L ` f ) ) ) ) )
77 51 76 mpd 
 |-  ( ( ph /\ p e. A ) -> E. f ( f e. T /\ p = ( O ` ( L ` f ) ) ) )
78 df-rex 
 |-  ( E. f e. T p = ( O ` ( L ` f ) ) <-> E. f ( f e. T /\ p = ( O ` ( L ` f ) ) ) )
79 77 78 sylibr 
 |-  ( ( ph /\ p e. A ) -> E. f e. T p = ( O ` ( L ` f ) ) )
80 sseq1 
 |-  ( p = ( O ` ( L ` f ) ) -> ( p C_ X <-> ( O ` ( L ` f ) ) C_ X ) )
81 sseq1 
 |-  ( p = ( O ` ( L ` f ) ) -> ( p C_ Y <-> ( O ` ( L ` f ) ) C_ Y ) )
82 80 81 imbi12d 
 |-  ( p = ( O ` ( L ` f ) ) -> ( ( p C_ X -> p C_ Y ) <-> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
83 82 adantl 
 |-  ( ( ph /\ p = ( O ` ( L ` f ) ) ) -> ( ( p C_ X -> p C_ Y ) <-> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) ) )
84 42 79 83 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 ) ) )
85 30 84 bitr2d 
 |-  ( ph -> ( A. f e. T ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) <-> X C_ Y ) )
86 28 85 sylibd 
 |-  ( ph -> ( { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } -> X C_ Y ) )
87 simplr 
 |-  ( ( ( ph /\ X C_ Y ) /\ f e. C ) -> X C_ Y )
88 sstr 
 |-  ( ( ( O ` ( L ` f ) ) C_ X /\ X C_ Y ) -> ( O ` ( L ` f ) ) C_ Y )
89 88 ancoms 
 |-  ( ( X C_ Y /\ ( O ` ( L ` f ) ) C_ X ) -> ( O ` ( L ` f ) ) C_ Y )
90 89 a1i 
 |-  ( ( ( ph /\ X C_ Y ) /\ f e. C ) -> ( ( X C_ Y /\ ( O ` ( L ` f ) ) C_ X ) -> ( O ` ( L ` f ) ) C_ Y ) )
91 87 90 mpand 
 |-  ( ( ( ph /\ X C_ Y ) /\ f e. C ) -> ( ( O ` ( L ` f ) ) C_ X -> ( O ` ( L ` f ) ) C_ Y ) )
92 91 ss2rabdv 
 |-  ( ( ph /\ X C_ Y ) -> { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } )
93 92 ex 
 |-  ( ph -> ( X C_ Y -> { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } ) )
94 86 93 impbid 
 |-  ( ph -> ( { f e. C | ( O ` ( L ` f ) ) C_ X } C_ { f e. C | ( O ` ( L ` f ) ) C_ Y } <-> X C_ Y ) )
95 17 94 bitrd 
 |-  ( ph -> ( ( M ` X ) C_ ( M ` Y ) <-> X C_ Y ) )