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 ) )