Metamath Proof Explorer

Theorem paddasslem5

Description: Lemma for paddass . Show s =/= z by contradiction. (Contributed by NM, 8-Jan-2012)

Ref Expression
Hypotheses paddasslem.l 
|- .<_ = ( le ` K )
paddasslem.j 
|- .\/ = ( join ` K )
paddasslem.a 
|- A = ( Atoms ` K )
Assertion paddasslem5 
|- ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) ) -> s =/= z )

Proof

Step Hyp Ref Expression
1 paddasslem.l 
 |-  .<_ = ( le ` K )
2 paddasslem.j 
 |-  .\/ = ( join ` K )
3 paddasslem.a 
 |-  A = ( Atoms ` K )
4 breq1 
 |-  ( s = z -> ( s .<_ ( x .\/ y ) <-> z .<_ ( x .\/ y ) ) )
5 4 biimpac 
 |-  ( ( s .<_ ( x .\/ y ) /\ s = z ) -> z .<_ ( x .\/ y ) )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 simpll1 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> K e. HL )
8 7 hllatd 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> K e. Lat )
9 simpll2 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> r e. A )
10 6 3 atbase 
 |-  ( r e. A -> r e. ( Base ` K ) )
11 9 10 syl 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> r e. ( Base ` K ) )
12 simp32 
 |-  ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> y e. A )
13 12 ad2antrr 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> y e. A )
14 6 3 atbase 
 |-  ( y e. A -> y e. ( Base ` K ) )
15 13 14 syl 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> y e. ( Base ` K ) )
16 simp33 
 |-  ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> z e. A )
17 16 ad2antrr 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> z e. A )
18 6 3 atbase 
 |-  ( z e. A -> z e. ( Base ` K ) )
19 17 18 syl 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> z e. ( Base ` K ) )
20 6 2 latjcl 
 |-  ( ( K e. Lat /\ y e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( y .\/ z ) e. ( Base ` K ) )
21 8 15 19 20 syl3anc 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> ( y .\/ z ) e. ( Base ` K ) )
22 simp31 
 |-  ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> x e. A )
23 22 ad2antrr 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> x e. A )
24 6 3 atbase 
 |-  ( x e. A -> x e. ( Base ` K ) )
25 23 24 syl 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> x e. ( Base ` K ) )
26 6 2 latjcl 
 |-  ( ( K e. Lat /\ x e. ( Base ` K ) /\ y e. ( Base ` K ) ) -> ( x .\/ y ) e. ( Base ` K ) )
27 8 25 15 26 syl3anc 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> ( x .\/ y ) e. ( Base ` K ) )
28 simplr 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> r .<_ ( y .\/ z ) )
29 1 2 3 hlatlej2 
 |-  ( ( K e. HL /\ x e. A /\ y e. A ) -> y .<_ ( x .\/ y ) )
30 7 23 13 29 syl3anc 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> y .<_ ( x .\/ y ) )
31 simpr 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> z .<_ ( x .\/ y ) )
32 6 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( y e. ( Base ` K ) /\ z e. ( Base ` K ) /\ ( x .\/ y ) e. ( Base ` K ) ) ) -> ( ( y .<_ ( x .\/ y ) /\ z .<_ ( x .\/ y ) ) <-> ( y .\/ z ) .<_ ( x .\/ y ) ) )
33 32 biimpd 
 |-  ( ( K e. Lat /\ ( y e. ( Base ` K ) /\ z e. ( Base ` K ) /\ ( x .\/ y ) e. ( Base ` K ) ) ) -> ( ( y .<_ ( x .\/ y ) /\ z .<_ ( x .\/ y ) ) -> ( y .\/ z ) .<_ ( x .\/ y ) ) )
34 8 15 19 27 33 syl13anc 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> ( ( y .<_ ( x .\/ y ) /\ z .<_ ( x .\/ y ) ) -> ( y .\/ z ) .<_ ( x .\/ y ) ) )
35 30 31 34 mp2and 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> ( y .\/ z ) .<_ ( x .\/ y ) )
36 6 1 8 11 21 27 28 35 lattrd 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ z .<_ ( x .\/ y ) ) -> r .<_ ( x .\/ y ) )
37 36 ex 
 |-  ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) -> ( z .<_ ( x .\/ y ) -> r .<_ ( x .\/ y ) ) )
38 5 37 syl5 
 |-  ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) -> ( ( s .<_ ( x .\/ y ) /\ s = z ) -> r .<_ ( x .\/ y ) ) )
39 38 expdimp 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ s .<_ ( x .\/ y ) ) -> ( s = z -> r .<_ ( x .\/ y ) ) )
40 39 necon3bd 
 |-  ( ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ r .<_ ( y .\/ z ) ) /\ s .<_ ( x .\/ y ) ) -> ( -. r .<_ ( x .\/ y ) -> s =/= z ) )
41 40 exp31 
 |-  ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( r .<_ ( y .\/ z ) -> ( s .<_ ( x .\/ y ) -> ( -. r .<_ ( x .\/ y ) -> s =/= z ) ) ) )
42 41 com23 
 |-  ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( s .<_ ( x .\/ y ) -> ( r .<_ ( y .\/ z ) -> ( -. r .<_ ( x .\/ y ) -> s =/= z ) ) ) )
43 42 com24 
 |-  ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( -. r .<_ ( x .\/ y ) -> ( r .<_ ( y .\/ z ) -> ( s .<_ ( x .\/ y ) -> s =/= z ) ) ) )
44 43 3imp2 
 |-  ( ( ( K e. HL /\ r e. A /\ ( x e. A /\ y e. A /\ z e. A ) ) /\ ( -. r .<_ ( x .\/ y ) /\ r .<_ ( y .\/ z ) /\ s .<_ ( x .\/ y ) ) ) -> s =/= z )