Metamath Proof Explorer

Theorem lhpexle2lem

Description: Lemma for lhpexle2 . (Contributed by NM, 19-Jun-2013)

Ref Expression
Hypotheses lhpex1.l 
|- .<_ = ( le ` K )
lhpex1.a 
|- A = ( Atoms ` K )
lhpex1.h 
|- H = ( LHyp ` K )
Assertion lhpexle2lem 
|- ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )

Proof

Step Hyp Ref Expression
1 lhpex1.l 
 |-  .<_ = ( le ` K )
2 lhpex1.a 
 |-  A = ( Atoms ` K )
3 lhpex1.h 
 |-  H = ( LHyp ` K )
4 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y ) -> ( K e. HL /\ W e. H ) )
5 1 2 3 lhpexle1 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X ) )
6 4 5 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y ) -> E. p e. A ( p .<_ W /\ p =/= X ) )
7 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y /\ ( p .<_ W /\ p =/= X ) ) -> p .<_ W )
8 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y /\ ( p .<_ W /\ p =/= X ) ) -> p =/= X )
9 simp2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y /\ ( p .<_ W /\ p =/= X ) ) -> X = Y )
10 8 9 neeqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y /\ ( p .<_ W /\ p =/= X ) ) -> p =/= Y )
11 7 8 10 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y /\ ( p .<_ W /\ p =/= X ) ) -> ( p .<_ W /\ p =/= X /\ p =/= Y ) )
12 11 3expia 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y ) -> ( ( p .<_ W /\ p =/= X ) -> ( p .<_ W /\ p =/= X /\ p =/= Y ) ) )
13 12 reximdv 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y ) -> ( E. p e. A ( p .<_ W /\ p =/= X ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) ) )
14 6 13 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X = Y ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )
15 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X =/= Y ) -> K e. HL )
16 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X =/= Y ) -> X e. A )
17 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X =/= Y ) -> Y e. A )
18 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X =/= Y ) -> X =/= Y )
19 eqid 
 |-  ( join ` K ) = ( join ` K )
20 1 19 2 hlsupr 
 |-  ( ( ( K e. HL /\ X e. A /\ Y e. A ) /\ X =/= Y ) -> E. p e. A ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) )
21 15 16 17 18 20 syl31anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X =/= Y ) -> E. p e. A ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) )
22 eqid 
 |-  ( Base ` K ) = ( Base ` K )
23 simpl1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> K e. HL )
24 23 hllatd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> K e. Lat )
25 simprlr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p e. A )
26 22 2 atbase 
 |-  ( p e. A -> p e. ( Base ` K ) )
27 25 26 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p e. ( Base ` K ) )
28 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> X e. A )
29 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> Y e. A )
30 22 19 2 hlatjcl 
 |-  ( ( K e. HL /\ X e. A /\ Y e. A ) -> ( X ( join ` K ) Y ) e. ( Base ` K ) )
31 23 28 29 30 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( X ( join ` K ) Y ) e. ( Base ` K ) )
32 simpl1r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> W e. H )
33 22 3 lhpbase 
 |-  ( W e. H -> W e. ( Base ` K ) )
34 32 33 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> W e. ( Base ` K ) )
35 simprr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p .<_ ( X ( join ` K ) Y ) )
36 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> X .<_ W )
37 simpl3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> Y .<_ W )
38 22 2 atbase 
 |-  ( X e. A -> X e. ( Base ` K ) )
39 28 38 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> X e. ( Base ` K ) )
40 22 2 atbase 
 |-  ( Y e. A -> Y e. ( Base ` K ) )
41 29 40 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> Y e. ( Base ` K ) )
42 22 1 19 latjle12 
 |-  ( ( K e. Lat /\ ( X e. ( Base ` K ) /\ Y e. ( Base ` K ) /\ W e. ( Base ` K ) ) ) -> ( ( X .<_ W /\ Y .<_ W ) <-> ( X ( join ` K ) Y ) .<_ W ) )
43 24 39 41 34 42 syl13anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( ( X .<_ W /\ Y .<_ W ) <-> ( X ( join ` K ) Y ) .<_ W ) )
44 36 37 43 mpbi2and 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( X ( join ` K ) Y ) .<_ W )
45 22 1 24 27 31 34 35 44 lattrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p .<_ W )
46 simprr1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p =/= X )
47 simprr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> p =/= Y )
48 45 46 47 3jca 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ ( ( X =/= Y /\ p e. A ) /\ ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) ) ) -> ( p .<_ W /\ p =/= X /\ p =/= Y ) )
49 48 exp44 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) -> ( X =/= Y -> ( p e. A -> ( ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) -> ( p .<_ W /\ p =/= X /\ p =/= Y ) ) ) ) )
50 49 imp31 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X =/= Y ) /\ p e. A ) -> ( ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) -> ( p .<_ W /\ p =/= X /\ p =/= Y ) ) )
51 50 reximdva 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X =/= Y ) -> ( E. p e. A ( p =/= X /\ p =/= Y /\ p .<_ ( X ( join ` K ) Y ) ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) ) )
52 21 51 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) /\ X =/= Y ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )
53 14 52 pm2.61dane 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )