Metamath Proof Explorer

Theorem exatleN

Description: A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in Crawley p. 112. (Contributed by NM, 28-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses atomle.b 
|- B = ( Base ` K )
atomle.l 
|- .<_ = ( le ` K )
atomle.j 
|- .\/ = ( join ` K )
atomle.a 
|- A = ( Atoms ` K )
Assertion exatleN 
|- ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R .<_ X <-> R = P ) )

Proof

Step Hyp Ref Expression
1 atomle.b 
 |-  B = ( Base ` K )
2 atomle.l 
 |-  .<_ = ( le ` K )
3 atomle.j 
 |-  .\/ = ( join ` K )
4 atomle.a 
 |-  A = ( Atoms ` K )
5 simpl32 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P ) -> -. Q .<_ X )
6 simp11l 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> K e. HL )
7 6 hllatd 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> K e. Lat )
8 simp122 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> Q e. A )
9 1 4 atbase 
 |-  ( Q e. A -> Q e. B )
10 8 9 syl 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> Q e. B )
11 simp121 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> P e. A )
12 1 4 atbase 
 |-  ( P e. A -> P e. B )
13 11 12 syl 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> P e. B )
14 simp123 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R e. A )
15 1 4 atbase 
 |-  ( R e. A -> R e. B )
16 14 15 syl 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R e. B )
17 1 3 latjcl 
 |-  ( ( K e. Lat /\ P e. B /\ R e. B ) -> ( P .\/ R ) e. B )
18 7 13 16 17 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( P .\/ R ) e. B )
19 simp11r 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> X e. B )
20 14 8 11 3jca 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( R e. A /\ Q e. A /\ P e. A ) )
21 simp2 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R =/= P )
22 6 20 21 3jca 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( K e. HL /\ ( R e. A /\ Q e. A /\ P e. A ) /\ R =/= P ) )
23 simp133 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R .<_ ( P .\/ Q ) )
24 2 3 4 hlatexch1 
 |-  ( ( K e. HL /\ ( R e. A /\ Q e. A /\ P e. A ) /\ R =/= P ) -> ( R .<_ ( P .\/ Q ) -> Q .<_ ( P .\/ R ) ) )
25 22 23 24 sylc 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> Q .<_ ( P .\/ R ) )
26 simp131 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> P .<_ X )
27 simp3 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> R .<_ X )
28 1 2 3 latjle12 
 |-  ( ( K e. Lat /\ ( P e. B /\ R e. B /\ X e. B ) ) -> ( ( P .<_ X /\ R .<_ X ) <-> ( P .\/ R ) .<_ X ) )
29 7 13 16 19 28 syl13anc 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( ( P .<_ X /\ R .<_ X ) <-> ( P .\/ R ) .<_ X ) )
30 26 27 29 mpbi2and 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> ( P .\/ R ) .<_ X )
31 1 2 7 10 18 19 25 30 lattrd 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P /\ R .<_ X ) -> Q .<_ X )
32 31 3expia 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P ) -> ( R .<_ X -> Q .<_ X ) )
33 5 32 mtod 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) /\ R =/= P ) -> -. R .<_ X )
34 33 ex 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R =/= P -> -. R .<_ X ) )
35 34 necon4ad 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R .<_ X -> R = P ) )
36 simp31 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> P .<_ X )
37 breq1 
 |-  ( R = P -> ( R .<_ X <-> P .<_ X ) )
38 36 37 syl5ibrcom 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R = P -> R .<_ X ) )
39 35 38 impbid 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P .<_ X /\ -. Q .<_ X /\ R .<_ ( P .\/ Q ) ) ) -> ( R .<_ X <-> R = P ) )