Metamath Proof Explorer

Theorem djhcvat42

Description: A covering property. ( cvrat42 analog.) (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses djhcvat42.h 
|- H = ( LHyp ` K )
djhcvat42.u 
|- U = ( ( DVecH ` K ) ` W )
djhcvat42.v 
|- V = ( Base ` U )
djhcvat42.o 
|- .0. = ( 0g ` U )
djhcvat42.n 
|- N = ( LSpan ` U )
djhcvat42.i 
|- I = ( ( DIsoH ` K ) ` W )
djhcvat42.j 
|- .\/ = ( ( joinH ` K ) ` W )
djhcvat42.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
djhcvat42.s 
|- ( ph -> S e. ran I )
djhcvat42.x 
|- ( ph -> X e. ( V \ { .0. } ) )
djhcvat42.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
Assertion djhcvat42 
|- ( ph -> ( ( S =/= { .0. } /\ ( N ` { X } ) C_ ( S .\/ ( N ` { Y } ) ) ) -> E. z e. ( V \ { .0. } ) ( ( N ` { z } ) C_ S /\ ( N ` { X } ) C_ ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 djhcvat42.h 
 |-  H = ( LHyp ` K )
2 djhcvat42.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 djhcvat42.v 
 |-  V = ( Base ` U )
4 djhcvat42.o 
 |-  .0. = ( 0g ` U )
5 djhcvat42.n 
 |-  N = ( LSpan ` U )
6 djhcvat42.i 
 |-  I = ( ( DIsoH ` K ) ` W )
7 djhcvat42.j 
 |-  .\/ = ( ( joinH ` K ) ` W )
8 djhcvat42.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 djhcvat42.s 
 |-  ( ph -> S e. ran I )
10 djhcvat42.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
11 djhcvat42.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
12 8 simpld 
 |-  ( ph -> K e. HL )
13 eqid 
 |-  ( Base ` K ) = ( Base ` K )
14 13 1 6 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. ran I ) -> ( `' I ` S ) e. ( Base ` K ) )
15 8 9 14 syl2anc 
 |-  ( ph -> ( `' I ` S ) e. ( Base ` K ) )
16 10 eldifad 
 |-  ( ph -> X e. V )
17 eldifsni 
 |-  ( X e. ( V \ { .0. } ) -> X =/= .0. )
18 10 17 syl 
 |-  ( ph -> X =/= .0. )
19 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
20 19 1 2 3 4 5 6 dihlspsnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ X =/= .0. ) -> ( `' I ` ( N ` { X } ) ) e. ( Atoms ` K ) )
21 8 16 18 20 syl3anc 
 |-  ( ph -> ( `' I ` ( N ` { X } ) ) e. ( Atoms ` K ) )
22 11 eldifad 
 |-  ( ph -> Y e. V )
23 eldifsni 
 |-  ( Y e. ( V \ { .0. } ) -> Y =/= .0. )
24 11 23 syl 
 |-  ( ph -> Y =/= .0. )
25 19 1 2 3 4 5 6 dihlspsnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V /\ Y =/= .0. ) -> ( `' I ` ( N ` { Y } ) ) e. ( Atoms ` K ) )
26 8 22 24 25 syl3anc 
 |-  ( ph -> ( `' I ` ( N ` { Y } ) ) e. ( Atoms ` K ) )
27 eqid 
 |-  ( le ` K ) = ( le ` K )
28 eqid 
 |-  ( join ` K ) = ( join ` K )
29 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
30 13 27 28 29 19 cvrat42 
 |-  ( ( K e. HL /\ ( ( `' I ` S ) e. ( Base ` K ) /\ ( `' I ` ( N ` { X } ) ) e. ( Atoms ` K ) /\ ( `' I ` ( N ` { Y } ) ) e. ( Atoms ` K ) ) ) -> ( ( ( `' I ` S ) =/= ( 0. ` K ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` S ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) -> E. r e. ( Atoms ` K ) ( r ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( r ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) ) )
31 12 15 21 26 30 syl13anc 
 |-  ( ph -> ( ( ( `' I ` S ) =/= ( 0. ` K ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` S ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) -> E. r e. ( Atoms ` K ) ( r ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( r ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) ) )
32 1 29 6 2 3 4 5 8 9 dih0sb 
 |-  ( ph -> ( S = { .0. } <-> ( `' I ` S ) = ( 0. ` K ) ) )
33 32 necon3bid 
 |-  ( ph -> ( S =/= { .0. } <-> ( `' I ` S ) =/= ( 0. ` K ) ) )
34 1 2 3 5 6 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I )
35 8 16 34 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ran I )
36 1 2 6 3 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ S e. ran I ) -> S C_ V )
37 8 9 36 syl2anc 
 |-  ( ph -> S C_ V )
38 1 2 3 5 6 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y e. V ) -> ( N ` { Y } ) e. ran I )
39 8 22 38 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ran I )
40 1 2 6 3 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { Y } ) e. ran I ) -> ( N ` { Y } ) C_ V )
41 8 39 40 syl2anc 
 |-  ( ph -> ( N ` { Y } ) C_ V )
42 1 6 2 3 7 djhcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( S C_ V /\ ( N ` { Y } ) C_ V ) ) -> ( S .\/ ( N ` { Y } ) ) e. ran I )
43 8 37 41 42 syl12anc 
 |-  ( ph -> ( S .\/ ( N ` { Y } ) ) e. ran I )
44 27 1 6 8 35 43 dihcnvord 
 |-  ( ph -> ( ( `' I ` ( N ` { X } ) ) ( le ` K ) ( `' I ` ( S .\/ ( N ` { Y } ) ) ) <-> ( N ` { X } ) C_ ( S .\/ ( N ` { Y } ) ) ) )
45 28 1 6 7 8 9 39 djhj 
 |-  ( ph -> ( `' I ` ( S .\/ ( N ` { Y } ) ) ) = ( ( `' I ` S ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) )
46 45 breq2d 
 |-  ( ph -> ( ( `' I ` ( N ` { X } ) ) ( le ` K ) ( `' I ` ( S .\/ ( N ` { Y } ) ) ) <-> ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` S ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) )
47 44 46 bitr3d 
 |-  ( ph -> ( ( N ` { X } ) C_ ( S .\/ ( N ` { Y } ) ) <-> ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` S ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) )
48 33 47 anbi12d 
 |-  ( ph -> ( ( S =/= { .0. } /\ ( N ` { X } ) C_ ( S .\/ ( N ` { Y } ) ) ) <-> ( ( `' I ` S ) =/= ( 0. ` K ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` S ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) ) )
49 8 adantr 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( K e. HL /\ W e. H ) )
50 eldifi 
 |-  ( z e. ( V \ { .0. } ) -> z e. V )
51 50 adantl 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> z e. V )
52 eldifsni 
 |-  ( z e. ( V \ { .0. } ) -> z =/= .0. )
53 52 adantl 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> z =/= .0. )
54 19 1 2 3 4 5 6 dihlspsnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ z e. V /\ z =/= .0. ) -> ( `' I ` ( N ` { z } ) ) e. ( Atoms ` K ) )
55 49 51 53 54 syl3anc 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( `' I ` ( N ` { z } ) ) e. ( Atoms ` K ) )
56 19 1 2 3 4 5 6 8 dihatexv2 
 |-  ( ph -> ( r e. ( Atoms ` K ) <-> E. z e. ( V \ { .0. } ) r = ( `' I ` ( N ` { z } ) ) ) )
57 breq1 
 |-  ( r = ( `' I ` ( N ` { z } ) ) -> ( r ( le ` K ) ( `' I ` S ) <-> ( `' I ` ( N ` { z } ) ) ( le ` K ) ( `' I ` S ) ) )
58 oveq1 
 |-  ( r = ( `' I ` ( N ` { z } ) ) -> ( r ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) = ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) )
59 58 breq2d 
 |-  ( r = ( `' I ` ( N ` { z } ) ) -> ( ( `' I ` ( N ` { X } ) ) ( le ` K ) ( r ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) <-> ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) )
60 57 59 anbi12d 
 |-  ( r = ( `' I ` ( N ` { z } ) ) -> ( ( r ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( r ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) <-> ( ( `' I ` ( N ` { z } ) ) ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) ) )
61 60 adantl 
 |-  ( ( ph /\ r = ( `' I ` ( N ` { z } ) ) ) -> ( ( r ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( r ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) <-> ( ( `' I ` ( N ` { z } ) ) ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) ) )
62 55 56 61 rexxfr2d 
 |-  ( ph -> ( E. r e. ( Atoms ` K ) ( r ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( r ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) <-> E. z e. ( V \ { .0. } ) ( ( `' I ` ( N ` { z } ) ) ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) ) )
63 1 2 3 5 6 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ z e. V ) -> ( N ` { z } ) e. ran I )
64 49 51 63 syl2anc 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( N ` { z } ) e. ran I )
65 9 adantr 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> S e. ran I )
66 27 1 6 49 64 65 dihcnvord 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( `' I ` ( N ` { z } ) ) ( le ` K ) ( `' I ` S ) <-> ( N ` { z } ) C_ S ) )
67 39 adantr 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( N ` { Y } ) e. ran I )
68 28 1 6 7 49 64 67 djhj 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( `' I ` ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) = ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) )
69 68 breq2d 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( `' I ` ( N ` { X } ) ) ( le ` K ) ( `' I ` ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) <-> ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) )
70 16 adantr 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> X e. V )
71 49 70 34 syl2anc 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( N ` { X } ) e. ran I )
72 1 2 6 3 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( N ` { z } ) e. ran I ) -> ( N ` { z } ) C_ V )
73 49 64 72 syl2anc 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( N ` { z } ) C_ V )
74 41 adantr 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( N ` { Y } ) C_ V )
75 1 6 2 3 7 djhcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( N ` { z } ) C_ V /\ ( N ` { Y } ) C_ V ) ) -> ( ( N ` { z } ) .\/ ( N ` { Y } ) ) e. ran I )
76 49 73 74 75 syl12anc 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( N ` { z } ) .\/ ( N ` { Y } ) ) e. ran I )
77 27 1 6 49 71 76 dihcnvord 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( `' I ` ( N ` { X } ) ) ( le ` K ) ( `' I ` ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) <-> ( N ` { X } ) C_ ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) )
78 69 77 bitr3d 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) <-> ( N ` { X } ) C_ ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) )
79 66 78 anbi12d 
 |-  ( ( ph /\ z e. ( V \ { .0. } ) ) -> ( ( ( `' I ` ( N ` { z } ) ) ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) <-> ( ( N ` { z } ) C_ S /\ ( N ` { X } ) C_ ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) ) )
80 79 rexbidva 
 |-  ( ph -> ( E. z e. ( V \ { .0. } ) ( ( `' I ` ( N ` { z } ) ) ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( ( `' I ` ( N ` { z } ) ) ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) <-> E. z e. ( V \ { .0. } ) ( ( N ` { z } ) C_ S /\ ( N ` { X } ) C_ ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) ) )
81 62 80 bitr2d 
 |-  ( ph -> ( E. z e. ( V \ { .0. } ) ( ( N ` { z } ) C_ S /\ ( N ` { X } ) C_ ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) <-> E. r e. ( Atoms ` K ) ( r ( le ` K ) ( `' I ` S ) /\ ( `' I ` ( N ` { X } ) ) ( le ` K ) ( r ( join ` K ) ( `' I ` ( N ` { Y } ) ) ) ) ) )
82 31 48 81 3imtr4d 
 |-  ( ph -> ( ( S =/= { .0. } /\ ( N ` { X } ) C_ ( S .\/ ( N ` { Y } ) ) ) -> E. z e. ( V \ { .0. } ) ( ( N ` { z } ) C_ S /\ ( N ` { X } ) C_ ( ( N ` { z } ) .\/ ( N ` { Y } ) ) ) ) )